October 31, 2009.
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.
Download the tools from the Microsoft Research site.
Unzip the file into
CLASSPATH for your shell:
Add this line to your configuration file:
Then re-source the file:
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:
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.)