[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] How can I check if a variable is stable if once set
Dear Stephan,
thanks a lot for your quick reply - your answer helps! I actually even wondered how to use [][A]_e = [ A \/ (e' = e )] shown in the TLA "cheat sheet" as it is in fact just what I want to check. But I didn't manage to compile the formula correctly. More inline
Am 25.06.2017 um 18:51 schrieb Stephan Merz:
Dear Christian,
the property that you are trying to verify expresses that once a value has been decided, the decision never changes. This property cannot be expressed as a (state) invariant because it involves more than one state. It can be written as the temporal formula
\A s \in Server : \A v \in View : [][ decided[s][v] # Undef => UNCHANGED decided[s][v] ]_vars
or, more concisely, as
\A s \in Server : \A v \in View : [][ decided[s][v] = Undef ]_<<decided[s][v]>>
which TLC should be able to check.
I first added your temporal formula to my invariant which should check agreement. This seems to be syntactically wrong which makes sense as it is no state invariant as you state above. It has to go to the Properties section where it works better... - right? Well if I try your approach TLC reports the following error when I add the property
DecidedStable == \A s \in Server: \A v_c \in View: [] [decided[s][v_c] = Undef]_<<decided[s][v_c]>>
to the Properties Section of the model:
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
:
Temporal formulas containing actions must be of forms <>[]A or []<>A.
Even though TLC tells me what it wants I struggle to come up with a predicate which checks the stability of a decided value and that is eventually always true or the other way round ... In both cases decided[s][v] could hop through arbitrary values before becoming stable - right? And if I understand the corresponding section 8.1 Temporal Formulas in "Specifying Systems" correctly, your proposal is a valid temporal formula even under stuttering.
Please note that this is only one of the properties expected of a Consensus algorithm. The main one is that whenever two servers have decided, then they must agree on the value.
FYI: I try to check this with the following state predicate without temporal logic. The idea here is, that the decision vector of every pair of servers must be equal up to the latest decision of the less advanced one:
maxdecided(s) == CHOOSE v \in View : decided[s][v] # Undef /\ ~ (\E w \in View : decided[s][w] # Undef /\ w > v)
mindecided(s,t) == min( { maxdecided(s), maxdecided(t) } )
DecidedSafe == \A s,t \in Server: \A v_c \in { vt \in View : vt <= mindecided(s,t) } :
(s # t ) => decided[s][v_c] = decided[t][v_c]
Together with the property that decisions are stable this should check the safety property of the algorithm.
Concerning your side remark on CHOOSE: TLC is unable to evaluate an unbounded CHOOSE expression, or one whose bound is an infinite set. If you use such a definition in your TLA+ specification, you will have to override it for TLC (see tab advanced options / definition override), for example by -1 or (a little nicer) by a model value.
Thanks for the confirmation, I changed Undef to be a Model Value.
Best regards,
Christian
On 24 Jun 2017, at 18:59, Christian Spann <cspanns....@xxxxxxxxx <mailto:cspanns....@xxxxxxxxx>> wrote:
Dear TLAplus group,
I would like to check the safety property of a byzantine fault tolerant consenus algorithm by specifying an invariant of the form :
CONSTANT View, Request, Server
Undef == -1
Init == ...
/\ decided = [ s \in Server |-> [ dv \in View |-> Undef ] ]
DecidedSafe == \A s \in Server: \A v_c \in View: decided[s][v_c] # Undef => decided[s][v_c] = decided[s][v_c]'
I think this should be equal to decided[s][v_c] # Undef -> UNCHANGED <<decided[s][v_c]>> which produces the same unwanted behavior.
For completeness: Undef == -1 because TLC runs into an error with my initial definition it like Leslie Lamport did in his proof of ByzPaxos BConProof.tla in an unbounded way (Undef == CHOOSE v \in Nat : v \notin Request OR Undef == CHOOSE v : v \notin Request} \) and TLC is forced to actually check it, but this is a different story and this "bug" is known if I read the TLC Website correctly.
Back to my approach: If I run TLC with the above stated invariant it stops execution every time decided[s][v_c] is initially set to some value != Undef. I unfortunately lack in depth understanding of TLA/TLC and so I failed to come up with a predicate which provides the expected invariant up to now. I also failed to state an invariant using a temporal formula e.g. by using the [] operator because I guess this operator does not work in a conditional way? Maybe someone can give me a pointer in the right direction. If I have to provide more Information I will try to create a more complete minimum working example without having to provide the complete spec.
Best regards,
Christian
--
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 <mailto:tlaplus+u...@xxxxxxxxxxxxxxxx>.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx <mailto: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 tlaplus+u...@xxxxxxxxxxxxxxxx <mailto:tlaplus+u...@xxxxxxxxxxxxxxxx>.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx <mailto:tla...@xxxxxxxxxxxxxxxx>.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.