Hi Pavel,
The Voting module instantiates the Consensus module to prove that Voting's Spec implies Consensus' Spec.
The consensus specification itself is pretty abstract.
Init expresses that chosen = {} is true in the first state of every behavior.
Next expresses that if chosen = {} is true, then chosen' = { <some value> }.
This means that, when some value has been chosen, it never changes again, so the original `Inv` invariant is strong enough.
By the way, `Inv` can't be augmented as you suggested. Invariants are state predicates, and state predicates don't contain primed variables.
Best,
Jones
On Wednesday 8 May 2024 at 16:41:29 UTC-3 Pavel Kalinnikov wrote:
Should this line
/\ Cardinality(chosen) \leq 1
be augmented with something like:
/\ Cardinality(chosen') \leq 1
/\ chosen = {} \/ chosen' = chosen
On Wednesday, May 8, 2024 at 8:24:27 PM UTC+1 Pavel Kalinnikov wrote:
Hello,
I am looking at the
Consensus spec in tlaplus examples repo, which specifies the single-value consensus problem.
The Init/Next spec in this file correctly specifies consensus, because it precludes the chosen set from changing after it got to contain exactly one value.
What value does the the safety invariant in
lines 36-37, and the theorem that follows it, bring to this spec? 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.
Is the value of this invariant+theorem in just demonstrating an interesting property? Is it not strictly needed to be in this spec?
Is there a way to fix this invariant, so that it fully represents the consensus safety property (rather than partially, like it seems).
Thank you,
Pavel