Re: [tlaplus] Fumbling Through TLA+

...is strange since the bound variable m1 doesn't appear in the body...
This is one of the "templates" I was talking about before. This is from TCConsistent.

TCConsistent ==
\A rm1, rm2 \in RM : ~ /\ rmState[rm1] = "aborted"
/\ rmState[rm2] = "committed"

I understand what the formula/function is saying. My formula doesn't use two different sets, so m1 and m2 would not be relevant. Each motion stands alone is not compared to each other like resource managers (RM) of TCommit. It was an experiment as I test out my understanding (or lack there of) hoping to stumble upon a correct answer and the glean why it did work and what I did wrong. While that has happened a few times, this time it did not.

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).

the invariant can be written as...
Reading your version, I can see the error in my understanding of how to write TLA, but your formula makes sense to me. However, I still got the same error. One thing I'm sure of is how to read these error statements. I know this is a "better" error (Error-Trace) than the one I was getting it's still the same error.

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