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

Re: [tlaplus] TLA+ Toolbox issues?



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 <jonesmvc@xxxxxxxxx> wrote:
> 
> Hi everyone,
> 
> In summary:
> 
> 	• Where does the Toolbox save its settings?
> 	• 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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/26F1F898-EF96-4419-B4E2-4577DFE01631%40lemmster.de.