Add more protocols for benchmarking

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/fast_majority
+cp ../examples/fast_majority.pp $benchmark_dir/$protocols_dir/fast_majority/fast_majority_m1_.pp
+
 # broadcast
 echo "generating broadcast protocol"
 mkdir -p $benchmark_dir/$protocols_dir/broadcast
@@ -25,25 +30,37 @@ 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
+# Remainder
+echo "generating remainder protocols"
+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 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
     $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
     $executable newBirdsPP $c >$benchmark_dir/$protocols_dir/newbirds/newbirds_c${c}_.pp
 done
+
+# Logarithmic Flock of Birds
+mkdir -p $benchmark_dir/$protocols_dir/logflockofbirds
+for c in 10 100 1000 10000 100000 1000000 10000000 100000000 1000000000; do
+    python python/execprotocol.py python/flock_log.py "{\"scheme\": { \"threshold\": { \"value\": ${c} } } }" >$benchmark_dir/$protocols_dir/logflockofbirds/logflockofbirds_c${c}_.pp
+done
+
+# Tower Flock of Birds
+mkdir -p $benchmark_dir/$protocols_dir/towerflockofbirds
+for c in 10 15 20 25 30 35 40 45 50 55 60 65 70 75 80 85 90 95 100; 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

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