Skip to content

Instantly share code, notes, and snippets.

@ligurio

ligurio/tla.md

Last active Feb 12, 2018
Embed
What would you like to do?

Using TLA Plus on Ubuntu

Console

  • apt-get install -y java-common texlive-latex-base
  • Download TLA Tools (tla.zip) from https://github.com/tlaplus/tlaplus/releases
  • Unpack archive and add directory with content to a variable export CLASSPATH /home/sergeyb/Downloads/
$ java tlc2.TLC
$ java tla2sany.SANY
$ java pcal.trans
$ java tla2tex.TLA

TLA Toolbox

Running TLAPS

How to run the model checker in headless mode:

  • Download tla2tools.jar
  • Run the model checker once in TLA+ Toolbox on desktop (can be aborted once started). This generates the folder elasticsearch.toolbox/model/ that contains all model files that are required to run the model checker in headless mode.
  • Copy the above folder and tla2tools.jar to the server running in headless mode.
  • cd to the folder and run java -Xmx30G -cp ../tla2tools.jar tlc2.TLC MC -deadlock -workers 12. The setting -Xmx30G denotes the amount of memory to allocate to the model checker and -workers 12 the number of worker threads (should be equal to the number of cores on machine). The setting -deadlock ensures that TLC explores the full reachable state space, not searching for deadlocks.

Using TLA Plus on OpenBSD

  • Building TLA tools:
- pkg_add apache-ant
- git clone https://github.com/tlaplus/tlaplus/
- cd tlaplus
- export ANT_OPTS=-Xmx1g
- ant -f tlatools/customBuild.xml -Dmaven.test.halt=true compile compile-test dist test-dist
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment