I came across the following relatively minor annoyance in the Toolbox when running TLC. The specification attached to this message contains non-properties for checking eventual executability of individual actions. Load it into the Toolbox, create a new model, and fix suitable parameters. (For example, assign the set of model values {a,b,c,d} to Data and 4 to maxChan.)
Now check (non-)invariant NeverSend. TLC will report through the Toolbox that the predicate does not hold in the initial state. Fine. Now check (non-)invariant NeverResend, deselecting the previous invariant NeverSend. TLC will report the same error message, making you believe that it didn't check the correct property. Looking at the TLC output (in AlternatingBit.toolbox/Model_1/MC.out), it becomes obvious that TLC checked the right property (indeed, action Resend is also enabled in the initial state), so it must be a display bug in the Toolbox. Not critical, but mildly annoying.
In fact, on checking the other (non-)invariants the Toolbox still claims that (non-checked) invariant NeverSend is violated, although it updates the counter-example.
Stephan
Attachment:
AlternatingBit.tla
Description: Binary data