TLA tools

[Michel Charpentier]

The command-line tools do not seem to be working with Java 9 or 10 (on MacOS).  Are the developers aware of that?  Is there a plan for a fix?

MC

[Markus Kuppe]

Hi Michel,

can you please be more specific of what does not work?

For model checking, I can successfully run TLC on macOS 10.13.6 with
Oracle Java 10.0.2 via the following command:

java --add-modules=java.activation -cp /path/to/tla2tools.jar tlc2.TLC
MC.tla

Thanks
Markus

[Michel Charpentier]

Thanks for the help.  Adding --add-modules solves the problem.  Is this documented anywhere?

As a side note, is there a way to run the TLC from the Toolbox using the command-line?  Why the need for a separate program?

MC

[Markus Kuppe]

On 06.09.2018 04:58, Michel Charpentier wrote:
> Thanks for the help.  Adding --add-modules solves the problem.  Is this
> documented anywhere?
>
> As a side note, is there a way to run the TLC from the Toolbox using the
> command-line?  Why the need for a separate program?
>

Hi Michel,

the next Toolbox won't require users to add
"--add-modules=java.activation" on Java 9 onward anymore (see [1]).


Assuming I understand your question correctly, you can run command-line
TLC also from a Toolbox installation. Let /opt/TLA+Toolbox be the path
to the Toolbox installation on Linux :

java -cp /opt/TLA+Toolbox/plugins/org.lamport.tlatools_[0-9.]*/ tlc2.TLC ...

For macOS and the Toolbox installed to /Applications:

java -cp /Applications/TLA+\
Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_[0-9.]*/
tlc2.TLC ...

For Windows:

java -cp (get-item 'C:\Program
Files\TLA+Toolbox\plugins\org.lamport.tlatools_*') tlc2.TLC ...


We provide tla2tools.jar for users who do not want to download the full
Toolbox.

Thanks
Markus

[1]
https://github.com/tlaplus/tlaplus/commit/c99791e8e079af50cae3d828cd849410e43c7ce0

[Michel Charpentier]

I'm now running into difficulties with Java 11.  Is any TLC (command-line or toolbox) supposed to be working with Java 11?

[Markus Kuppe]

On 15.11.18 05:34, Michel Charpentier wrote:
> I'm now running into difficulties with Java 11.  Is any TLC
> (command-line or toolbox) supposed to be working with Java 11?

Hi Michel,

Java 11 hasn't been tested extensively and for now I would advise to
keep using Java 1.8.  That said, TLC and SANY both work with Oracle Java
11.0.1 x86_64 here.

What difficulties do you actually see?

Thanks

Markus

[Markus Kuppe]

Can you please also check if the current nightly build [1] fixes your
incompatibility issues?

Thanks
Markus

[1] https://tla.msr-inria.inria.fr/tlatoolbox/ci/dist/

[Michel Charpentier]

Command-line tools work with Java 11 using the build you pointed to.  As for the toolbox, I edited the Info.plist to use Java 10 (it won't start at all on Java 11).

Thanks,

MC

[Markus Kuppe]

On 16.11.18 08:13, Michel Charpentier wrote:
> Command-line tools work with Java 11 using the build you pointed to.  As
> for the toolbox, I edited the Info.plist to use Java 10 (it won't start
> at all on Java 11).

Hi Michel,

you might also want to give the nightly Toolbox build a try with Java 11
[1].


In the long run we want to bundle the Java VM with the Toolbox
installation to avoid future version mismatches.

Thanks
Markus

[1]
https://tla.msr-inria.inria.fr/tlatoolbox/ci/products/TLAToolbox-1.5.7-macosx.cocoa.x86_64.zip

[Markus Kuppe]

On 16.11.18 11:42, Markus Kuppe wrote:
> you might also want to give the nightly Toolbox build a try with Java 11
> [1].

Hi Michel,

today's nightly build fixes [1] the Toolbox's Java 11 incompatibility.

Thanks
Markus

[1]
https://github.com/tlaplus/tlaplus/commit/96b4ea1c0bf60d930c856204da42f2b21f6858c3