...
 
Commits (39)
image: gitlab-runner/haskell
stages:
- build
Build:
stage:
build
script:
- make build
- cp dist/build/peregrine/peregrine peregrine
artifacts:
paths:
- peregrine
when: on_success
expire_in: 1 week
all: build all: build
build: build:
cabal install --only-dependencies
cabal build cabal build
install: install:
......
...@@ -11,6 +11,11 @@ echo "generating majority protocol" ...@@ -11,6 +11,11 @@ echo "generating majority protocol"
mkdir -p $benchmark_dir/$protocols_dir/majority mkdir -p $benchmark_dir/$protocols_dir/majority
$executable majorityPP >$benchmark_dir/$protocols_dir/majority/majority_m1_.pp $executable majorityPP >$benchmark_dir/$protocols_dir/majority/majority_m1_.pp
# fast majority
echo "generating fast majority protocol"
mkdir -p $benchmark_dir/$protocols_dir/fastmajority
cp ../examples/fastmajority.pp $benchmark_dir/$protocols_dir/fastmajority/fastmajority_m1_.pp
# broadcast # broadcast
echo "generating broadcast protocol" echo "generating broadcast protocol"
mkdir -p $benchmark_dir/$protocols_dir/broadcast mkdir -p $benchmark_dir/$protocols_dir/broadcast
...@@ -25,25 +30,64 @@ for l in 2 3 4 5 6 7 8 9 10 11 12 13 14 15; do ...@@ -25,25 +30,64 @@ for l in 2 3 4 5 6 7 8 9 10 11 12 13 14 15; do
done done
done done
# modulo # Remainder
echo "generating modulo protocols" echo "generating remainder protocols"
mkdir -p $benchmark_dir/$protocols_dir/modulo mkdir -p $benchmark_dir/$protocols_dir/remainder
for m in 2 3 4 5 6 7 8 9 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150; do for m in 2 3 4 5 6 7 8 9 10 15 20 25 30 35 40 45 50 55 60 65 70 75 80 90 100 110 120 130 140 150; do
for c in 1; do for c in 1; do
$executable moduloPP $m $c >$benchmark_dir/$protocols_dir/modulo/modulo_m${m}_c${c}_.pp $executable moduloPP $m $c >$benchmark_dir/$protocols_dir/remainder/remainder_m${m}_c${c}_.pp
done done
done done
# flock of birds # Flock of Birds from Chatzigianniks, Michail, Spirakis: Algorithmic verification of population protocols
echo "generating flockofbirds protocols" echo "generating flockofbirds protocols"
mkdir -p $benchmark_dir/$protocols_dir/flockofbirds mkdir -p $benchmark_dir/$protocols_dir/flockofbirds
for c in 10 15 20 25 30 35 40 45 50 55 60 65 70 75 80 85 90 95 100; do for c in 10 15 20 25 30 35 40 45 50 55 60 65 70 80 90 100 110 120 130 140 150; do
$executable flockOfBirdsPP $c >$benchmark_dir/$protocols_dir/flockofbirds/flockofbirds_c${c}_.pp $executable flockOfBirdsPP $c >$benchmark_dir/$protocols_dir/flockofbirds/flockofbirds_c${c}_.pp
done done
# new birds # new birds from Clément, Delporte-Gallet, Fauconnier, Sighireanu: Guidelines for the verification of population protocols
echo "generating newbirds protocols" echo "generating newbirds protocols"
mkdir -p $benchmark_dir/$protocols_dir/newbirds mkdir -p $benchmark_dir/$protocols_dir/newbirds
for c in 10 20 25 30 40 50 75 100 125 150 175 200 225 250 275 300 325 350; do for c in 50 100 150 200 250 300 350 400 450 500 550 600 650 700 750 800; do
$executable newBirdsPP $c >$benchmark_dir/$protocols_dir/newbirds/newbirds_c${c}_.pp $executable newBirdsPP $c >$benchmark_dir/$protocols_dir/newbirds/newbirds_c${c}_.pp
done done
# Logarithmic Flock of Birds
echo "generating logarithmic flock of birds protocols"
mkdir -p $benchmark_dir/$protocols_dir/logflockofbirds
for clog in 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 25 30 35 40; do
c=$(python -c "print(10**${clog})")
python python/execprotocol.py python/flock_log.py "{\"scheme\": { \"threshold\": { \"value\": ${c} } } }" >$benchmark_dir/$protocols_dir/logflockofbirds/logflockofbirds_c${clog}_.pp
done
# Tower Flock of Birds
echo "generating tower flock of birds protocols"
mkdir -p $benchmark_dir/$protocols_dir/towerflockofbirds
for c in 25 50 75 100 125 150 175 200 225 250 275 300 325 350 375 400 425 450 475 500 525 550 575 600; do
python python/execprotocol.py python/flock_of_birds_-_tower.py "{\"scheme\": { \"c\": { \"value\": ${c} } } }" >$benchmark_dir/$protocols_dir/towerflockofbirds/towerflockofbirds_c${c}_.pp
done
# Average and Conquer
echo "generating average and conquer protocol"
mkdir -p $benchmark_dir/$protocols_dir/avc
n_lower=2
#for m in 3 5 7 9 11 13 15 17 19 21 23 25 27 29 31 33 35 37 39 41 45 51 55 61 65 71 75 81 85 91 95 101; do
for m in 15 25 35 45 55 65 75 85 95 105; do
n_upper=10000000
## while [[ $(($n_upper - $n_lower)) -gt 1 ]]; do
## n=$(((n_upper + n_lower) / 2))
## mlow=$(python -c "import math; print(math.ceil(math.log(${n})*math.log(math.log(${n}))))")
## #echo "At m=$m, intervl [$n_lower, $n_upper], n = $n; m'=$mlow"
## if [[ $mlow -le $m ]]; then
## n_lower=$n
## else
## n_upper=$n
## fi
## done
## n=$n_lower
## d=$(python -c "import math; print(math.ceil(math.log(${m})*math.log(${n})))")
## echo "For m=$m got n=$n, d=$d"
d=1
python python/execprotocol.py python/avc.py "{\"scheme\": { \"m\": { \"value\": ${m} }, \"d\": { \"value\": ${d} } } }">$benchmark_dir/$protocols_dir/avc/avc_m${m}_d${d}_.pp
done
...@@ -26,7 +26,7 @@ if len(sys.argv) >= 2: ...@@ -26,7 +26,7 @@ if len(sys.argv) >= 2:
print("unknown argument: %s" % arg, file=sys.stderr) print("unknown argument: %s" % arg, file=sys.stderr)
sys.exit(-1) sys.exit(-1)
else: else:
results_file = sys.argv[1] results_file = arg
# long table # long table
...@@ -136,7 +136,6 @@ if long_table: ...@@ -136,7 +136,6 @@ if long_table:
# short table # short table
if short_table: if short_table:
results_file='results.csv'
results = pd.read_csv(results_file) results = pd.read_csv(results_file)
......
...@@ -21,6 +21,7 @@ executable pp-print ...@@ -21,6 +21,7 @@ executable pp-print
main-is: Main.hs main-is: Main.hs
other-modules: other-modules:
-- other-extensions: -- other-extensions:
build-depends: multiset, base >= 4.8, containers, aeson, aeson-pretty, bytestring build-depends: base >= 4.8, containers, aeson, aeson-pretty, bytestring
hs-source-dirs: src hs-source-dirs: src
default-language: Haskell2010 default-language: Haskell2010
ghc-options: -dynamic
module PopulationProtocol ( PopulationProtocol (..) module PopulationProtocol ( PopulationProtocol (..)
, Population
, createModuloProtocol , createModuloProtocol
, createThresholdProtocol , createThresholdProtocol
, createOldThresholdProtocol , createOldThresholdProtocol
...@@ -18,7 +17,6 @@ module PopulationProtocol ( PopulationProtocol (..) ...@@ -18,7 +17,6 @@ module PopulationProtocol ( PopulationProtocol (..)
import Util import Util
import qualified Data.Set as S import qualified Data.Set as S
import qualified Data.MultiSet as MS
import qualified Data.Map.Strict as M import qualified Data.Map.Strict as M
import Data.Tuple (swap) import Data.Tuple (swap)
import Data.List (intercalate, nub) import Data.List (intercalate, nub)
...@@ -47,8 +45,6 @@ type FlockOfBirdsProtocol = PopulationProtocol Int ...@@ -47,8 +45,6 @@ type FlockOfBirdsProtocol = PopulationProtocol Int
type VerifiableFlockOfBirdsProtocol = PopulationProtocol (Bool, Int) type VerifiableFlockOfBirdsProtocol = PopulationProtocol (Bool, Int)
type Population qs = MS.MultiSet qs
data ThresholdState = Neg Int | Pos Int | BiasPos Int | Passive Bool deriving (Ord, Eq, Show) data ThresholdState = Neg Int | Pos Int | BiasPos Int | Passive Bool deriving (Ord, Eq, Show)
data SimpleState = L Int | NL Int deriving (Ord, Eq, Show) data SimpleState = L Int | NL Int deriving (Ord, Eq, Show)
...@@ -283,9 +279,9 @@ createModuloProtocol n c = PopulationProtocol { states = [Mod i | i <- [0..(n-1) ...@@ -283,9 +279,9 @@ createModuloProtocol n c = PopulationProtocol { states = [Mod i | i <- [0..(n-1)
modOpinion (Mod a) = a == c modOpinion (Mod a) = a == c
modOpinion (ModPassive b) = b modOpinion (ModPassive b) = b
modPredicate = "EXISTS k : " ++ modPredicate = "( " ++
(intercalate " + " [ show i ++ " * " ++ toVar (Mod i) | i <- [0..(n-1)] ]) ++ (intercalate " + " [ show i ++ " * " ++ toVar (Mod i) | i <- [0..(n-1)] ]) ++
" = " ++ show c ++ " + " ++ show n ++ " * k" " ) =% " ++ show n ++ " " ++ show c
createMajorityProtocol :: MajorityProtocol createMajorityProtocol :: MajorityProtocol
......
# -*- coding: utf-8 -*-
params = {
'scheme': {
'm': {
'descr': "m",
'values': range(3, 22, 2),
'value': 3
},
'd': {
'descr': "d",
'values': range(1, 16),
'value': 1
}
}
}
def generateProtocol(params):
m = params["scheme"]["m"]["value"]
d = params["scheme"]["d"]["value"]
# Generate states
states = [("weak", ("+", 0)), ("weak", ("-", 0))]
for n in range(3, m + 1, 2):
states.append(("strong", n))
states.append(("strong", -n))
for n in range(1, d + 1):
states.append(("intermediate", ("+", n)))
states.append(("intermediate", ("-", n)))
# Helper functions
def strong(x):
return x[0] == "strong"
def intermediate(x):
return x[0] == "intermediate"
def weak(x):
return x[0] == "weak"
def value(x):
if strong(x):
return x[1]
elif intermediate(x):
return 1 if x[1][0] == "+" else -1
elif weak(x):
return 0
def weight(x):
return abs(value(x))
def sgn(x):
if strong(x) or intermediate(x):
return 1 if value(x) > 0 else -1
else:
return 1 if x[1][0] == "+" else -1
def phi(r):
if abs(r) > 1:
return ("strong", r)
else:
return ("intermediate", ("+" if r > 0 else "-", 1))
def r_down(k):
r = k if abs(k) % 2 == 1 else k - 1
return phi(r);
def r_up(k):
r = k if abs(k) % 2 == 1 else k + 1
return phi(r)
def shift_to_zero(x):
if intermediate(x):
j = x[1][1]
if j < d:
sign = "+" if value(x) == 1 else "-"
return ("intermediate", (sign, j + 1))
return x
def sign_to_zero(x):
sign = "+" if sgn(x) > 0 else "-"
return ("weak", (sign, 0))
def update(x, y):
if ((weight(x) > 0 and weight(y) > 1) or (weight(y) > 0 and weight(x) > 1)):
x_ = r_down((value(x) + value(y)) // 2)
y_ = r_up((value(x) + value(y)) // 2)
elif (weight(x) * weight(y) == 0 and value(x) + value(y) != 0):
if weight(x) != 0:
x_ = shift_to_zero(x)
y_ = sign_to_zero(x)
else:
y_ = shift_to_zero(y)
x_ = sign_to_zero(y)
elif ((intermediate(x) and x[1][1] == d and weight(y) and sgn(x) != sgn(y)) or
(intermediate(y) and y[1][1] == d and weight(x) and sgn(y) != sgn(x))):
x_ = ("weak", ("-", 0))
y_ = ("weak", ("+", 0))
else:
x_ = shift_to_zero(x)
y_ = shift_to_zero(y)
return (x_, y_)
def state_repr(x):
sign = "G" if sgn(x) > 0 else "B"
if strong(x):
return "{}{}".format(sign, weight(x))
elif intermediate(x):
return "{}1_{}".format(sign, x[1][1])
else:
return "{}0".format(sign)
def pair_repr(pair):
return list(map(state_repr, pair))
def generate_states():
return list(map(state_repr, states))
def generate_transitions():
transitions = []
for x in range(0, len(states)):
for y in range(x, len(states)):
p = states[x]
q = states[y]
pre = pair_repr((p, q))
post = pair_repr(update(p, q))
if not Utils.silent(pre, post):
transitions.append(Utils.transition(pre, post))
return transitions
def generate_initial_states():
return ["G{}".format(m), "B{}".format(m)]
def generate_true_states():
return [state_repr(q) for q in states if sgn(q) == 1]
def generate_predicate():
return "C[G{0}] >= C[B{0}]".format(m)
def generate_precondition():
return "C[G{0}] != C[B{0}]".format(m)
def generate_pescription():
return """This protocol is a fast and exact majority protocol. It computes
whether there are initially more agents voting yes (represented by
state Gm) than agents voting no (represented by state Bm). The protocol
does not handle ties. Parameters m and d control the running time
of the protocol. Described in Dan Alistarh, Rati Gelashvili,
Milan Vojnović. Fast and Exact Majority in Population Protocols.
PODC 2015."""
return {
"title": "Average and Conquer protocol",
"states": generate_states(),
"transitions": generate_transitions(),
"initialStates": generate_initial_states(),
"trueStates": generate_true_states(),
"predicate": generate_predicate(),
"precondition": generate_precondition(),
"description": generate_pescription()
}
# EDIT_WYSIWYG_ONLY
# -*- coding: utf-8 -*-
# This file has been created by Peregrine.
# Do not edit manually!
def generateProtocol(params):
return {
"title": "Broadcast protocol",
"states": ["yes", "no"],
"transitions": [Utils.transition(["yes", "no"], ["yes", "yes"])],
"initialStates": ["yes", "no"],
"trueStates": ["yes"],
"predicate": "C[yes] >= 1",
"description": """This protocol computes whether at least one agent is
initially in state yes."""
}
\ No newline at end of file
#!/usr/bin/env python
# -*- coding: utf-8 -*-
import sys
import json
import re
class Utils:
@staticmethod
def transition(pre, post):
return {
"name": "{}, {} -> {}, {}".format(pre[0], pre[1], post[0], post[1]),
"pre": [pre[0], pre[1]],
"post": [post[0], post[1]]
}
@staticmethod
def silent(pre, post):
return ((pre[0] == post[0] and pre[1] == post[1]) or
(pre[0] == post[1] and pre[1] == post[0]))
n = len(sys.argv)
def to_string(p):
return "s" + re.sub(r'[^a-zA-Z0-9_]', r'_', str(p))
if (n != 2 and n != 3):
print("Usage: program [file path] [param dict]")
else:
script = sys.argv[1]
exec(open(script).read())
if (n == 3):
params = json.loads(sys.argv[2])
protocol = generateProtocol(params)
# Convert states to strings
for p in ["states", "initialStates", "trueStates"]:
protocol[p] = list(map(to_string, protocol[p]))
for i in range(len(protocol["transitions"])):
for p in ["pre", "post"]:
protocol["transitions"][i][p] = list(map(to_string, protocol["transitions"][i][p]))
protocol["predicate"] = re.sub(r'C\[([^]]*)\]', lambda match: to_string(match.group(1)), protocol["predicate"])
if "precondition" in protocol:
protocol["precondition"] = re.sub(r'C\[([^]]*)\]', lambda match: to_string(match.group(1)), protocol["precondition"])
if "statesStyle" in protocol:
style = protocol["statesStyle"]
protocol["statesStyle"] = {str(p): style[p] for p in style}
print(json.dumps(protocol))
else:
try:
params
except NameError:
params = {}
print(json.dumps(params))
# -*- coding: utf-8 -*-
import math
params = {
"scheme": {
"threshold": {
"descr": "Threshold c",
"values": range(1, 201),
"value": 10
}
}
}
def generateProtocol(params):
c = params["scheme"]["threshold"]["value"]
i = int(math.log(c, 2))
states = [0] + [2**j for j in range(0, i + 1)]
cur_state = 2**i
for j in range(i-1, 0, -1):
if c & 2**j:
cur_state += 2**j
states.append(cur_state)
if c not in states:
states.append(c)
transitions = []
for x in range(len(states)):
for y in range(x, len(states)):
q1 = states[x]
q2 = states[y]
sum = q1 + q2
pre = (q1, q2)
post = None
if sum < c and q1 != 0 and q2 != 0 and sum in states:
post = (sum, 0)
elif sum >= c:
post = (c, c)
if (post is not None) and (not Utils.silent(pre, post)):
transitions.append(Utils.transition(pre, post))
style = {q: {} for q in states}
for q in states:
if q < c:
style[q]["size"] = 0.5 + 0.5 * (q + 1) / (c + 1)
style[q]["color"] = "rgb({}, {}, {})".format(105 + 128 * (c - q) / c, 30, 99)
style[0]["color"] = "rgb(175, 175, 175)"
return {
"title": "Logarithmic flock-of-birds protocol",
"states": states,
"transitions": transitions,
"initialStates": [1],
"trueStates": [c],
"predicate": "C[1] >= {}".format(c),
"description": """This protocol computes whether the population size
is at least c. The protocol has O(log c) states.""",
"statesStyle": style
}
# -*- coding: utf-8 -*-
params = {
"scheme": {
"c": {
"descr": "Threshold c",
"values": range(1, 201),
"value": 3
}
}
}
def generateProtocol(params):
c = params["scheme"]["c"]["value"]
states = range(1, c + 1)
transitions = []
for i in states:
for j in states:
if i < c and i == j:
transitions.append(Utils.transition((i, j), (i, j+1)))
elif (i == c or j == c) and (i != c or j != c):
transitions.append(Utils.transition((i, j), (c, c)))
return {
"title": "Flock-of-birds protocol (Tower)",
"states": states,
"transitions": transitions,
"initialStates": [1],
"trueStates": [c],
"predicate": "C[1] >= {}".format(c),
"description": """This protocol computes whether a population of
birds contains at least c sick birds, i.e. whether
C[1] >= c. Described in Dana Angluin, James
Aspnes, David Eisenstat, Eric Ruppert.
The Computational Power of Population Protocols.
"""
}
\ No newline at end of file
# EDIT_WYSIWYG_ONLY
#-*- coding: utf-8 -*-
# This file has been created by Peregrine.
# Do not edit manually!
def generateProtocol(params):
return {
"title": "Majority voting protocol",
"states": ["Y", "N", "y", "n"],
"transitions": [Utils.transition(("Y", "N"), ("y", "n")),
Utils.transition(("Y", "n"), ("Y", "y")),
Utils.transition(("N", "y"), ("N", "n")),
Utils.transition(("y", "n"), ("y", "y"))],
"initialStates": ["Y", "N"],
"trueStates": ["Y", "y"],
"predicate": "C[Y] >= C[N]",
"description": """This protocol takes a majority vote. More precisely,
it computes whether there are initially more agents
in state Y than N.""",
"statesStyle": {"Y": {"size": 1.0},
"N": {"size": 1.0},
"y": {"size": 0.5},
"n": {"size": 0.5}}
}
\ No newline at end of file
# -*- coding: utf-8 -*-
params = {
"scheme": {
"remainder": {
"descr": "Remainder c",
"values": range(0, 101),
"value": 1
},
"modulo": {
"descr": "Modulo m",
"values": range(2, 101),
"value": 2
}
}
}
def generateProtocol(params):
c = params["scheme"]["remainder"]["value"]
m = params["scheme"]["modulo"]["value"]
# Helper functions
def label(q):
if q is True:
return "y";
elif q is False:
return "f";
else:
return q
# Generate states
numeric = range(m)
boolean = [False, True]
states = numeric + boolean
# Generate transitions
transitions = []
for i in range(len(numeric)):
p = numeric[i]
for j in range(i, len(numeric)):
q = numeric[j]
pre = map(label, (p, q))
post = map(label, ((p + q) % m, ((p + q) % m) == (c % m)))
if not Utils.silent(pre, post):
transitions.append(Utils.transition(pre, post))
for j in boolean:
q = boolean[j]
pre = map(label, (p, q))
post = map(label, (p, p == (c % m)))
if not Utils.silent(pre, post):
transitions.append(Utils.transition(pre, post))
# Generate predicate
expr = ["{0}*C[{0}]".format(q) for q in numeric]
predicate = "{} %=_{} {}".format(" + ".join(expr), m, c)
# Generate style
style = {label(q): {} for q in states}
for q in numeric:
style[label(q)]["size"] = 0.5 + 0.5 * q / (m - 1)
style[label(True)]["size"] = 0.5
style[label(False)]["size"] = 0.5
style[label(True)]["color"] = "blue"
style[label(False)]["color"] = "red"
return {
"title": "Remainder protocol",
"states": map(label, states),
"transitions": transitions,
"initialStates": map(label, numeric),
"trueStates": map(label, [c % m, True]),
"predicate": predicate,
"description": """This protocol tests whether
0·C[0] + 1·C[1] + ... + (m-1)·C[m-1] ≡ c (mod m).""",
"statesStyle": style
}
# -*- coding: utf-8 -*-
params = {
"scheme": {
"minCoeff": {
"descr": "Min. coeff. a",
"values": range(-30, 31),
"value": -1
},
"maxCoeff": {
"descr": "Max. coeff. b",
"values": range(-30, 31),
"value": 1
},
"threshold": {
"descr": "Threshold c",
"values": range(1, 101),
"value": 2
}
}
}
def generateProtocol(params):
a = params["scheme"]["minCoeff"]["value"]
b = params["scheme"]["maxCoeff"]["value"]
c = params["scheme"]["threshold"]["value"]
s = max(abs(a), abs(b), abs(c) + 1)
# Helper functions
def is_leader(q):
return (q[0] == 1)
def output(q):
return (q[1] == 1)
def value(q):
return q[2]
def f(m, n):
return max(-s, min(s, m + n))
def g(m, n):
return m + n - f(m, n)
def o(m, n):
return 1 if f(m, n) < c else 0
# Generate states
states = [(x, y, u) for u in range(-s, s + 1)
for x in [0, 1] for y in [0, 1]]
# Generate transitions
transitions = []
for i in range(len(states)):
for j in range(i, len(states)):
p = states[i]
q = states[j]
if is_leader(p) or is_leader(q):
m = value(p)
n = value(q)
pre = (p, q)
post = ((1, o(m, n), f(m, n)), (0, o(m, n), g(m, n)))
t = Utils.transition(pre, post)
if (not Utils.silent(pre, post) and t not in transitions):
transitions.append(t)
# Generate initial states
initial_states = [q for q in states if is_leader(q) and
value(q) >= a and value(q) <= b and
output(q) == (value(q) < c)]
# Generate true states
true_states = [q for q in states if output(q)]
# Generate predicate
expr = ["{}*C[{}]".format(value(q), q) for q in initial_states]
predicate = "{} < {}".format(" + ".join(expr), c)
# Generate description
description = """This protocol evaluates the linear inequality
a·x_a + ... + b·x_b < c. Each state of the protocol
is of the form (l, o, v) where l is a bit indicating
whether the agent is active, o is the output of the
agent, and v is an integer indicating the value of
the agent. Described in Dana Angluin,
James Aspnes, Zoë Diamadi, Michael J. Fischer and
René Peralta. Computation in Networks of Passively
Mobile Finite-State Sensors. PODC 2004."""
# Generate style
style = {q: {} for q in states}
for q in states:
scale = (value(q) * 0.5 / s) + 0.5
style[q]["size"] = 1.0 if is_leader(q) else 0.5
if output(q):
style[q]["color"] = "rgb({}, {}, {})".format(63, int(81 + 200 * (1 - scale)),
int(100 + 81 * scale))
else:
style[q]["color"] = "rgb({}, {}, {})".format(int(105 + 128 * scale),
int(30 + 180 * (1 - scale)), 99)
return {
"title": "Threshold protocol",
"states": states,
"transitions": transitions,
"initialStates": initial_states,
"trueStates": true_states,
"predicate": predicate,
"description": description,
"statesStyle": style
}
{
"title": "Average and Conquer protocol",
"states": ["G0", "B0", "G3", "B3", "G1_1", "B1_1"],
"transitions": [
{"name": "G0, B3 -> B0, B3", "pre": ["G0", "B3"], "post": ["B0", "B3"]},
{"name": "G0, B1_1 -> B0, B1_1", "pre": ["G0", "B1_1"], "post": ["B0", "B1_1"]},
{"name": "B0, G3 -> G0, G3", "pre": ["B0", "G3"], "post": ["G0", "G3"]},
{"name": "B0, G1_1 -> G0, G1_1", "pre": ["B0", "G1_1"], "post": ["G0", "G1_1"]},
{"name": "G3, B3 -> B1_1, G1_1", "pre": ["G3", "B3"], "post": ["B1_1", "G1_1"]},
{"name": "G3, B1_1 -> G1_1, G1_1", "pre": ["G3", "B1_1"], "post": ["G1_1", "G1_1"]},
{"name": "B3, G1_1 -> B1_1, B1_1", "pre": ["B3", "G1_1"], "post": ["B1_1", "B1_1"]},
{"name": "G1_1, B1_1 -> B0, G0", "pre": ["G1_1", "B1_1"], "post": ["B0", "G0"]}
],
"initialStates": ["G3", "B3"],
"trueStates": ["G0", "G3", "G1_1"],
"initialPredicate": "G3 != B3",
"predicate": "G3 >= B3",
"precondition": "G3 != B3",
"description":
"This protocol is a fast and exact majority protocol. It computes\n
whether there are initially more agents voting yes (represented by\n
state Gm) than agents voting no (represented by state Bm). The protocol\n
does not handle ties. Parameters m and d control the running time\n
of the protocol. Described in Dan Alistarh, Rati Gelashvili,\n
Milan Vojnovi\u0107. Fast and Exact Majority in Population Protocols.\n
PODC 2015."
}
{ "title": "Broadcast Protocol", { "title": "Broadcast Protocol",
"states": ["true", "false"], "states": ["_true", "_false"],
"transitions": [{ "name": "true,false->true,true", "transitions": [{ "name": "true,false->true,true",
"pre": ["true", "false"], "pre": ["_true", "_false"],
"post": ["true", "true"] "post": ["_true", "_true"]
} }
], ],
"initialStates": ["true", "false"], "initialStates": ["_true", "_false"],
"trueStates": ["true"], "trueStates": ["_true"],
"predicate": "true >= 1" "predicate": "_true >= 1"
} }
{
"transitions": [
{
"pre": [
"AY",
"AT"
],
"post": [
"AY",
"PY"
],
"name": "x__AY__AT"
},
{
"pre": [
"AY",
"AN"
],
"post": [
"AT",
"PT"
],
"name": "x__AY__AN"
},
{
"pre": [
"AT",
"AN"
],
"post": [
"AN",
"PN"
],
"name": "x__AT__AN"
},
{
"pre": [
"AT",
"AT"
],
"post": [
"AT",
"PT"
],
"name": "x__AT__AT"
},
{
"pre": [
"AY",
"PN"
],
"post": [
"AY",
"PY"
],
"name": "x__AY__PN"
},
{
"pre": [
"AY",
"PT"
],
"post": [
"AY",
"PY"
],
"name": "x__AY__PT"
},
{
"pre": [
"AN",
"PY"
],
"post": [
"AN",
"PN"
],
"name": "x__AN__PY"
},
{
"pre": [
"AN",
"PT"
],
"post": [
"AN",
"PN"
],
"name": "x__AN__PT"
},
{
"pre": [
"AT",
"PN"
],
"post": [
"AT",
"PT"
],
"name": "x__AT__PN"
},
{
"pre": [
"AT",
"PY"
],
"post": [
"AT",
"PT"
],
"name": "x__AT__PY"
}
],
"states": [
"AY",
"AT",
"AN",
"PY",
"PT",
"PN"
],
"initialStates": [
"AY",
"AN"
],
"predicate": "AY >= AN",
"trueStates": [
"AY",
"AT",
"PY",
"PT"
],
"title": "Fast Majority Protocol"
}
...@@ -112,10 +112,10 @@ ...@@ -112,10 +112,10 @@
"_mod1", "_mod1",
"_mod2" "_mod2"
], ],
"predicate": "EXISTS k : 0 * _mod0 + 1 * _mod1 + 2 * _mod2 = 1 + 3 * k", "predicate": "0 * _mod0 + 1 * _mod1 + 2 * _mod2 =%3 1",
"trueStates": [ "trueStates": [
"_mod1", "_mod1",
"_modpassivetrue" "_modpassivetrue"
], ],
"title": "Modulo Protocol with m = 3 and c = 1" "title": "Modulo Protocol with m = 3 and c = 1"
} }
\ No newline at end of file
...@@ -23,7 +23,7 @@ executable peregrine ...@@ -23,7 +23,7 @@ executable peregrine
other-modules: other-modules:
-- other-extensions: -- other-extensions:
build-depends: base >=4 && <5, sbv, parsec >= 3.1, containers, transformers, build-depends: base >=4 && <5, sbv, parsec >= 3.1, containers, transformers,
bytestring, mtl, stm, async, parallel-io, text, aeson bytestring, mtl, stm, async, text, aeson
hs-source-dirs: src hs-source-dirs: src
default-language: Haskell2010 default-language: Haskell2010
ghc-options: -fsimpl-tick-factor=1000 -threaded -rtsopts -with-rtsopts=-N ghc-options: -fsimpl-tick-factor=1000 -threaded -rtsopts -with-rtsopts=-N -dynamic
...@@ -3,7 +3,6 @@ module Main where ...@@ -3,7 +3,6 @@ module Main where
import System.Exit import System.Exit
import System.IO import System.IO
import Control.Monad import Control.Monad
import Control.Concurrent.ParallelIO
import Control.Arrow (first) import Control.Arrow (first)
import Data.List (partition,minimumBy,genericLength) import Data.List (partition,minimumBy,genericLength)
import Data.Ord (comparing) import Data.Ord (comparing)
...@@ -23,6 +22,7 @@ import StructuralComputation ...@@ -23,6 +22,7 @@ import StructuralComputation
import Solver import Solver
import Solver.LayeredTermination import Solver.LayeredTermination
import Solver.StrongConsensus import Solver.StrongConsensus
import Solver.ReachableTermConfigInConsensus
writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO () writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO ()
writeFiles basename pp props = do writeFiles basename pp props = do
...@@ -79,9 +79,11 @@ checkProperty :: PopulationProtocol -> Property -> OptIO PropResult ...@@ -79,9 +79,11 @@ checkProperty :: PopulationProtocol -> Property -> OptIO PropResult
checkProperty pp prop = do checkProperty pp prop = do
verbosePut 1 $ "\nChecking " ++ show prop verbosePut 1 $ "\nChecking " ++ show prop
r <- case prop of r <- case prop of
LayeredTermination -> checkLayeredTermination pp LayeredTermination -> checkLayeredTermination False pp
DeterministicLayeredTermination -> checkLayeredTermination True pp
StrongConsensus -> checkStrongConsensus False pp StrongConsensus -> checkStrongConsensus False pp
StrongConsensusWithCorrectness -> checkStrongConsensus True pp StrongConsensusWithCorrectness -> checkStrongConsensus True pp
ReachableTermConfigInConsensus -> checkReachableTermConfigInConsensus pp
verbosePut 0 $ show prop ++ " " ++ show r verbosePut 0 $ show prop ++ " " ++ show r
return r return r
...@@ -93,6 +95,52 @@ printInvariant inv = do ...@@ -93,6 +95,52 @@ printInvariant inv = do
" (total of " ++ show (sum invSize) ++ ")" " (total of " ++ show (sum invSize) ++ ")"
mapM_ (putLine . show) inv mapM_ (putLine . show) inv
checkReachableTermConfigInConsensus :: PopulationProtocol -> OptIO PropResult
checkReachableTermConfigInConsensus pp = do
r <- checkReachableTermConfigInConsensus' pp ([], [])
case r of
(Nothing, _) -> return Satisfied
(Just _, _) -> return Unknown
checkReachableTermConfigInConsensus' :: PopulationProtocol -> RefinementObjects ->
OptIO (Maybe ReachableTermConfigInConsensusCounterExample, RefinementObjects)
checkReachableTermConfigInConsensus' pp refinements = do
optRefine <- opt optRefinementType
r <- checkSat $ checkReachableTermConfigInConsensusSat pp refinements
case r of
Nothing -> return (Nothing, refinements)
Just c -> do
case optRefine of
RefDefault ->
let refinementMethods = [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
in refineReachableTermConfigInConsensus pp refinementMethods refinements c
RefList refinementMethods ->
refineReachableTermConfigInConsensus pp refinementMethods refinements c
RefAll -> error "All refinement method not supported for checking reachable term config in consensus"
refineReachableTermConfigInConsensus :: PopulationProtocol -> [RefinementType] -> RefinementObjects ->
ReachableTermConfigInConsensusCounterExample ->
OptIO (Maybe ReachableTermConfigInConsensusCounterExample, RefinementObjects)
refineReachableTermConfigInConsensus _ [] refinements c = return (Just c, refinements)
refineReachableTermConfigInConsensus pp (ref:refs) refinements c = do
let refinementMethod = case ref of
TrapRefinement -> Solver.ReachableTermConfigInConsensus.findTrapConstraintsSat
SiphonRefinement -> Solver.ReachableTermConfigInConsensus.findSiphonConstraintsSat
UTrapRefinement -> Solver.ReachableTermConfigInConsensus.findUTrapConstraintsSat
USiphonRefinement -> Solver.ReachableTermConfigInConsensus.findUSiphonConstraintsSat
r <- checkSatMin $ refinementMethod pp c
case r of
Nothing -> do
refineReachableTermConfigInConsensus pp refs refinements c
Just refinement -> do
let (utraps, usiphons) = refinements
let refinements' = case ref of
TrapRefinement -> (refinement:utraps, usiphons)
SiphonRefinement -> (utraps, refinement:usiphons)
UTrapRefinement -> (refinement:utraps, usiphons)
USiphonRefinement -> (utraps, refinement:usiphons)
checkReachableTermConfigInConsensus' pp refinements'
checkStrongConsensus :: Bool -> PopulationProtocol -> OptIO PropResult checkStrongConsensus :: Bool -> PopulationProtocol -> OptIO PropResult
checkStrongConsensus checkCorrectness pp = do checkStrongConsensus checkCorrectness pp = do
r <- checkStrongConsensus' checkCorrectness pp ([], []) r <- checkStrongConsensus' checkCorrectness pp ([], [])
...@@ -147,19 +195,19 @@ refineStrongConsensus checkCorrectness pp (ref:refs) refinements c = do ...@@ -147,19 +195,19 @@ refineStrongConsensus checkCorrectness pp (ref:refs) refinements c = do
USiphonRefinement -> (utraps, refinement:usiphons) USiphonRefinement -> (utraps, refinement:usiphons)
checkStrongConsensus' checkCorrectness pp refinements' checkStrongConsensus' checkCorrectness pp refinements'
checkLayeredTermination :: PopulationProtocol -> OptIO PropResult checkLayeredTermination :: Bool -> PopulationProtocol -> OptIO PropResult
checkLayeredTermination pp = do checkLayeredTermination deterministic pp = do
let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp
checkLayeredTermination' pp nonTrivialTriplets 1 $ genericLength $ transitions pp checkLayeredTermination' deterministic pp nonTrivialTriplets 1 $ genericLength $ transitions pp
checkLayeredTermination' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult checkLayeredTermination' :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkLayeredTermination' pp triplets k kmax = do checkLayeredTermination' deterministic pp triplets k kmax = do
verbosePut 1 $ "Checking layered termination with at most " ++ show k ++ " layers" verbosePut 1 $ "Checking layered termination with at most " ++ show k ++ " layers"
r <- checkSatMin $ checkLayeredTerminationSat pp triplets k r <- checkSatMin $ checkLayeredTerminationSat deterministic pp triplets k
case r of case r of
Nothing -> Nothing ->
if k < kmax then if k < kmax then
checkLayeredTermination' pp triplets (k + 1) kmax checkLayeredTermination' deterministic pp triplets (k + 1) kmax
else else
return Unknown return Unknown
Just inv -> do Just inv -> do
...@@ -203,6 +251,4 @@ exitErrorWith msg = do ...@@ -203,6 +251,4 @@ exitErrorWith msg = do
cleanupAndExitWith $ ExitFailure 3 cleanupAndExitWith $ ExitFailure 3
cleanupAndExitWith :: ExitCode -> IO () cleanupAndExitWith :: ExitCode -> IO ()
cleanupAndExitWith code = do cleanupAndExitWith code = exitWith code
stopGlobalPool
exitWith code
{-# LANGUAGE TupleSections #-} {-# LANGUAGE TupleSections #-}
module Options module Options
(InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..), (InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),BackendSolver(..),
PropertyOption(..),Options(..),startOptions,options,parseArgs, PropertyOption(..),Options(..),startOptions,options,parseArgs,
usageInformation) usageInformation)
where where
...@@ -20,6 +20,9 @@ instance Show InputFormat where ...@@ -20,6 +20,9 @@ instance Show InputFormat where
instance Show OutputFormat where instance Show OutputFormat where
show OutDOT = "DOT" show OutDOT = "DOT"
data BackendSolver = Z3
| CVC4
data RefinementType = TrapRefinement data RefinementType = TrapRefinement
| SiphonRefinement | SiphonRefinement
| UTrapRefinement | UTrapRefinement
...@@ -37,10 +40,10 @@ data Options = Options { inputFormat :: InputFormat ...@@ -37,10 +40,10 @@ data Options = Options { inputFormat :: InputFormat
, optVerbosity :: Int , optVerbosity :: Int
, optShowHelp :: Bool , optShowHelp :: Bool
, optShowVersion :: Bool , optShowVersion :: Bool
, optSolver :: BackendSolver
, optProperties :: PropertyOption , optProperties :: PropertyOption
, optRefinementType :: RefinementOption , optRefinementType :: RefinementOption
, optMinimizeRefinement :: Int , optMinimizeRefinement :: Int
, optSMTAuto :: Bool
, optInvariant :: Bool , optInvariant :: Bool
, optOutput :: Maybe String , optOutput :: Maybe String
, outputFormat :: OutputFormat , outputFormat :: OutputFormat
...@@ -53,10 +56,10 @@ startOptions = Options { inputFormat = InPP ...@@ -53,10 +56,10 @@ startOptions = Options { inputFormat = InPP
, optVerbosity = 1 , optVerbosity = 1
, optShowHelp = False , optShowHelp = False
, optShowVersion = False , optShowVersion = False
, optSolver = Options.Z3
, optProperties = PropDefault , optProperties = PropDefault
, optRefinementType = RefDefault , optRefinementType = RefDefault
, optMinimizeRefinement = 0 , optMinimizeRefinement = 0
, optSMTAuto = True
, optInvariant = False , optInvariant = False
, optOutput = Nothing , optOutput = Nothing
, outputFormat = OutDOT , outputFormat = OutDOT
...@@ -78,6 +81,10 @@ options = ...@@ -78,6 +81,10 @@ options =
(NoArg (addProperty LayeredTermination)) (NoArg (addProperty LayeredTermination))
"Prove that the protocol satisfies layered termination" "Prove that the protocol satisfies layered termination"
, Option "" ["deterministic-layered-termination"]
(NoArg (addProperty DeterministicLayeredTermination))
"Prove that the protocol satisfies deterministic layered termination"
, Option "" ["strong-consensus"] , Option "" ["strong-consensus"]
(NoArg (addProperty StrongConsensus)) (NoArg (addProperty StrongConsensus))
"Prove that the protocol satisfies strong consensus" "Prove that the protocol satisfies strong consensus"
...@@ -86,10 +93,24 @@ options = ...@@ -86,10 +93,24 @@ options =
(NoArg (addProperty StrongConsensusWithCorrectness)) (NoArg (addProperty StrongConsensusWithCorrectness))
"Prove that the protocol correctly satisfies the given predicate" "Prove that the protocol correctly satisfies the given predicate"
, Option "" ["terminal-consensus"]
(NoArg (addProperty ReachableTermConfigInConsensus))
"Prove that reachable terminal configurations are in consensus"
, Option "i" ["invariant"] , Option "i" ["invariant"]
(NoArg (\opt -> Right opt { optInvariant = True })) (NoArg (\opt -> Right opt { optInvariant = True }))
"Generate an invariant" "Generate an invariant"
, Option "" ["solver"]
(ReqArg (\arg opt ->
case arg of
"z3" -> Right opt { optSolver = Options.Z3 }
"cvc4" -> Right opt { optSolver = Options.CVC4 }
_ -> Left ("invalid argument for refinement method: " ++ arg)
)
"SOLVER")
("Use backend solver SOLVER (z3, cvc4)")
, Option "r" ["refinement"] , Option "r" ["refinement"]
(ReqArg (\arg opt -> (ReqArg (\arg opt ->
let addRef ref = let addRef ref =
...@@ -143,10 +164,6 @@ options = ...@@ -143,10 +164,6 @@ options =
"METHOD") "METHOD")
"Minimize size of refinement structure by method METHOD (1-4)" "Minimize size of refinement structure by method METHOD (1-4)"
, Option "" ["smt-disable-auto-config"]
(NoArg (\opt -> Right opt { optSMTAuto = False }))
"Disable automatic configuration of the SMT solver"
, Option "v" ["verbose"] , Option "v" ["verbose"]
(NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 })) (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
"Increase verbosity (may be specified more than once)" "Increase verbosity (may be specified more than once)"
......
...@@ -17,6 +17,6 @@ parseString p str = ...@@ -17,6 +17,6 @@ parseString p str =
parseFile :: Parser a -> String -> IO a parseFile :: Parser a -> String -> IO a
parseFile p file = do parseFile p file = do
contents <- T.unpack <$> TIO.readFile file contents <- T.unpack <$> TIO.readFile file
case parse p file contents of case parse p file contents of
Left e -> print e >> fail "parse error" Left e -> print e >> fail "parse error"
Right r -> return r Right r -> return r
...@@ -6,7 +6,7 @@ module Parser.PP ...@@ -6,7 +6,7 @@ module Parser.PP
(parseContent) (parseContent)
where where
import Data.Aeson import Data.Aeson (FromJSON, ToJSON, toJSON, parseJSON, Value(String), eitherDecode)
import Data.Aeson.TH (deriveJSON, defaultOptions) import Data.Aeson.TH (deriveJSON, defaultOptions)
import Control.Applicative ((<*),(*>),(<$>)) import Control.Applicative ((<*),(*>),(<$>))
import Data.Functor.Identity import Data.Functor.Identity
...@@ -30,10 +30,10 @@ languageDef = ...@@ -30,10 +30,10 @@ languageDef =
Token.identStart = letter <|> char '_', Token.identStart = letter <|> char '_',
Token.identLetter = alphaNum <|> char '_', Token.identLetter = alphaNum <|> char '_',
Token.reservedNames = ["true", "false", "EXISTS", "FORALL"], Token.reservedNames = ["true", "false", "EXISTS", "FORALL"],
Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">", Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">", "=%", "!=%",
"+", "-", "*", "&&", "||", "!", ":"] "+", "-", "*", "&&", "||", "!", ":"]
} }
lexer :: Token.TokenParser () lexer :: Token.TokenParser ()
lexer = Token.makeTokenParser languageDef lexer = Token.makeTokenParser languageDef
...@@ -103,14 +103,16 @@ parseOp = (reservedOp "<" *> return Lt) <|> ...@@ -103,14 +103,16 @@ parseOp = (reservedOp "<" *> return Lt) <|>
(reservedOp "=" *> return Eq) <|> (reservedOp "=" *> return Eq) <|>
(reservedOp "!=" *> return Ne) <|> (reservedOp "!=" *> return Ne) <|>
(reservedOp ">" *> return Gt) <|> (reservedOp ">" *> return Gt) <|>
(reservedOp ">=" *> return Ge) (reservedOp ">=" *> return Ge) <|>
(reservedOp "=%" *> (ModEq <$> integer)) <|>
(reservedOp "!=%" *> (ModNe <$> integer))
linIneq :: Parser (Formula String) equation :: Parser (Formula String)
linIneq = do equation = do
lhs <- term lhs <- term
op <- parseOp op <- parseOp
rhs <- term rhs <- term
return (LinearInequation lhs op rhs) return (Equation lhs op rhs)
formOperatorTable :: [[Operator String () Identity (Formula String)]] formOperatorTable :: [[Operator String () Identity (Formula String)]]
formOperatorTable = formOperatorTable =
...@@ -120,7 +122,7 @@ formOperatorTable = ...@@ -120,7 +122,7 @@ formOperatorTable =
] ]
formAtom :: Parser (Formula String) formAtom :: Parser (Formula String)
formAtom = try linIneq formAtom = try equation
<|> (reserved "true" *> return FTrue) <|> (reserved "true" *> return FTrue)
<|> (reserved "false" *> return FFalse) <|> (reserved "false" *> return FFalse)
<|> parens formula <|> parens formula
...@@ -129,27 +131,15 @@ formAtom = try linIneq ...@@ -129,27 +131,15 @@ formAtom = try linIneq
formula :: Parser (Formula String) formula :: Parser (Formula String)
formula = buildExpressionParser formOperatorTable formAtom <?> "formula" formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
quantFormula :: Parser (QuantFormula String) instance FromJSON (Formula String) where
quantFormula =
(do
reserved "EXISTS"
xs <- optionalCommaSep ident
reservedOp ":"
p <- formula
return (ExQuantFormula xs p)
)
<|>
(ExQuantFormula [] <$> formula)
instance FromJSON (QuantFormula String) where
parseJSON (String v) = do parseJSON (String v) = do
let formula = parse quantFormula "" (T.unpack v) let f = parse formula "" (T.unpack v)
case formula of case f of
Left e -> fail "Predicate formula not well-formed." Left e -> fail "Predicate formula not well-formed."
Right r -> return r Right r -> return r
parseJSON _ = fail "Expect string for predicate." parseJSON _ = fail "Expect string for predicate."
instance ToJSON (QuantFormula String) where instance ToJSON (Formula String) where
toJSON x = String "" toJSON x = String ""
data RecordTransition = RecordTransition { data RecordTransition = RecordTransition {
...@@ -164,7 +154,8 @@ data RecordPP = RecordPP { ...@@ -164,7 +154,8 @@ data RecordPP = RecordPP {
transitions :: [RecordTransition], transitions :: [RecordTransition],
initialStates :: [String], initialStates :: [String],
trueStates :: [String], trueStates :: [String],
predicate :: Maybe (QuantFormula String), precondition :: Maybe (Formula String),
predicate :: Maybe (Formula String),
description :: Maybe String description :: Maybe String
} deriving (Show) } deriving (Show)
...@@ -172,20 +163,22 @@ $(deriveJSON defaultOptions ''RecordTransition) ...@@ -172,20 +163,22 @@ $(deriveJSON defaultOptions ''RecordTransition)
$(deriveJSON defaultOptions ''RecordPP) $(deriveJSON defaultOptions ''RecordPP)
recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol
recordPP2PopulationProtocol r = recordPP2PopulationProtocol r =
makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p arcs where makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p precond arcs where
falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))] falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))]
arcs = [(q, name t, 1) | t <- transitions r, q <- pre t] ++ arcs = [(q, name t, 1) | t <- transitions r, q <- pre t] ++
[(name t, q, 1) | t <- transitions r, q <- post t] [(name t, q, 1) | t <- transitions r, q <- post t]
p = case predicate r of Nothing -> ExQuantFormula [] FTrue p = case predicate r of Nothing -> FTrue
(Just p') -> p' (Just p') -> p'
precond = case precondition r of Nothing -> FTrue
(Just p') -> p'
parseContent :: Parser PopulationProtocol parseContent :: Parser PopulationProtocol
parseContent = do parseContent = do
str <- manyTill anyChar eof str <- manyTill anyChar eof
let r = eitherDecode (BS.pack str) let r = eitherDecode (BS.pack str)
case r of case r of
(Left e) -> fail e (Left e) -> fail e
(Right pp) -> return (recordPP2PopulationProtocol pp) (Right pp) -> return (recordPP2PopulationProtocol pp)
...@@ -6,7 +6,7 @@ module PopulationProtocol ...@@ -6,7 +6,7 @@ module PopulationProtocol
Configuration,FlowVector,RConfiguration,RFlowVector, Configuration,FlowVector,RConfiguration,RFlowVector,
renameState,renameTransition,renameStatesAndTransitions, renameState,renameTransition,renameStatesAndTransitions,
invertPopulationProtocol, invertPopulationProtocol,
name,showNetName,states,transitions,initialStates,trueStates,falseStates,predicate, name,showNetName,states,transitions