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

Thanks for the reply. Let me check my spec again. Or I will see if I can find somebody with more familiarity.

On Tuesday, March 26, 2019 at 10:42:41 PM UTC-4, Hillel Wayne wrote:

Hi,

As far as I can tell, that trace should satisfy []Stability. I think this is something we can't diagnose on the newsfeed. My guess is there's either a TLC configuration issue in your spec or some nonstandard way you wrote the spec, but again it's not something we can figure out without sitting down and looking at your whole project. Is anybody else in your department familiar with TLA+?

H

On 3/25/19 3:32 PM, Balaji Arun wrote:

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.

--
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 tla...@googlegroups.com.
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.