The TLA+ Syntactic Analyzer

Last modified 13 January 2003

What is SANY?

SANY is a parser and semantic analyzer for the TLA+ specification language.   It was written by Jean-Charles Grégoire and David Jefferson, with help from Yuan Yu.   See the TLA web page or the book Specifying Systems to find out about TLA and TLA+.   Please report bugs to Leslie Lamport.

The Current Version

The version on the Microsoft Research site is Version 0.99. See the main TLA+ tools page for how it differs from the version described in Specifying Concurrent Systems .

How to install SANY

See the main TLA+ tools page for instructions on how to install Sany.

How to run SANY

To run SANY on a file  spec.tla , you can use the following command:
     java tlasany.SANY spec  
The extension .tla is implied, and may be present or absent.