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

Any help would be appreciated. Still trying to figure this out.

On Thursday, March 21, 2019 at 12:34:59 PM UTC-4, Balaji Arun wrote:

Thanks for the help. To answer your questions:

1. I tried only with the minimal possible number of replicas.

2. I checked for Stability alone

3. Attached is the shortest error trace I could get. Sorry about that.

On Wednesday, March 20, 2019 at 10:25:46 PM UTC-4, Hillel Wayne wrote:

Making it fair shouldn't change the spec, since this is a temporal safety property- stuttering shouldn't play into the counterexample.

I created a simple spec that starts with cmdLog in the penultimate state, transitions to the ultimate state, and then stays in that state. That does not give a counterexample for Stability or []Stability. I don't think there's enough info here to diagnose what the issue is. So three questions:

Do you get a counterexample for a smaller number of replicas? If so, is it shorter? This is important because TLC doesn't guarantee a minimal error trace for temporal properties.

What is the exact temporal property you checked? Is it Stability, []Stability, or something else? Are there any other temporal properties you are checking as part of the same model? If so, does removing them get rid of the counterexample?

What is the error trace, in full? If you can produce an error with a smaller number of replicas, please provide that instead.

H

On 3/20/19 6:24 PM, Balaji Arun wrote:

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