Yes, (Actually M=2 and N = 4) But the requirement that M >= N -1 is not a liveness temporal property set in the spec anywhere. It's just the model checking fails for those cases.I am trying to understand why, because with strong fairness on all the actions, this cycle with unstable states should be broken and jump into the stable states.For example, from the init state [0, 0, 1, 0], which is part of the cycle, if the PassToken2 or PassToken3 were executed, the system would have reached either [0, 0, 0, 0] or [0, 0, 1, 1] both are stable. Since both these are Strong Fair, and the action gets enabled infinitely often (because of the cycle), it should have taken at least once.--On Wed, 13 Mar 2024 at 09:06, divyanshu ranjan <idivyanshu.ranjan@xxxxxxxxx> wrote:Looking at the state trace, it seems to me that M = 2 and N = 3 which does n't satisfy M >= N requirement.--On Wed, Mar 13, 2024 at 2:29 PM jayaprabhakar k <jayaprabhakar@xxxxxxxxx> wrote: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.
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/CAL9hw27Wg%3Dz7gJOQGQ_tt%3Dcr_Lnnw-mVHgbSqanURbzxcR4jcA%40mail.gmail.com.
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%3DSiJ9PHkK5kfC34ZLK8tUr17P8KL0FB6BwXQB03cjbmkOUA%40mail.gmail.com.
