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

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

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)

Screenshot 2024-02-18 at 3.58.55 PM.png

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.