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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 13 Feb 2019 18:41:48 +0100*References*: <bd0c4d46-753e-4cfa-8c70-bac91a52b3fd@googlegroups.com> <1287F129-1A1A-4E50-BDC2-A3B60514D446@gmail.com> <edbb77cb-b6a4-446e-b8b9-d9057522fe17@googlegroups.com>

TCConsistent is not using two sets but one set RM. It says that the states of any two *elements* rm1 and rm2 of that set must agree in the sense that it cannot be the case that one has decided to abort (is in state "aborted") whereas the other one has decided to commit (is in state "committed"). This is a different pattern than your assertion, which links the state of a single motion (an element of set M) with states of movant / respondent (that are not elements of M). At any rate, a formula \A x \in S : P or \E x \in S : P where P does not contain x is just equivalent to P, assuming that S is non-empty (if S is empty then the \A formula is equivalent to TRUE and the \E formula is equivalent to FALSE).
OK, the invariant suggested in the previous message asserted that the system can be in one of two classes of states: one in which some m is in state "motion" or "reply" and some conditions hold, and one in which some m is in state "response" or "surreply" and certain conditions hold. But now TLC shows you that there exist states that are not covered by these two classes, namely a state where (the only) m is in state "hearing". For your invariant to be true at all states of the execution, these states must be covered by the invariant, presumably by adding a disjunct \/ ... \/ ... \/ /\ \E m \in M : mState[m] = "hearing" /\ ... \* whatever conditions you expect to hold for the other variables Figuring out invariants can be quite hard when you aren't used to this way of thinking about your system, but they structure your thinking about the system. Did you try what happens if set M contains more than one element? I'd expect you to see new counter-examples. Regards, Stephan -- 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout. |

**Follow-Ups**:**Re: [tlaplus] Fumbling Through TLA+***From:*Curt Flowers

**References**:**[tlaplus] Fumbling Through TLA+***From:*Curt Flowers

**Re: [tlaplus] Fumbling Through TLA+***From:*Stephan Merz

**Re: [tlaplus] Fumbling Through TLA+***From:*Curt Flowers

- Prev by Date:
**Re: [tlaplus] Fumbling Through TLA+** - Next by Date:
**Re: [tlaplus] Re: Temporal prop is violated, but error-trace doesn't show it** - Previous by thread:
**Re: [tlaplus] Fumbling Through TLA+** - Next by thread:
**Re: [tlaplus] Fumbling Through TLA+** - Index(es):