[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 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,

On 24 Jun 2017, at 18:59, Christian Spann <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,

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.