TLC Models "resetting" problem

Hi all,

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.

Thank you,
-Michael