Software Engineering Documentation

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.

====== TLA+_REPL ======

[[https://github.com/will62794/tlaplus_repl|github source]]

A session on the EECS Linux servers:

<code>
> 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!

</code>

Here is the script:
<code>
>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
</code>

Software Engineering Documentation

User Tools

Site Tools

Page Tools