Hi,--I am trying out Dijkstra's Self Stabilizing for Token ring algorithm.https://muratbuffalo.blogspot.com/2022/10/checking-statistical-properties-of.html
The spec has two actions - CreateToken and PassToken. The spec as given, fails liveness property if N < M - 1. The trace looks reasonable.Looking at the state space, making these two actions as Strong Fair should fix the liveness issue, but it doesn't seem to.Listing out all the states,There are two cycles. The unstabilized cycle at the top in black and the stabilized cycle at the bottom in green.
1. Once the stable (green) nodes are reached, there is no way to reach an unstable (black) node.2. From any unstable node, there is always a next state to the green node.
And, from every action here is Strong Fair, the link should be enabled infinitely often, and so one of the transitions should happen eventually.The code is:
---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]]
PassTokens ==
\E i \in Node \ {0} : PassToken(i)
PassToken1 == c [1] # c [0] /\ c' = [ c EXCEPT ![1] = c[0]]
PassToken2 == c [2] # c [1] /\ c' = [ c EXCEPT ![2] = c[1]]
PassToken3 == c [3] # c [2] /\ c' = [ c EXCEPT ![3] = c[2]]
---------------------------------------------------------------------------------------
Next ==
\/ CreateToken
\/ PassToken1
\/ PassToken2
\/ PassToken3
Spec == Init /\ [][Next]_vars /\ SF_vars(PassToken1) /\ SF_vars(PassToken2) /\ SF_vars(PassToken3) /\ SF_vars(CreateToken)
---------------------------------------------------------------------------------------
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
---
The error trace:
<<
[
_TEAction |-> [
position |-> 1,
name |-> "Initial predicate",
location |-> "Unknown location"
],
c |-> (0 :> 0 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> 0)
],
[
_TEAction |-> [
position |-> 2,
name |-> "CreateToken",
location |-> "line 30, col 5 to line 31, col 47 of module TokenRing"
],
c |-> (0 :> 1 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> 0)
],
[
_TEAction |-> [
position |-> 3,
name |-> "PassToken3",
location |-> "line 44, col 15 to line 44, col 59 of module TokenRing"
],
c |-> (0 :> 1 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> 1)
],
[
_TEAction |-> [
position |-> 4,
name |-> "PassToken2",
location |-> "line 43, col 15 to line 43, col 59 of module TokenRing"
],
c |-> (0 :> 1 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 1)
],
[
_TEAction |-> [
position |-> 5,
name |-> "PassToken1",
location |-> "line 42, col 15 to line 42, col 59 of module TokenRing"
],
c |-> (0 :> 1 @@ 1 :> 1 @@ 2 :> 0 @@ 3 :> 1)
],
[
_TEAction |-> [
position |-> 6,
name |-> "CreateToken",
location |-> "line 30, col 5 to line 31, col 47 of module TokenRing"
],
c |-> (0 :> 0 @@ 1 :> 1 @@ 2 :> 0 @@ 3 :> 1)
],
[
_TEAction |-> [
position |-> 7,
name |-> "PassToken3",
location |-> "line 44, col 15 to line 44, col 59 of module TokenRing"
],
c |-> (0 :> 0 @@ 1 :> 1 @@ 2 :> 0 @@ 3 :> 0)
],
[
_TEAction |-> [
position |-> 8,
name |-> "PassToken2",
location |-> "line 43, col 15 to line 43, col 59 of module TokenRing"
],
c |-> (0 :> 0 @@ 1 :> 1 @@ 2 :> 1 @@ 3 :> 0)
]
>>What am I missing here?
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CA%2Bt%3DSi%2B11pQwgXkCZdnB_q%3DNdS1XCVEumqd7tPLO%2B28R1%3Ddegg%40mail.gmail.com.
