Re: [tlaplus] TLC Models "resetting" problem

[Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 13.04.2015 14:10, Michael Peterson wrote:
> 
> I'm fairly new to TLA+ and PlusCal.  I've worked through most of the
> examples in Leslie's writings and really enjoyed them. Now I'm writing a
> spec for an algorithm of my own design.
> 
> I've noticed a problem with TLC that I'm wondering someone else has seen
> and knows what's happening.  Here's the problem scenario that has
> occurred now perhaps two dozen times working on different specs
> (including the example ones):
> 
> I have a working PlusCal/TLA spec and model and I run the model, all is
> good.  Then I make some change to my TLA spec and get an error.  I then
> fix the error, have it retranslated into TLA and reparsed. then when I
> go back to the Model to run it, TLC reports an error, which is that
> defaultInitValue is no longer assigned (it had been assigned before to
> the default model value you get when you create a new model).
> 
> So then I select defaultInitValue in the "What is the model" section and
> specify "model value" for it.  Now when I press the Run TLC button it
> always and forever immediately finishes with Diameter=0, States Found=0,
> Distinct States=0 and Queue Size=0 and has no output in the User Output
> (even if I have print statements).   No matter what I try, at this point
> that model is confused and I can't get it working again.  It reports no
> errors and the Spec status is "parsed".
> 
> If I then create a new model with the exact same TLA Spec, it works fine.
> 
> So I have this workaround, but when you start getting to a dozen models,
> when you only need one, it gets pretty frustrating.
> 
> It doesn't happen every time, and I don't know the exact keystrokes that
> cause it.
> 
> Does anyone else see this problem and is there a way to make it stop or
> get the Model "unstuck".  I am working with TLA+ Toolbox 1.4.8 on Linux.

Hi Michael,

unfortunately I fail to reproduce your problem with both 1.4.8 and the
current development version locally, so I can't tell if the development
version [1] fixes your problem. Can you try and let us know?

If you are able to reproduce it even with the development version, then
please provide some or info about your environment and possibly share
the spec.

Thanks
Markus

[1] http://tla.msr-inria.inria.fr/tlatoolbox/ci/products/