Re: [tlaplus] Consensus spec safety in Paxos example

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

What Pavel suggests (chosen = {} / chosen' = chose) is not a liveness but a safety property; its counterexample is a finite prefix of a behavior, e.g., a prefix where v1 is chosen but replaced by v2.

This property cannot be stated as an invariant, i.e., a state-level formula. The occurrence of the prime operator turns it into an action-level formula.  Note, though, that Pavel’s formula is not a legal TLA formula because it is not stuttering-insensitive (see page 90 in Specifying Systems).


Regarding the original question: Note that Voting states the theorem Spec => Consensus!Spec, making the behavior formula Spec in Consensus Pavel’s desired correctness property, except for Voting.  We can also say that Voting refines Consensus.  For Consensus, it is probably easy enough to see that Consensus satisfies the proposed property above.

M.


> On May 10, 2024, at 10:38 AM, Jones Martins <jonesmvc@xxxxxxxxx> wrote:
> 
> Sure! What you seem to be trying to express is a liveness property instead of an invariant.
> Just be careful not to assert about values in the next state, such as chosen'.


-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/B121361B-894F-421E-BA0A-E1F0156F187E%40lemmster.de.