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

Re: [tlaplus] Fumbling Through TLA+

I fixed the original error by completing the IF statement. All 3 statements must be present IF/THEN/ELSE. However, that only introduced an new error as I don't know who to express what I'm trying to say properly in that statement still. The error is now with my my questions I asked about /\ jdState \in JD. That is the error thrown when running the checker.

In computing initial states, the right side of \IN is not enumerable.
line 35, col 9 to line 35, col 22 of module summons
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. SInit
1. Line 33, column 6 to line 38, column 16 in summons
2. Line 33, column 9 to line 33, column 44 in summons
3. Line 34, column 9 to line 34, column 43 in summons
4. Line 35, column 9 to line 35, column 22 in summons

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.