TLA+ Toolbox issues?

[Jones Martins]

Hi everyone,

In summary:

1. Where does the Toolbox save its settings?
2. Does the Toolbox run tla2tools.jar from /opt/TLA+Toolbox/tla2tools.jar?

---

I’m running Ubuntu 22.04 and I’m having some issues with the Toolbox.

I stumbled upon a liveness “bug” in the Toolbox version 1.71 and version 1.80, where TLC detects stuttering where there isn’t any when verifying liveness properties.

The specification is simple enough to see there isn’t stuttering at all. I ran an external tla2tools.jar version 2.18 from the terminal and no problems were detected in my spec.

So I thought: “Maybe it’s TLC. I should replace this tla2tools file with the one TLA+ Toolbox uses.” It didn’t work.

Am I missing something?

I’d like to do a clean install this time. A full uninstallation doesn’t seem to happen through sudo apt purge tla+toolbox because, when reinstalling the Toolbox through a .deb file, it seems to remember all my previous settings. Shouldn’t the settings be removed along the Toolbox when uninstalling?

I hope this isn't confusing…

Best,

Jones

​

[Markus Kuppe]

Hi Jones,

the Toolbox saves its settings in your user director in the '.tlaplus/' folder. The Toolbox does *not* use 'tla2tools.jar' but the classes in 'plugins/org.lamport.tlatools_1.0.0.202204200054' relative to the Toolbox installation directory. However, the classes should be the same.

Is it possible that the Toolbox model has 'Init' and 'Next' under "What is the behavior spec?" on the "Model Overview" page? At the same time, do you check 'SPECIFICATION Spec' on the command line? If that is not the case, let's move the discussion to 'https://github.com/tlaplus/tlaplus/issues’.

Markus

> On May 7, 2022, at 4:49 PM, Jones Martins <jone...@gmail.com> wrote:
>
> Hi everyone,
>
> In summary:
>
> • Where does the Toolbox save its settings?
> • Does the Toolbox run tla2tools.jar from /opt/TLA+Toolbox/tla2tools.jar?
>
>

[Jones Martins]

Hi Markus,

It was the case, funnily enough. I tested Init and Next in the Toolbox, and Spec in the terminal.

Yet, when I wrote "Spec" in the "Temporal Formula" text box, the same problem happened. Nothing changed.

I'll create an issue on GitHub where I can share the spec as well. I still find it likely to be an error on my part, anyway.

Thank you!

Jones

--
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/k6tw6sf-uDU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/26F1F898-EF96-4419-B4E2-4577DFE01631%40lemmster.de.