|
The problem is that you made GoodReplicas a symmetry
set. You shouldn't combine temporal properties and symmetry sets.
In this case it just gave you a false positive, but it can also
miss actual violations when you do this.
H
On 4/1/19 9:41 PM, Balaji Arun wrote:
Thanks for the help. PFA.
On Saturday, March 30, 2019 at 4:52:23 PM UTC-4, Giuliano wrote:
Can you send us all the files necessary to reproduce the
problem locally?
On March 30, 2019 12:37:42 PM PDT,
Balaji Arun < ba2...@xxxxxx> wrote:
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...@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.
--
Sent from my mobile device
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.
|