New to TLA - problem running model

[paul....@xxxxxxxxx]

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