TLC -- The TLA+ Model Checker

Leslie Lamport and Yuan Yu
Microsoft Research
Mountain View, California

Last modified 14 June 2011 

TLC is a model checker for specifications written in TLA+.  TLA+ is a specification language based on TLA, the Temporal Logic of Actions.  See the TLA web page for general information about TLA.  

You will most likely want to use TLC from the TLA Toolbox.  Downloading the Toolbox brings with it the latest version of all the TLA+ tools, including TLC.  How to write TLA+ specifications is explained in Specifying Concurrent Systems , which also describes TLC.  However, it doesn't tell you how to use the Toolbox.

TLC contains a number of features that are available as command-line options and are documented only in the code and on this web page.  Command-line options can be specified in the Toolbox on the TLC Options section of a model's Advanced Options page.

If for some reason you want to run TLC from outside the Toolbox, see the main TLA+ tools page for instructions on how to obtain, install, and run TLC.