...
 
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
build:
cabal install --only-dependencies
cabal build
install:
......
......@@ -11,6 +11,11 @@ echo "generating majority protocol"
mkdir -p $benchmark_dir/$protocols_dir/majority
$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
echo "generating broadcast protocol"
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
done
done
# modulo
echo "generating modulo protocols"
mkdir -p $benchmark_dir/$protocols_dir/modulo
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
# Remainder
echo "generating remainder protocols"
mkdir -p $benchmark_dir/$protocols_dir/remainder
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
$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
# flock of birds
# Flock of Birds from Chatzigianniks, Michail, Spirakis: Algorithmic verification of population protocols
echo "generating flockofbirds protocols"
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
done
# new birds
# new birds from Clément, Delporte-Gallet, Fauconnier, Sighireanu: Guidelines for the verification of population protocols
echo "generating newbirds protocols"
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
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:
print("unknown argument: %s" % arg, file=sys.stderr)
sys.exit(-1)
else:
results_file = sys.argv[1]
results_file = arg
# long table
......@@ -136,7 +136,6 @@ if long_table:
# short table
if short_table:
results_file='results.csv'
results = pd.read_csv(results_file)
......
......@@ -21,6 +21,7 @@ executable pp-print
main-is: Main.hs
other-modules:
-- 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
default-language: Haskell2010
ghc-options: -dynamic
module PopulationProtocol ( PopulationProtocol (..)
, Population
, createModuloProtocol
, createThresholdProtocol
, createOldThresholdProtocol
......@@ -18,7 +17,6 @@ module PopulationProtocol ( PopulationProtocol (..)
import Util
import qualified Data.Set as S
import qualified Data.MultiSet as MS
import qualified Data.Map.Strict as M
import Data.Tuple (swap)
import Data.List (intercalate, nub)
......@@ -47,8 +45,6 @@ type FlockOfBirdsProtocol = PopulationProtocol 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 SimpleState = L Int | NL Int deriving (Ord, Eq, Show)
......@@ -283,9 +279,9 @@ createModuloProtocol n c = PopulationProtocol { states = [Mod i | i <- [0..(n-1)
modOpinion (Mod a) = a == c
modOpinion (ModPassive b) = b
modPredicate = "EXISTS k : " ++
modPredicate = "( " ++
(intercalate " + " [ show i ++ " * " ++ toVar (Mod i) | i <- [0..(n-1)] ]) ++
" = " ++ show c ++ " + " ++ show n ++ " * k"
" ) =% " ++ show n ++ " " ++ show c
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",
"states": ["true", "false"],
"states": ["_true", "_false"],
"transitions": [{ "name": "true,false->true,true",
"pre": ["true", "false"],
"post": ["true", "true"]
"pre": ["_true", "_false"],
"post": ["_true", "_true"]
}
],
"initialStates": ["true", "false"],
"trueStates": ["true"],
"predicate": "true >= 1"
"initialStates": ["_true", "_false"],
"trueStates": ["_true"],
"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,7 +112,7 @@
"_mod1",
"_mod2"
],
"predicate": "EXISTS k : 0 * _mod0 + 1 * _mod1 + 2 * _mod2 = 1 + 3 * k",
"predicate": "0 * _mod0 + 1 * _mod1 + 2 * _mod2 =%3 1",
"trueStates": [
"_mod1",
"_modpassivetrue"
......
......@@ -23,7 +23,7 @@ executable peregrine
other-modules:
-- other-extensions:
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
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
import System.Exit
import System.IO
import Control.Monad
import Control.Concurrent.ParallelIO
import Control.Arrow (first)
import Data.List (partition,minimumBy,genericLength)
import Data.Ord (comparing)
......@@ -23,6 +22,7 @@ import StructuralComputation
import Solver
import Solver.LayeredTermination
import Solver.StrongConsensus
import Solver.ReachableTermConfigInConsensus
writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO ()
writeFiles basename pp props = do
......@@ -79,9 +79,11 @@ checkProperty :: PopulationProtocol -> Property -> OptIO PropResult
checkProperty pp prop = do
verbosePut 1 $ "\nChecking " ++ show prop
r <- case prop of
LayeredTermination -> checkLayeredTermination pp
LayeredTermination -> checkLayeredTermination False pp
DeterministicLayeredTermination -> checkLayeredTermination True pp
StrongConsensus -> checkStrongConsensus False pp
StrongConsensusWithCorrectness -> checkStrongConsensus True pp
ReachableTermConfigInConsensus -> checkReachableTermConfigInConsensus pp
verbosePut 0 $ show prop ++ " " ++ show r
return r
......@@ -93,6 +95,52 @@ printInvariant inv = do
" (total of " ++ show (sum invSize) ++ ")"
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 checkCorrectness pp = do
r <- checkStrongConsensus' checkCorrectness pp ([], [])
......@@ -147,19 +195,19 @@ refineStrongConsensus checkCorrectness pp (ref:refs) refinements c = do
USiphonRefinement -> (utraps, refinement:usiphons)
checkStrongConsensus' checkCorrectness pp refinements'
checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
checkLayeredTermination pp = do
checkLayeredTermination :: Bool -> PopulationProtocol -> OptIO PropResult
checkLayeredTermination deterministic pp = do
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' pp triplets k kmax = do
checkLayeredTermination' :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkLayeredTermination' deterministic pp triplets k kmax = do
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
Nothing ->
if k < kmax then
checkLayeredTermination' pp triplets (k + 1) kmax
checkLayeredTermination' deterministic pp triplets (k + 1) kmax
else
return Unknown
Just inv -> do
......@@ -203,6 +251,4 @@ exitErrorWith msg = do
cleanupAndExitWith $ ExitFailure 3
cleanupAndExitWith :: ExitCode -> IO ()
cleanupAndExitWith code = do
stopGlobalPool
exitWith code
cleanupAndExitWith code = exitWith code
{-# LANGUAGE TupleSections #-}
module Options
(InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),
(InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),BackendSolver(..),
PropertyOption(..),Options(..),startOptions,options,parseArgs,
usageInformation)
where
......@@ -20,6 +20,9 @@ instance Show InputFormat where
instance Show OutputFormat where
show OutDOT = "DOT"
data BackendSolver = Z3
| CVC4
data RefinementType = TrapRefinement
| SiphonRefinement
| UTrapRefinement
......@@ -37,10 +40,10 @@ data Options = Options { inputFormat :: InputFormat
, optVerbosity :: Int
, optShowHelp :: Bool
, optShowVersion :: Bool
, optSolver :: BackendSolver
, optProperties :: PropertyOption
, optRefinementType :: RefinementOption
, optMinimizeRefinement :: Int
, optSMTAuto :: Bool
, optInvariant :: Bool
, optOutput :: Maybe String
, outputFormat :: OutputFormat
......@@ -53,10 +56,10 @@ startOptions = Options { inputFormat = InPP
, optVerbosity = 1
, optShowHelp = False
, optShowVersion = False
, optSolver = Options.Z3
, optProperties = PropDefault
, optRefinementType = RefDefault
, optMinimizeRefinement = 0
, optSMTAuto = True
, optInvariant = False
, optOutput = Nothing
, outputFormat = OutDOT
......@@ -78,6 +81,10 @@ options =
(NoArg (addProperty LayeredTermination))
"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"]
(NoArg (addProperty StrongConsensus))
"Prove that the protocol satisfies strong consensus"
......@@ -86,10 +93,24 @@ options =
(NoArg (addProperty StrongConsensusWithCorrectness))
"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"]
(NoArg (\opt -> Right opt { optInvariant = True }))
"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"]
(ReqArg (\arg opt ->
let addRef ref =
......@@ -143,10 +164,6 @@ options =
"METHOD")
"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"]
(NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
"Increase verbosity (may be specified more than once)"
......
......@@ -6,7 +6,7 @@ module Parser.PP
(parseContent)
where
import Data.Aeson
import Data.Aeson (FromJSON, ToJSON, toJSON, parseJSON, Value(String), eitherDecode)
import Data.Aeson.TH (deriveJSON, defaultOptions)
import Control.Applicative ((<*),(*>),(<$>))
import Data.Functor.Identity
......@@ -30,7 +30,7 @@ languageDef =
Token.identStart = letter <|> char '_',
Token.identLetter = alphaNum <|> char '_',
Token.reservedNames = ["true", "false", "EXISTS", "FORALL"],
Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">", "=%", "!=%",
"+", "-", "*", "&&", "||", "!", ":"]
}
......@@ -103,14 +103,16 @@ parseOp = (reservedOp "<" *> return Lt) <|>
(reservedOp "=" *> return Eq) <|>
(reservedOp "!=" *> return Ne) <|>
(reservedOp ">" *> return Gt) <|>
(reservedOp ">=" *> return Ge)
(reservedOp ">=" *> return Ge) <|>
(reservedOp "=%" *> (ModEq <$> integer)) <|>
(reservedOp "!=%" *> (ModNe <$> integer))
linIneq :: Parser (Formula String)
linIneq = do
equation :: Parser (Formula String)
equation = do
lhs <- term
op <- parseOp
rhs <- term
return (LinearInequation lhs op rhs)
return (Equation lhs op rhs)
formOperatorTable :: [[Operator String () Identity (Formula String)]]
formOperatorTable =
......@@ -120,7 +122,7 @@ formOperatorTable =
]
formAtom :: Parser (Formula String)
formAtom = try linIneq
formAtom = try equation
<|> (reserved "true" *> return FTrue)
<|> (reserved "false" *> return FFalse)
<|> parens formula
......@@ -129,27 +131,15 @@ formAtom = try linIneq
formula :: Parser (Formula String)
formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
quantFormula :: Parser (QuantFormula String)
quantFormula =
(do
reserved "EXISTS"
xs <- optionalCommaSep ident
reservedOp ":"
p <- formula
return (ExQuantFormula xs p)
)
<|>
(ExQuantFormula [] <$> formula)
instance FromJSON (QuantFormula String) where
instance FromJSON (Formula String) where
parseJSON (String v) = do
let formula = parse quantFormula "" (T.unpack v)
case formula of
let f = parse formula "" (T.unpack v)
case f of
Left e -> fail "Predicate formula not well-formed."
Right r -> return r
parseJSON _ = fail "Expect string for predicate."
instance ToJSON (QuantFormula String) where
instance ToJSON (Formula String) where
toJSON x = String ""
data RecordTransition = RecordTransition {
......@@ -164,7 +154,8 @@ data RecordPP = RecordPP {
transitions :: [RecordTransition],
initialStates :: [String],
trueStates :: [String],
predicate :: Maybe (QuantFormula String),
precondition :: Maybe (Formula String),
predicate :: Maybe (Formula String),
description :: Maybe String
} deriving (Show)
......@@ -173,11 +164,13 @@ $(deriveJSON defaultOptions ''RecordPP)
recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol
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)))]
arcs = [(q, name t, 1) | t <- transitions r, q <- pre 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'
precond = case precondition r of Nothing -> FTrue
(Just p') -> p'
parseContent :: Parser PopulationProtocol
......
......@@ -6,7 +6,7 @@ module PopulationProtocol
Configuration,FlowVector,RConfiguration,RFlowVector,
renameState,renameTransition,renameStatesAndTransitions,
invertPopulationProtocol,
name,showNetName,states,transitions,initialStates,trueStates,falseStates,predicate,
name,showNetName,states,transitions,initialStates,trueStates,falseStates,predicate,precondition,
pre,lpre,post,lpost,mpre,mpost,context,
makePopulationProtocol,makePopulationProtocolWithTrans,
makePopulationProtocolFromStrings,makePopulationProtocolWithTransFromStrings,
......@@ -77,7 +77,8 @@ data PopulationProtocol = PopulationProtocol {
initialStates :: [State],
trueStates :: [State],
falseStates :: [State],
predicate :: QuantFormula State,
predicate :: Formula State,
precondition :: Formula State,
adjacencyQ :: M.Map State ([(Transition,Integer)], [(Transition,Integer)]),
adjacencyT :: M.Map Transition ([(State,Integer)], [(State,Integer)])
}
......@@ -94,6 +95,7 @@ instance Show PopulationProtocol where
"\nTrue states : " ++ show (trueStates pp) ++
"\nFalse states : " ++ show (falseStates pp) ++
"\nPredicate : " ++ show (predicate pp) ++
"\nPrecondition : " ++ show (precondition pp) ++
"\nState arcs :\n" ++ unlines
(map showContext (M.toList (adjacencyQ pp))) ++
"\nTransition arcs:\n" ++ unlines
......@@ -123,6 +125,8 @@ renameStatesAndTransitions f pp =
listSet $ map (renameState f) $ falseStates pp,
predicate =
fmap (renameState f) $ predicate pp,
precondition =
fmap (renameState f) $ precondition pp,
adjacencyQ = mapAdjacency (renameState f) (renameTransition f) $
adjacencyQ pp,
adjacencyT = mapAdjacency (renameTransition f) (renameState f) $
......@@ -142,6 +146,7 @@ invertPopulationProtocol pp =
trueStates = trueStates pp,
falseStates = falseStates pp,
predicate = predicate pp,
precondition = precondition pp,
adjacencyQ = M.map swap $ adjacencyQ pp,
adjacencyT = M.map swap $ adjacencyT pp
}
......@@ -149,10 +154,10 @@ invertPopulationProtocol pp =
makePopulationProtocol :: String -> [State] -> [Transition] ->
[State] -> [State] -> [State] -> QuantFormula State ->
[State] -> [State] -> [State] -> Formula State -> Formula State ->
[Either (Transition, State, Integer) (State, Transition, Integer)] ->
PopulationProtocol
makePopulationProtocol name states transitions initialStates trueStates falseStates predicate arcs =
makePopulationProtocol name states transitions initialStates trueStates falseStates predicate precondition arcs =
PopulationProtocol {
name = name,
states = listSet states,
......@@ -161,6 +166,7 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
trueStates = listSet trueStates,
falseStates = listSet falseStates,
predicate = predicate,
precondition = precondition,
adjacencyQ = M.map (listMap *** listMap) adQ,
adjacencyT = M.map (listMap *** listMap) adT
}
......@@ -183,8 +189,8 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
makePopulationProtocolFromStrings :: String -> [String] -> [String] -> [String] -> [String] -> [String] ->
QuantFormula String -> [(String, String, Integer)] -> PopulationProtocol
makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates predicate arcs =
Formula String -> Formula String -> [(String, String, Integer)] -> PopulationProtocol
makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates predicate precondition arcs =
makePopulationProtocol
name
(map State (S.toAscList stateSet))
......@@ -193,6 +199,7 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
(map State trueStates)
(map State falseStates)
(fmap State predicate)
(fmap State precondition)
(map toEitherArc arcs)
where
stateSet = S.fromList states
......@@ -217,18 +224,18 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
error $ l ++ " and " ++ r ++ " both transitions"
makePopulationProtocolWithTrans :: String -> [State] -> [State] -> [State] -> [State] ->
QuantFormula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] ->
Formula State -> Formula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] ->
PopulationProtocol
makePopulationProtocolWithTrans name states initialStates trueStates falseStates predicate ts =
makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates predicate arcs
makePopulationProtocolWithTrans name states initialStates trueStates falseStates predicate precondition ts =
makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates predicate precondition arcs
where
arcs = [ Right (q,t,w) | (t,(is,_)) <- ts, (q,w) <- is ] ++
[ Left (t,q,w) | (t,(_,os)) <- ts, (q,w) <- os ]
makePopulationProtocolWithTransFromStrings :: String -> [String] -> [String] -> [String] -> [String] ->
QuantFormula String -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
Formula String -> Formula String -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
PopulationProtocol
makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates predicate arcs =
makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates predicate precondition arcs =
makePopulationProtocolWithTrans
name
(map State states)
......@@ -236,6 +243,7 @@ makePopulationProtocolWithTransFromStrings name states initialStates trueStates
(map State trueStates)
(map State falseStates)
(fmap State predicate)
(fmap State precondition)
(map toTArc arcs)
where
toTArc (t, (iq, oq)) =
......