A session on the EECS Linux servers:
> tlaplus_repl160
-------------------------------------------------------------------------------------
Welcome to the TLA+ REPL! This REPL uses the TLC model checker
to evaluate TLA+ expressions interactively. It is meant as an
aid for learning TLA+ and debugging TLA+ specs.
-------------------------------------------------------------------------------------
(TLA+REPL) >>> 3*4
12
(TLA+REPL) >>> {x*2: x \in 1 .. 5}
{2, 4, 6, 8, 10}
(TLA+REPL) >>> CHOOSE x \in 1..4: x > 3
4
(TLA+REPL) >>> quit
Goodbye!
Here is the script:
>more /cs/local/bin/tlaplus_repl157 #!/bin/sh tlatools=/eecs/local/pkg/tla-1.5.7 # Set Java CLASSPATH correctly. export CLASSPATH=$tlatools:$CLASSPATH python /eecs/local/pkg/tlaplus_repl/tla_repl.py