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

Re: Display bug in TLA+ Toolbox / TLC

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.


On Oct 12, 2012, at 7:47 PM, Chris Newcombe <chris.n...@xxxxxxxxx> wrote:

Hi Stephan,

I run into this bug quite a lot.   I reported it a while back, and Leslie added comments to the bug report. 


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.


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.