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

[Tatiana Racheva <tatiana.racheva@xxxxxxxxx>]

Oh goodness. I think this works if you provide the spec name that isn't the same as the one that's already there.

If, in the browse dialog, I specify the correct filename, it warns that it'll be replaced. But then, it doesn't always happen, and I haven't figured out the exact steps that lead to the warning and those that don't.

So, I chose a different name.

I changed the filename in the previous menu and changed the "Specification Name" field to match the one in the TLA file.

But now, the model is not in the view (even though "Include models" is checked).

The first time I tried this successfully, the model was included, but somehow I don't remember what exactly I clicked on and in what order.

This is non-deterministic and a crazy experience! Kind of ironic :)

On Sunday, February 18, 2024 at 10:28:10 PM UTC-8 Morgan Weetman wrote:

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...@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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a9f563d3-461d-49d4-aea7-1a887383a702n%40googlegroups.com.

-- 
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/8ced83c6-2605-4d69-9076-97dddc5810c8n%40googlegroups.com.