[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Why is this temporal property violated?



Hi,

I have a temporal property that must be satisfied, but I am not able to figure out the violation from the counter-example.

This is my temporal property:
Stability ==
   
\A replica \in Replicas :
       
\A i \in Instances :
           
\A C \in Commands :
               
[]((\E rec1 \in cmdLog[replica] :
                   
/\ rec1.inst = i
                    /
\ rec1.cmd = C
                   
/\ rec1.status \in {"committed"}) =>
                   
[](\E rec2 \in cmdLog[replica] :
                       
/\ rec2.inst = i
                        /
\ rec2.cmd = C
                       
/\ rec2.status \in {"committed"}))

This is the last state of cmdLog before stuttering: 

( r0 :>
     
{ [ inst |-> <<r0, 1>>,
          ballot
|-> <<0, r0>>,
          cmd
|-> cmd1,
          deps
|-> {},
          seq
|-> 1,
          status
|-> "committed" ] } @@
  r1
:>
     
{ [ inst |-> <<r0, 1>>,
          ballot
|-> <<0, r0>>,
          cmd
|-> cmd1,
          deps
|-> {},
          seq
|-> 1,
          status
|-> "committed" ] } @@
  r2
:>
     
{ [ inst |-> <<r0, 1>>,
          ballot
|-> <<0, r0>>,
          cmd
|-> cmd1,
          deps
|-> {},
          seq
|-> 1,
          status
|-> "committed" ] } @@
  r3
:>
     
{ [ inst |-> <<r0, 1>>,
          ballot
|-> <<0, r0>>,
          cmd
|-> cmd1,
          deps
|-> {},
          seq
|-> 1,
          status
|-> "committed" ] } )

This is the state before last:

( r0 :>
     
{ [ inst |-> <<r0, 1>>,
          ballot
|-> <<0, r0>>,
          cmd
|-> cmd1,
          deps
|-> {},
          seq
|-> 1,
          status
|-> "committed" ] } @@
  r1
:>
     
{ [ inst |-> <<r0, 1>>,
          ballot
|-> <<0, r0>>,
          cmd
|-> cmd1,
          deps
|-> {},
          seq
|-> 1,
          status
|-> "committed" ] } @@
  r2
:>
     
{ [ inst |-> <<r0, 1>>,
          ballot
|-> <<0, r0>>,
          cmd
|-> cmd1,
          deps
|-> {},
          seq
|-> 1,
          status
|-> "committed" ] } @@
  r3
:>
     
{ [ inst |-> <<r0, 1>>,
          ballot
|-> <<0, r0>>,
          cmd
|-> cmd1,
          deps
|-> {},
          seq
|-> 1,
          status
|-> "spec-ordered" ] } )

Why is Stability violated 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.