CSE 128 Spring 2004: Running the TLA+ Tools

CSE 128 Spring 2004
Running the TLA+ Tools

There are three TLA+ tools: a syntax analyzer (tla), a model checker (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.

To check the syntax of a specification Foo.tla, type tla Foo.
To model check Foo.tla using Foo.cfg, type tlc Foo.

The last tool is more complex. You can get a brief introduction using

tlatex -help

and can get more information on the tool using

tlatex -info

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 directory /home/solaris/ieng9/cs128s/public/spec/.

As a simple warmup exercise, copy Game.tla and 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.