[tlaplus] Re: Why is this temporal property violated?

[Balaji Arun <ba2669@xxxxxx>]

I tried with the fairness assumption, but did not work.

Thanks,

Balaji

On Wednesday, March 20, 2019 at 7:05:30 PM UTC-4, Andrew Helwer wrote:

Are you assuming any fairness properties?

On Wednesday, March 20, 2019 at 3:03:48 PM UTC-7, Balaji Arun wrote:

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.