Re: [tlaplus] Open an existing spec - does it work in the TLA+ Toolbox?

Hi Tatiana,

It is misleading but you can use "File > Open Spec > Add New Spec" to open an existing spec, just browse to it.

The "Open" item in the context menu is only related to which spec is "active" in the Spec Explorer, so selecting MissionariesAndCannibals then right-clicking and selecting open will expand the spec.

hope this helps

On Mon, Feb 19, 2024 at 1:53 PM Tatiana Racheva <tatiana.racheva@xxxxxxxxx> wrote:

I found a discussion from 2014 that indicates this was a problem in the past but that it has since been fixed. But, in 2024, I seem to have this problem again.

The only thing I can do is create a new module, either using the File->Open Spec... menu options, or the Spec Explorer.

I'm on Ventura 13.5.2. My TLA+ Toolbox is `Version 1.7.1 of 31 December 2020`.

`java --version` prints:

openjdk 21.0.2 2024-01-16 LTS

OpenJDK Runtime Environment Temurin-21.0.2+13 (build 21.0.2+13-LTS)

OpenJDK 64-Bit Server VM Temurin-21.0.2+13 (build 21.0.2+13-LTS, mixed mode)

--
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/a9f563d3-461d-49d4-aea7-1a887383a702n%40googlegroups.com.