Bounded Retransmission Protocol (BRP) and Rabin Mutual Exclusion Protocol

data/brp.py

@@ -0,0 +1,55 @@
+"""
+probprogs benchmark | brp.py
+
+A variant of the bounded retransmission protocol (BRP). Tries to send `toSend`
+number of packets via an unreliable channel. At most `maxFail` retransmissions
+are attempted. `totalFail` marks the total number of failed attempts to send a
+packet.
+
+Leen Helmink, M. P. A. Sellink, Frits W. Vaandrager:
+Proof-Checking a Data Link Protocol. TYPES 1993.
+"""
+import numpy as np
+import time
+from scipy.stats import bernoulli
+
+np.random.seed(int(time.time()))
+
+def brp(toSend: uint, maxFailed: uint) -> uint:
+    """
+    Properties:
+        - send4
+            type: uexp
+            post: totalFailed
+            pre: "[toSend <= 4] * (totalFailed + 1) + [toSend > 4] * \infty"
+        - send10
+            type: uexp
+            post: totalFailed
+            pre: "[toSend <= 10] * (totalFailed + 1) + [toSend > 10] * \infty"
+    """
+    sent: uint = 0
+    failed: uint = 0
+    totalFailed: uint = 0
+
+    while failed < maxFailed and sent < toSend:
+        """
+        Hints:
+            - send4:
+                k-induction:
+                    invariant: "[toSend <= 4] * (totalFailed + 1) + [toSend > 4] * \infty"
+                    k: 5
+            - send10:
+                k-induction:
+                    invariant: "[toSend <= 10] * (totalFailed + 1) + [toSend > 10] * \infty"
+                    k: 11
+        """
+        if bernoulli(0.1).rvs():
+            # successful transmission of current packet
+            failed = 0
+            sent = sent + 1
+        else:
+            # failed transmission of current packet
+            failed = failed + 1
+            totalFailed = totalFailed + 1
+
+    return totalFailed

data/geometric.py

@@ -18,10 +18,8 @@
 x = 1 
 
 while x == 1:
-    """
-    HeyVL.invariant: "...." 
-    """
-    Annotate.HeyVL(" .... ")
+    Annotate ("HeyVL.invariant", "....")
+    Annotate("HeyVL", " .... ")
     if bernoulli(0.5).rvs(): 
         x = 0 
     else: 

data/rabin.py

@@ -0,0 +1,40 @@
+"""
+probprogs benchmark | rabin.py
+
+A variant of Rabin's mutual exclusion protocol [1] taken from [2]. We verify
+that the probability of successfully selecting a unique winning process as at
+least 2/3, independently of how many processes are contending for ownership of
+the mutex.
+
+[1]: Eyal Kushilevitz, Michael O. Rabin: Randomized Mutual Exclusion Algorithms Revisited.
+[2]: Joe Hurd, Annabelle McIver, Carroll Morgan: Probabilistic Guarded Commands Mechanized in HOL. QAPL 2004.
+"""
+import numpy as np
+import time
+from scipy.stats import bernoulli
+
+np.random.seed(int(time.time()))
+
+def rabin(i: uint, n: uint) -> bool:
+    """
+    Properties:
+        - successprob
+            type: lexp
+            post: [success]
+            pre: "[1 == i] + [1 > i] * (2/3)"
+    """
+    while 1 < i:
+        """
+        Hints:
+            - successprob:
+                induction:
+                    invariant: "([(0 <= n) && (n <= i)]) * (((2/3) * (1 - ((([i == n] * (n + 1)) * (2 ** -n)) + ([i == (n + 1)] * (2 ** -n))))) + ((([i == n] * n) * (2 ** -n)) + ([i == (n + 1)] * (2 ** -n))))"
+        """
+        n = i
+        while 0 < n:
+            d = 0 if bernoulli(0.5).rvs() else 1
+            i = i - d
+            n = n - 1
+
+    success: bool = i == 1
+    return success