Re: [tlaplus] TLA tools

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

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