From f6689cf1c3802123649406fccd8ef73070c95cd6 Mon Sep 17 00:00:00 2001 From: Murat Demirbas Date: Fri, 30 Sep 2022 22:20:53 -0700 Subject: [PATCH] Add ewd426 --- README.md | 1 + specifications/ewd426/SimTokenRing.cfg | 25 ++++++++++ specifications/ewd426/SimTokenRing.tla | 27 +++++++++++ specifications/ewd426/TokenRing.cfg | 18 ++++++++ specifications/ewd426/TokenRing.tla | 63 ++++++++++++++++++++++++++ 5 files changed, 134 insertions(+) create mode 100644 specifications/ewd426/SimTokenRing.cfg create mode 100644 specifications/ewd426/SimTokenRing.tla create mode 100644 specifications/ewd426/TokenRing.cfg create mode 100644 specifications/ewd426/TokenRing.tla diff --git a/README.md b/README.md index c14a6a57..929aacac 100644 --- a/README.md +++ b/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 | Specification and model-checking of both safety and liveness properties of Streamlet with TLC | Giuliano Losa | | ✔ | Sequences, Integers, FiniteSets | ✔ | | | 90 | Petri Nets | Instantiable Petri Nets with liveness properties | Eugene Huang | | ✔ | Integers, Sequences, FiniteSets, TLC | | | 91 | Knuth Yao & Markov Chains | Knuth-Yao algorithm for simulating a sixsided die | Ron Pressler, Markus Kuppe | | ✔ | DyadicRationals | | +| 92 | ewd426 - Token Stabilization | Self-stabilizing systems in spite of distributed control | Murat Demirbas, Markus Kuppe | | ✔ | Naturals, FiniteSets | | ## License diff --git a/specifications/ewd426/SimTokenRing.cfg b/specifications/ewd426/SimTokenRing.cfg new file mode 100644 index 00000000..3051ac2f --- /dev/null +++ b/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 diff --git a/specifications/ewd426/SimTokenRing.tla b/specifications/ewd426/SimTokenRing.tla new file mode 100644 index 00000000..a8096835 --- /dev/null +++ b/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", <>,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' \ No newline at end of file diff --git a/specifications/ewd426/TokenRing.cfg b/specifications/ewd426/TokenRing.cfg new file mode 100644 index 00000000..41613bba --- /dev/null +++ b/specifications/ewd426/TokenRing.cfg @@ -0,0 +1,18 @@ +CONSTANTS + N = 6 + M = 6 + +CHECK_DEADLOCK + FALSE + +SPECIFICATION + Spec + +INVARIANT + TypeOK + +PROPERTIES + Stab + +ALIAS + Alias \ No newline at end of file diff --git a/specifications/ewd426/TokenRing.tla b/specifications/ewd426/TokenRing.tla new file mode 100644 index 00000000..729333f5 --- /dev/null +++ b/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 + ] + +=======================================================================================