Setting Up TLA+ Tools on OS X

tla (1)

A coworker, Mark Z., has been on a TLA+ kick, and has gotten me cautiously optimistic about the idea as well.

After reading through most of the TLA+ Book (it's freely available for download), the next step was to actually start writing and model checking some TLA of my own, which meant I needed to setup the [TLA+ Tools].

The setup turned out to be rather straightforward, but figured I would briefly jot them down anyway.

  1. Download the tools from the Microsoft Research site.

  2. Unzip the file into ~/tla/.

  3. Update the CLASSPATH for your shell:

    emacs ~/.bash_profile

    Add this line to your configuration file:

    export CLASSPATH="$CLASSPATH:/Users/<USERNAME>/tla"

    Then re-source the file:

    source ~/.bash_profile

At this point the installation is finished, and you can run the TLC model checker on the examples:

cd ~/tla/examples/AsynchronousInterface
java tlc.TLC AsynchInterface.tla

The output of which should look like:

TLC Version 2.01 of April 9, 2008
Model-checking
Parsing file AsynchInterface.tla
Parsing file /Users/lethain/tla/tlasany/StandardModules/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module AsynchInterface
Finished computing initial states: 6 distinct states generated.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
    calculated (optimistic):  1.1709383462843448E-17
    based on the actual fingerprints:  7.43635344891595E-18
30 states generated, 12 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 2.

You can also use the TLATeX tool for generating LaTeX output:

java tlatex.TLA AsynchInterface.tla

Which generates the LaTeX for this file:

TLA Example

The other tools seem to work correct as well. Hopefully they'll work for you as well.

(I happen to be using TeXShop for compiling LaTeX, which seems to work adequately, but I lack the LaTeX perspective to recommend it over any other existing solutions.)