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:
java tlc.TLC AsynchInterface.tla
The output of which should look like:
TLC Version 2.01 of April 9, 2008
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.)