TLA+ Tools (original) (raw)

| Leslie Lamport Last modified on 18 March 2022 | | | ------------------------------------------------- | |

Most users of TLA+ will run the TLA+ tools from the TLA+ Toolbox. How to download them and run them outside the Toolbox is explained here.

The Tools

SANY Syntactic Analyzer [show]

A parser and syntax checker for TLA+ specifications. It catches parsing errors and some semantic errors such as priming an expression containing primed variables. It was written by Jean-Charles Gr�goire, David Jefferson, and Yuan Yu.

TLC Model Checker [show]

A model checker and simulator for executable TLA+ specifications, which include most specifications written by engineers. It is an explicit-state model checker that can check both safety and liveness properties. For safety checking, TLC achieves an approximately linear speedup on modern large computers using 32 or more cores. It can further speed up model checking by running on a network of computers, and provides easy deployment on cloud systems. TLC was written by Yuan Yu and extended by Markus Kuppe.

Apalache Model Checker [show]

PlusCal Translator [show]

A translator from the PlusCalalgorithm language to TLA+. It was written by Keith Marzullo and the author of this web page.

TLAPS Proof System [show]

TLATeX Pretty-Printer [show]

A program for typesetting TLA+ specifications. It is used by the Toolbox's Produce PDF Version command to generate and display a pdf file with a pretty-printed version of a specification. Chapter 13 of Specifying Systemshas some tips on formatting this version. TLATeX can also be used outside the Toolbox to include TLA+ formulas and PlusCal code as part of a LaTeX document. Click here to find out how to run TLATeX outside the Toolbox. Here are instructions for how to include TLA+ formulas and PlusCal code in a LaTeX document. You will have to download the <tlatex.sty>package file to use TLATeX with LaTeX.

Documentation

Except for the PlusCal translator and TLAPS, the tools are described in the bookSpecifying Systems. Documentation of the PlusCal translator can be found here. Some documentation of the TLAPS proof system can be found on its web site and in the TLA+ Hyperbook.

The current versions of the language and tools differ somewhat from the ones described in the book. Most notably, language constructs for writing proofs have been added to TLA+, and a number of features have been added to TLC. All significant changes to the tools since the book was written are described in the document Current Versions of the TLA+ Tools, which contains a complete list of TLC command-line options. Changes to the language are described inthis web page.

Known bugs in the tools are reported on the TLA+Github issues page. Requests for additional features are also posted there. Tell us about any problems or inadequacies you find with the tools. But please remember that we are a small number of people trying to respond to the needs of an ever-growing number of users.