| 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. 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.
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.
Hope this helps, Stephan
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.
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.
|