Hi Chris,
indeed, I should have checked the bug page on tlaplus.net before reporting this. It happened to me on an x86_64 architecture, running Mac OS X 10.8.2.
Stephan
Hi Stephan,
I run into this bug quite a lot. I reported it a while back, and Leslie added comments to the bug report.
http://bugzilla.tlaplus.net/show_bug.cgi?id=98 It appears to be a concurrency bug, which so far only manifests on x86_64 machines. What machine architecture and OS are you using? The easiest work-around I've found is to clone the affected model; the clone doesn't seem to have the problem.
Chris On Friday, October 12, 2012 8:42:49 AM UTC-7, Stephan Merz wrote: 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
|