I'm assuming that your constant set M contains not just one element...
Correct.
...[M -> {"motion", "response", "reply", "surreply", "hearing", "granted", "denied", "ruling"}]
...[M -> {"motion", "response", "reply", "surreply", "hearing", "granted", "denied", "ruling"}]
mState[m] is either "motion" or "reply" *
Yes, this is what I'm trying to say. When the state of a motion (m) is in either "motion" or "reply" then movant should = "active" (not not be "idle"). I tried that and I got an error saying that my function requires 1 arg, which confused me. But I digress.
...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"
\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.
...showing that there is some real misunderstanding of logical formulas...
An invariant is true in every reachable state. If that's not the meaning then I also don't understand that. I thought/think I understood logical formulas, but that's also why I'm here. I'm unsure its the understanding or the writing of logical formulas (like any other language. Understanding is not the same as speaking it).
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.
