New to TLA - problem running model

[paul....@gmail.com]

Hi,

I've been trying to follow the initial examples in https://www.learntla.com/introduction/ , using the TLA+ toolbox 1.5.3 (64-bit, Linux, Java 8) but when I click on 'Run', nothing seems to happen in the UI.

Looking in the eclipse log, I find the following stack trace:
org.eclipse.core.runtime.AssertionFailedException: assertion failed: Cannot launch dirty model, save first.
at org.eclipse.core.runtime.Assert.isTrue(Assert.java:110)
at org.lamport.tla.toolbox.tool.tlc.model.Model.launch(Model.java:855)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor$5.run(ModelEditor.java:709)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2241)
at org.eclipse.core.internal.resources.Workspace.run(Workspace.java:2225)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor.launchModel(ModelEditor.java:577)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.ModelEditor.launchModel(ModelEditor.java:562)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.page.BasicFormPage.doRun(BasicFormPage.java:748)
at org.lamport.tla.toolbox.tool.tlc.ui.editor.page.BasicFormPage$RunAction.run(BasicFormPage.java:837)
at org.eclipse.jface.action.Action.runWithEvent(Action.java:473)
...


I can't see any way to deliberately save a model, and I get this error even if I restart the toolbox and immediately click on run.

I've searched on Google but can't seem to find anyone else with this problem. Any ideas what's wrong?

Thanks,
Paul Viney

[Leslie Lamport]

Please send all the necessary information to debug the problem to
Markus Kuppe.  That includes the the log file and the contents of the
spec's .toobox directory.  (See the "Reporting Problems" section of
the "In Case of Trouble" help page for instructions on how to find the
log file.

After you've done that, you can try to recover.  You can save the
model by typing Control-S in in the model.  However, I doubt if that
will help because I suspect the model is corrupted.  I suggest cloning
the model, deleting the original model, and running the clone.  If that
doesn't work, try creating a new model from scratch and running it.
If that fails, try deleting the spec and creating it again. 

If that doesn't fix the problem, see how broken your Toolbox is.  Create a new spec whose body consists of

   VARIABLE x
   Init == x = {}
   Next == x' = x \cup {1}

create a new model and run TLC on it.

Let us know what happens.

Leslie

[Paul Viney]

Thanks for the reaction. I've sent an email to Markus (to the address posted at github.com, which seemed to be the only email address I could find). I'll post any results as and when available.

Paul

[Paul Viney]

Markus was able to track the problem. Checking and unchecking anything in the model and resaving works around the problem.

Paul