|
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+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.
--
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.
|