TLA+

Citations

The TLA+ Home Page

Specifying Systems

TLA+ is a high-level language for modeling programs and systems, especially concurrent and distributed ones. TLA+ is particulary effective at revealing concurrency errors, ones that arise through the interaction of ascynchronous components. TLA+ comes with several tools, including

• SANY Syntactic Analyzer (which checks syntactic correctness)
• TLC Model Checker
• TLAPS Proof System

VS Code extension for TLA+

The TLA+ Video Course. A quite good introduction to TLA+.

Examples

How to run

Download tla2tools.jar from github.

Invoke the TLC model checker

java -cp tla2tools.jar tlc2.TLC

Invoke the Syntactic Analyzer

java -cp tla2tools.jar tla2sany.SANY

Translate PlusCal to TLA+

java -cp tla2tools.jar pcal.trans

Getting started

See the Channel example. Note that THEOREM statements are not checked by the TLC. They merely serve as a documentation.

The input to TLC consists of a TLA+ module, a .tla file, and a configuration file, a .cfg file.

A module begins with four or more dashes (-), followed by zero or more space characters, followed by a keyword MODULE. A module ends with four or more equals (=). All characters that precede the beginning of a module is ignored. Four or more dashes are purely cosmetic and can be used as separators for readability.

Notations

f.prof is an abbreviation for f["prof"].

[ f EXCEPT !.prof = "Red" ]
UNCHANGED <<a,b,c>>
INSTANCE TCommit