User Tools

Site Tools


tla:repl:start

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
tla:repl:start [2018/08/30 17:25]
jonathan
tla:repl:start [2019/08/26 02:11] (current)
jonathan
Line 1: Line 1:
 ====== TLA+_REPL ====== ====== TLA+_REPL ======
  
-<​code>​+[[https://​github.com/​will62794/​tlaplus_repl|github source]]
  
-tlaplus_repl157+A session on the EECS Linux servers: 
 + 
 +<​code>​ 
 +> tlaplus_repl160
 ------------------------------------------------------------------------------------- -------------------------------------------------------------------------------------
  ​Welcome to the TLA+ REPL! This REPL uses the TLC model checker  ​Welcome to the TLA+ REPL! This REPL uses the TLC model checker
Line 18: Line 21:
 Goodbye! 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>​ </​code>​
tla/repl/start.1535649911.txt.gz · Last modified: 2018/08/30 17:25 by jonathan