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

*From*: "'Pavel Kalinnikov' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Fri, 10 May 2024 05:45:26 -0700 (PDT)*References*: <1fbd9797-40e6-4121-b559-e0a60195d41cn@googlegroups.com> <f9b1929a-7fdc-496f-8fd2-71b6f882c4a7n@googlegroups.com> <1d30479e-a03f-4f9d-b15f-fca2ba5cf07fn@googlegroups.com> <8b18774d-7507-4ef2-ab36-0e85c9854221n@googlegroups.com> <fa542e83-de10-46f2-b816-e32d00fc4754n@googlegroups.com>

Hi Jones,

Yes, I agree that Init/Next on its own correctly specifies consensus, with the temporal aspect of it. Hence was my original question: what value does the `Inv` and THEOREM bring to this spec, given that it only states a necessary but not sufficient invariant for consensus? For what I see, both `Inv` and THEOREM can be removed from this file, and the spec will remain rigorous.

And the second part of my question was: can we state a more rigorous property here, instead of `Inv`, such as:

"chosen \in chosen' /\ Cardinality(chosen') \leq 1"

and prove a THEOREM that more convincingly confirms that Init/Next spec is the right thing?

Thank you,

Pavel

On Thursday, May 9, 2024 at 4:07:07 AM UTC+1 Jones Martins wrote:

Hi Pavel,If I understood you correctly, you're saying the formula `Inv` doesn't represent a consensus safety property: this invariant is too weak, and it's satisfied by a sequence of assignments for `chosen` such as {} -> {1} -> {} -> {2} -> {2} -> etc.That's true. In fact, there's an infinite number of possible behaviors in the universe such that `Inv` is True, but these behaviors are irrelevant. It depends on what specification described these behaviors in the first place, and that `chosen` has the same meaning in both specifications. Meaning is essential.> To demonstrate that, we can change the `Next` action in such a way that the invariant will still hold. For example, if we can allow a transition from {v} back to {}, the invariant is still true, but the safety is broken.Indeed, but that wouldn't be a consensus specification anymore.> The safety invariant here has to have a temporal aspect: once the chosen set is non-empty, it stays so.What is so elegant about TLA+ is that the “temporal aspect” you mentioned is the specification itself. In other words, Consensus' Spec expresses that “once the chosen set is non-empty, it stays so”: action `Next` in `Consensus` selects one value, then stutters forever.Best,JonesP.S. I'd expand on the true danger of false positives through bad refinement mappings, but it's late here, and I need to sleep hahaOn Wednesday 8 May 2024 at 19:51:00 UTC-3 Pavel Kalinnikov wrote:Hi Jones,Your explanation matches my understanding, however I think the `Inv` does not correctly represent a consensus safety property. To demonstrate that, we can change the `Next` action in such a way that the invariant will still hold. For example, if we can allow a transition from {v} back to {}, the invariant is still true, but the safety is broken.The safety invariant here has to have a temporal aspect: once the chosen set is non-empty, it stays so.I.e. the comment "Safety: At most one value is chosen" seems misleading here. It does expresssomeinvariant, but this invariant does not on its own guarantee safety.Thank you,PavelOn Wednesday, May 8, 2024 at 10:58:17 PM UTC+1 Jones Martins wrote: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,JonesOn Wednesday 8 May 2024 at 16:41:29 UTC-3 Pavel Kalinnikov wrote:Should this line/\ Cardinality(chosen) \leq 1be augmented with something like:/\ Cardinality(chosen') \leq 1/\ chosen = {} \/ chosen' = chosenOn 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

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/bdfa1d6c-3554-4dd2-b539-70a9ee6accf5n%40googlegroups.com.

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

**References**:**[tlaplus] Consensus spec safety in Paxos example***From:*'Pavel Kalinnikov' via tlaplus

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

**[tlaplus] Re: Consensus spec safety in Paxos example***From:*Jones Martins

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

**[tlaplus] Re: Consensus spec safety in Paxos example***From:*Jones Martins

- Prev by Date:
**Re: [tlaplus] Developing a TLA+ Model for the KafkaRoller in the Strimzi Project** - Next by Date:
**[tlaplus] Re: Consensus spec safety in Paxos example** - Previous by thread:
**[tlaplus] Re: Consensus spec safety in Paxos example** - Next by thread:
**[tlaplus] Re: Consensus spec safety in Paxos example** - Index(es):