tla2tools 1.7.1-0.6932e19 TLA+ tools (analyzer, TLC, TLATeX, PlusCal translator)

TLA+ is a high-level language for modeling programs and systems---especially concurrent and distributed ones. It's based on the idea that the best way to describe things precisely is with simple mathematics. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.

The following TLA+ tools are available in this distribution:

  • The Syntactic Analyzer: A parser and syntax checker for TLA+ specifications;

  • TLC: A model checker and simulator for a subclass of "executable" TLA+ specifications;

  • TLATeX: A program for typesetting TLA+ specifications;

  • Beta test versions of 1-3 for the TLA+2 language; and

  • The PlusCal translator.