Add ewd426

README.md

@@ -102,6 +102,7 @@ Do you have your own case study that you like to share with the community? Send
 | 89 | The Streamlet consensus algorithm | <a href="https://www.losa.fr/blog/streamlet-in-tla+">Specification and model-checking of both safety and liveness properties of Streamlet with TLC</a> | Giuliano Losa | | &#10004; | Sequences, Integers, FiniteSets | &#10004; | |
 | 90 | Petri Nets | <a href="https://github.com/elh/petri-tlaplus">Instantiable Petri Nets with liveness properties</a> | Eugene Huang | | &#10004; | Integers, Sequences, FiniteSets, TLC | |
 | 91 | Knuth Yao & Markov Chains | <a href="specifications/KnuthYao">Knuth-Yao algorithm for simulating a sixsided die</a> | Ron Pressler, Markus Kuppe | | &#10004; | DyadicRationals | |
+| 92 | ewd426 - Token Stabilization | <a href="specifications/ewd426">Self-stabilizing systems in spite of distributed control</a> | Murat Demirbas, Markus Kuppe | | &#10004; | Naturals, FiniteSets | |
 
 ## License
 

specifications/ewd426/SimTokenRing.cfg

@@ -0,0 +1,25 @@
+CONSTANTS
+    N = 7
+    M = 7
+
+\* Relevant for statistics only! Exhaustive model
+\* checking will *not* work with  AtStabilazation
+\* because it evaluates to false  UniqueToken  is
+\* true. 
+CONSTRAINTS 
+    AtStabilization
+
+CHECK_DEADLOCK
+    FALSE
+
+SPECIFICATION 
+    Spec
+
+INVARIANT
+    TypeOK
+
+\* TLC will report a (bogus) violation of  Stab  in 
+\* "generate" or "simulate" mode, due to the way these
+\* modes work.
+\* PROPERTIES 
+\*     Stab

specifications/ewd426/SimTokenRing.tla

@@ -0,0 +1,27 @@
+-------------------------------- MODULE SimTokenRing -------------------------------
+EXTENDS TokenRing, TLC, CSV, IOUtils
+
+(* Statistics collection *)
+
+CSVFile ==
+    "SimTokenRing.csv"
+
+ASSUME
+    \* Initialize the CSV file with a header.
+    /\ CSVRecords(CSVFile) = 0 => CSVWrite("steps", <<>>, CSVFile)
+
+AtStabilization == 
+    \* State constraint at cfg
+    UniqueToken => 
+        /\ CSVWrite("%1$s", <<TLCGet("level")>>,CSVFile)
+        /\ TLCGet("stats").traces % 250 = 0 =>
+            /\ IOExec(<<"/usr/bin/env", "Rscript", "SimTokenRing.R", CSVFile>>).exitValue = 0        
+        /\ FALSE \* to make TLC simulate the next behavior one the system stabilizes.
+
+=======================================================================================
+$ rm -rf states/ ; rm *.csv ; tlc SimTokenRing -note -generate -depth -1
+
+
+
+$ alias tlc
+tlc='java -cp /path/to/tla2tools.jar tlc2.TLC'

specifications/ewd426/TokenRing.cfg

@@ -0,0 +1,18 @@
+CONSTANTS
+    N = 6
+    M = 6
+
+CHECK_DEADLOCK
+    FALSE
+
+SPECIFICATION 
+    Spec
+
+INVARIANT
+    TypeOK
+
+PROPERTIES 
+    Stab
+
+ALIAS
+    Alias

specifications/ewd426/TokenRing.tla

@@ -0,0 +1,63 @@
+--------------------------------- MODULE TokenRing ---------------------------------
+(***********************************************************************************)
+(* Dijkstra's classical stabilizing token ring algorithm: EWD426                   *)
+(* https://muratbuffalo.blogspot.com/2015/01/dijkstras-stabilizing-token-ring.html *)
+(***********************************************************************************)
+EXTENDS Naturals, FiniteSets
+
+CONSTANTS  N, M
+ASSUME NAssumption == N \in Nat \ {0} \* At least one node
+ASSUME MAssumption == M \in Nat \ {0} \* Value domain of c 
+
+ASSUME NMAssumption == N <= M + 1
+
+Node == 0 .. N-1
+
+VARIABLES 
+    c   \* counter at each node, token is defined as function of c's in nbring nodes
+
+vars == << c >>    
+
+TypeOK ==
+    /\ c \in [ Node -> 0 .. M-1 ]
+------------------------------------------------------------------------------------
+
+Init ==
+    /\ c \in [ Node -> 0 .. M-1 ]
+
+CreateToken ==
+    (* Node 0 executes this action to inject new value into system *)
+    /\ c [0] = c [N-1]
+    /\ c' = [ c EXCEPT ![0] = (c[N-1]+ 1) % M ]
+
+PassToken(i) ==
+    (* Other nodes just copy value of the predecessor *)
+    /\ i # 0
+    /\ c [i] # c [i-1]
+    /\ c' = [ c EXCEPT ![i] = c[i-1]]    
+
+---------------------------------------------------------------------------------------
+Next == 
+    \/ CreateToken
+    \/ \E i \in Node \ {0} : PassToken(i)
+
+Spec == Init /\ [][Next]_vars /\ WF_vars(Next)    
+
+---------------------------------------------------------------------------------------
+UniqueToken ==
+    \E i \in 0 .. N :                           \* unique token at i (or i=N => token is at 0)
+       /\ \A j \in 0..i-1: c[j]= c[0]           \* before i all c equals c[0] 
+       /\ \A j \in i..N-1: c[j]= (c[0]-1) % M   \* after i all c following c[0]
+
+(* Stabilization property *)
+Stab  == <>[]UniqueToken
+
+---------------------------------------------------------------------------------------
+
+Alias ==
+    [
+        counter|-> c,
+        unique |-> UniqueToken
+    ]
+
+=======================================================================================