[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: "'Pavel Kalinnikov' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Wed, 8 May 2024 12:10:33 -0700 (PDT)

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

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/1fbd9797-40e6-4121-b559-e0a60195d41cn%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Consensus spec safety in Paxos example***From:*'Pavel Kalinnikov' via tlaplus

- Prev by Date:
**Re: [tlaplus] TLC Development** - Next by Date:
**[tlaplus] Re: Consensus spec safety in Paxos example** - Previous by thread:
**Re: [tlaplus] TLC Development** - Next by thread:
**[tlaplus] Re: Consensus spec safety in Paxos example** - Index(es):