[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Non reactive HMI



I have toolbox 1.5.0 running on windows 10.

I have been working through the TLA+ book.

I was able to work through the one bit clock exercise.

Having dived into the Die Hard Problem I was able to draft the spec and build a model to run.  The model ran without problems, however I had yet to add the invariant under "What to Check?".

When I clicked on the Add button for "What to Check?" there was no response.  

I reopened the One Bit Counter project than back to the Die Hard project to find no edit windows opened. That is, neither the specification editor or the model editor would open after a double click.  Although, I did note, eventually, the model editor came up after a couple of minutes after the double mouse click on the explorer.  It was hit or miss if I shutdown the app, whether (when it was restarted) that the specification editor was open.

I subsequently found neither Add or Edit buttons on the model editor were reacting.  I could enter text in text fields and check boxes and scroll buttons etc seemed to work.

Getting now the following error from specification page:

An internal error occurred during: "Periodic workspace save.".
Cannot set lower sequence number for root (previous: 13, new: 12). Location: D:\Safety\TLA+\workspace\.metadata\.plugins\org.eclipse.core.resources\.safetable\org.eclipse.core.resources

When I switch to model editor I get:
An internal error has occurred.
java.lang.NullPointerException