.gitlab-ci.yml

+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

Makefile

 all: build
 
 build:
+	cabal install --only-dependencies
 	cabal build
 
 install:

benchmarks/generate_protocols.sh

@@ -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

benchmarks/make_table.py

@@ -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)
 

benchmarks/pp-print/pp-print.cabal

@@ -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

benchmarks/pp-print/src/PopulationProtocol.hs

 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

benchmarks/python/avc.py

+# -*- 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()
+  }

benchmarks/python/broadcast.py

+# 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

benchmarks/python/execprotocol.py

+#!/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))

benchmarks/python/flock_log.py

+# -*- 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
+  }

benchmarks/python/flock_of_birds_-_tower.py

+# -*- 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

benchmarks/python/majority_basic.py

+# 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

benchmarks/python/remainder.py

+# -*- 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
+  }

benchmarks/python/threshold.py

+# -*- 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
+  }

examples/averageandconquer.pp

+{
+    "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."
+}

examples/broadcast.pp

 { "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"
 }

examples/fastmajority.pp

+{
+    "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"
+}

examples/remainder_m3_c1.pp

@@ -112,10 +112,10 @@
         "_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"
     ],
     "title": "Modulo Protocol with m = 3 and c = 1"
-}
\ No newline at end of file
+}

peregrine.cabal

@@ -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

src/Main.hs

@@ -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

src/Options.hs

 {-# 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)"

src/Parser.hs

@@ -17,6 +17,6 @@ parseString p str =
 parseFile :: Parser a -> String -> IO a
 parseFile p file =  do
         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"
             Right r -> return r

src/Parser/PP.hs

@@ -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,10 +30,10 @@ languageDef =
                  Token.identStart      = letter <|> char '_',
                  Token.identLetter     = alphaNum <|> char '_',
                  Token.reservedNames   = ["true", "false", "EXISTS", "FORALL"],
-                 Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
+                 Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">", "=%", "!=%",
                                           "+", "-", "*", "&&", "||", "!", ":"]
                  }
- 
+
 lexer :: Token.TokenParser ()
 lexer = Token.makeTokenParser languageDef
 
@@ -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)
 
@@ -172,20 +163,22 @@ $(deriveJSON defaultOptions ''RecordTransition)
 $(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
+recordPP2PopulationProtocol r =
+  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] ++ 
+        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
-parseContent  = do 
+parseContent  = do
   str <- manyTill anyChar eof
   let r = eitherDecode (BS.pack str)
   case r of
     (Left e) ->  fail e
     (Right pp) -> return (recordPP2PopulationProtocol pp)
- 
+
 

src/PopulationProtocol.hs

@@ -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