How to launch clean IDE

[Daniel Espinosa]

Hi all

I've seen videos showing how automagically IDE starts in clear, init state, i.e., no need to specify a .tla or .cfg file as opposite running the CLI tools.

But nowhere says how to launch the IDE

I've installed everything the latest on Ubuntu, installing in default paths:

sudo ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin

unzip TLAToolbox-1.7.1-linux.gtk.x86_64.zip

sudo cp cvc4-1.8-x86_64-linux-opt /usr/local/lib/tlaps/cvc4

But all my attempts to run

java -XX:+UseParallelGC -jar ./tla2tools.jar tlasany.SANY

or tlc.TLC or whatever else asks for a .tla and a .cfg

I know I need to read a chapter of Specifying Systems to learn how to create a .cfg, I have a .tla file but fails (maybe some syntax failure)

I'm not  asking about how to fix my first .tla file

I just want to know how to launch the IDE, clean state i.e., without a preexisting tla file.

Old and even newer videos like this https://www.google.com/search?channel=fs&client=ubuntu-sn&q=beginning+with+tla%2B+tools#fpstate=ive&vld=cid:48fee981,vid:U2FAnyPygrA

they show that starting IDE without preexisting file is possible, but how?

I think should be

java -XX:+UseParallelGC -jar ./tla2tools.jar  <something_here>

but exactly what, I don't know

Please help!

[Stephan Merz]

It looks like you are starting the TLC command-line tools such as SANY or TLC. There are two IDEs with support for TLC: in the videos you will have seen the TLA+ Toolbox [1] (a stand-alone Eclipse application), but there is also a VS Code Extension [2] with support for TLC.

Hope this helps,

Stephan

[1] https://lamport.azurewebsites.net/tla/toolbox.html

[2] https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ec69088c-be1c-409e-9223-b898966e3f27n%40googlegroups.com.

[J.D. Meadows]

Is there a way to clean the files generated by past model checking runs?. I don't want them cluttering my machine, and I'd also like to keep them out of version control.This is how the .gitignore I used as a template treats the toolbox folder:

# Exclude all files related to TLA+ Toolbox
# *.toolbox/**

# toolbox model metadata
*.toolbox/*.launch
*.toolbox/*.pmap

# TLA+ Toolbox model checking
*.toolbox/**/*.tla
*.toolbox/**/*.out   # model results
# *.toolbox/**/*.cfg # model config

I had to add additional lines to ignore the Model_* folders, but ideally would like to keep the bare minimum so that the eclipse project can be downloaded and works if other developers download it.

How can I manually clean a TLA+ Toolbox project? The Toolbox doesn't come with eclipse's 'clean project' option.