Non reactive HMI

44 views
Skip to first unread message

Asterion Daedalus

unread,
Apr 25, 2017, 7:44:39 AM4/25/17
to tlaplus
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

Markus Alexander Kuppe

unread,
Apr 26, 2017, 3:20:48 AM4/26/17
to tla...@googlegroups.com
On 25.04.2017 13:44, Asterion Daedalus wrote:
> I have toolbox 1.5.0 running on windows 10.
>
> [...]
>
> 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


In a private email Asterion confirmed, that the bug is gone in the most
recent 1.5.3 release of the Toolbox.

M.

Asterion Daedalus

unread,
Apr 26, 2017, 5:13:14 AM4/26/17
to tla...@googlegroups.com
Ah hem. I did not say bug was gone. I said it hasn't materialised yet in 1.5.3.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/YrjXD9K_0Rc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
Reply all
Reply to author
Forward
0 new messages