[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
How can I check if a variable is stable if once set
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.