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.
