CSE 128 Spring 2004
Running the TLA+ Tools
There are three TLA+ tools: a syntax analyzer (tla), a model
(tlc), and a typesetter (tlatex). To use these tools,
either execute prep cs128s when you log in or add the
following line to your .login file:
set path = ( $path /home/solaris/ieng9/cs128s/public/bin )
The first two tools are simple to use.
The last tool is more complex. You can get a brief introduction using
- To check the syntax of a specification Foo.tla, type
- To model check Foo.tla using Foo.cfg, type
and can get more information on the tool using
Note that the help information asks you to run java
tlatex.TLA, but the script tlatex does this for you; you
only need to type tlatex [options] [inputFile].
I am placing the specifications that we cover in class in the
As a simple warmup exercise, copy Game.tla
Game.cfg into your home directory, and try running tlc
on the specification. You'll see that there's a bug in the
specification. Figure out what the problem is (the tool's output will
give you a good hint), fix the specification, and try again. There
will be another bug, so fix that, too. On the third try, you should be
able to pass tlc.