Hi Chris,
I presume that the workaround by cloning means cloning the model, producing a new model with some of the invariants de-selected, and then running the clone; and that the
Toolbox then reports the correct error. I also presume that the bug will reappear in the clone if you change which invariants are selected. Is this correct?
My current inclination is to eliminate the ability to un-check invariants and properties. (Do you know if the problem occurs with properties as well as invariants?) One
can obtain the equivalent functionality by cloning the model and deleting invariants from the clone, and the inconvenience of having to do this seems better than leaving the bug to bite unsuspecting users.
What do people think of this “fix”?
Leslie
From: tla...@xxxxxxxxxxxxxxxx [mailto:tla...@xxxxxxxxxxxxxxxx]
On Behalf Of Chris Newcombe
Sent: Friday, October 12, 2012 10:48 AM
To: tla...@xxxxxxxxxxxxxxxx
Cc: stepha...@xxxxxxxx
Subject: [tlaplus] Re: Display bug in TLA+ Toolbox / TLC
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
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
To unsubscribe from this group, send email to
tlaplus+unsu...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.