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
On Saturday, September 30, 2017 at 4:05:10 AM UTC-7, paul.viney wrote:
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