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

Re: [tlaplus] Re: Display bug in TLA+ Toolbox / TLC

Hi Leslie,

   >>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. 

Yes.

  >>I also presume that the bug will reappear in the clone if you change which invariants are selected.

I suspect so, but I can't clearly recall an incident in which this happened.   I just spent 10 minutes trying to reproduce the bug, and failed.   I recently switched to using a newer 32-core x86_64 machine, and I am now using Sun Java JDK 7 update 7 64-bit.  When I reported the bug I was using Sun Java 6, on either a 2-core or a 16-core machine (I can't remember, but it was definitely not the same as my current machine).  I'm not sure if the newer machine or newer version of java has 'fixed' the issue, or if I'm just being temporarily (un)lucky with the non-determinism.

  >>Do you know if the problem occurs with properties as well as invariants?

I've only very recently started checking liveness properties.  The one occasion I've tried checking 2 separate properties in the list, the toolbox simply reported "Temporal properties were violated" and gave an error trace.  i.e. It didn't report which property was violated.  So I don't know if the problem affects properties.  (It would be nice if the toolbox did say which property was violated.)

     >>My current inclination is to eliminate the ability to un-check invariants and properties.

In my opinion that's fine from the user-interface perspective.   I found that comments in the (* ... *) style work as expected in invariants/properties, so it's very easy to temporarily disable an invariant by commenting-out the actual invariant and prefixing it with TRUE.

One point; in my original bug report...
    http://bugzilla.tlaplus.net/show_bug.cgi?id=98 
... I mention a second related bug in which the problem still occurred if the unchecked invariants were completely removed from the list.  It even continued to occure if the entire list was emptied, and one broken invariant added back in.   
So I suspect there's a more fundamental problem.  

Still, your proposal should 'fix' the problem, as long as the bug does not affect visibility of changes to the text of invariants.  So far I've never observed that kind of issue.

thanks,

Chris


On Sun, Oct 21, 2012 at 12:45 PM, Leslie Lamport <lam...@xxxxxxxxxxxxx> wrote:

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+u...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
 
 

--
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+u...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.