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:
\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:
{ [ 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:
{ [ 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?