--------------------------------- 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
]
=======================================================================================