Re: [tlaplus] Consensus spec safety in Paxos example

Thanks, Markus. I may not have been clear enough.

Pavel was worried about the value of chosen changing from one state to the next:

>> If I am interpreting it correctly, the invariant does not fully specify the safety property: it allows a sequence in which a value is chosen, then another value replaces it (the size of the chosen set is still 1, so the invariant remains true). Or a value is chosen, then the set is emptied, then another value is chosen; etc.

One way to assert that chosen doesn't change after being set is through a liveness property like StaysChosen.

On Fri, 10 May 2024 at 15:29, Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:

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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/4PvjXi0tEBA/unsubscribe.
To unsubscribe from this group and all its topics, 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.