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

Re: [tlaplus] Fumbling Through TLA+

I still can't get this to work. I've tried everything. I keep getting an error saying mState is undefined or not an operator with the:

\E m \in M : mState[m] = "anything state here"

Went back to HyperBook and looked at the Math section. Everything lines up. I used the examples as templates that I modified to make sense with my spec (of course that is questionable at this point).

However, after talking with you I did redesign the spec as I noticed I didn't have enough states. There needed to an idle period (both movant and respondent "idle") after each state.

Still...with all my effort, I've emerged empty handed. I've been working on this all day. I can get BothNotActiveInv to work just fine but anything that mention mState or M doesn't work.

I did use the "Evaluate Constant _expression_" section and found that if I put:

m \in M # "any state here" it came back TRUE (and if = to any state, FALSE).

That is the closet I got to something working. So it recognizes m \in M but on with any elements of the set of M.

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.