Model Checking with TLC
Relevant source files
The following files were used as context for generating this wiki page:TLC is the model checker for TLA⁺ and is a primary verification tool used throughout this repository. It is used to check TLA⁺ specifications for correctness by exploring the state space of the system model. This includes verifying safety properties (invariants), liveness properties, and checking for deadlocks. The repository is configured to use TLC extensively within its Continuous Integration (CI) pipeline to automatically validate the included specifications.
The examples in this repository demonstrate various applications of TLC, from checking simple puzzles to verifying complex distributed algorithms. Users are encouraged to run TLC on the provided models to understand the algorithms and to gain familiarity with the tool. A key goal is to write a correct spec where TLC reports an error in the algorithm, which is then confirmed by examining the generated error trace.
Sources: README.md:14, specifications/PaxosHowToWinATuringAward/README.txt:38-41, 50-54
Running TLC Models
To run the TLC model checker on a specification, you typically use the TLA⁺ Toolbox. The general workflow involves creating a new specification, selecting the root .tla module, and importing any existing models associated with it. Each model is defined by a .tla file and a corresponding .cfg configuration file.
Sources: specifications/PaxosHowToWinATuringAward/README.txt:28-33
The following diagram illustrates the typical user workflow for checking a model with TLC via the TLA⁺ Toolbox.
Configuration
TLC models are configured using .cfg files. These files specify what specification to check, which properties (invariants, liveness) to verify, and any constraints or symmetries to apply, which can significantly reduce the state space.
Sources: CONTRIBUTING.md:15, README.md:40
Common Configuration Keywords
The repository's .cfg files use several standard TLC keywords to define the model checking parameters.
| Keyword | Description |
|---|---|
SPECIFICATION | Defines the main specification to be checked. |
INVARIANT | Specifies safety properties that must hold in every reachable state. |
PROPERTY | Specifies temporal (liveness) properties that the model must satisfy. |
CONSTRAINT | Adds constraints on variables to prune the state space. |
SYMMETRY | Declares model symmetries to reduce the state space explored by TLC. |
VIEW | Defines a mapping of the state space, used for abstracting away details. |
ALIAS | Creates an alias for a lengthy expression. |
DEADLOCK | Instructs TLC to check for deadlock (states with no successors). |
Sources: README.md:40-41
Continuous Integration (CI) Validation
The repository uses a CI pipeline to automatically validate all TLA⁺ specifications. This process involves running TLC on the models associated with each spec to ensure they parse correctly, do not crash, and produce the expected results.
Sources: CONTRIBUTING.md:10, DEVELOPING.md:8
The CI process distinguishes between small and large models based on their expected runtime, which is specified in the manifest.json file for each spec.
- Small Models: Models with an expected runtime of less than 30 seconds are run to completion. The CI script checks that the model's result (e.g., success, safety failure) matches the expected outcome defined in the manifest. For successful exhaustive searches, it also verifies the number of distinct states, total states, and state depth.
- Large Models: Models expected to take longer than 30 seconds are "smoke-tested" by running them for five seconds to ensure they do not crash immediately.
Sources: CONTRIBUTING.md:58-59, DEVELOPING.md:25-31
This diagram shows the CI workflow for checking TLC models.
Sources: DEVELOPING.md:25-31
Model Metadata (manifest.json)
Each specification directory contains a manifest.json file that stores metadata used by the CI scripts. For TLC models, this file records configuration details, expected runtime, and verification results.
Sources: CONTRIBUTING.md:36, DEVELOPING.md:10
Model Attributes
The models array in manifest.json contains objects with the following key attributes for TLC models:
| Field | Description |
|---|---|
path | The file path to the model's .cfg file. |
runtime | The approximate runtime on an ordinary workstation in "HH:MM:SS" format. |
mode | The checking mode. Can be "exhaustive search", {"simulate": {"traceCount": N}}, or "generate". |
result | The expected outcome of the model check. |
distinctStates | (Optional) The number of distinct states found by TLC. |
totalStates | (Optional) The total number of states explored by TLC. |
stateDepth | (Optional) The maximum depth of the state graph. |
Sources: CONTRIBUTING.md:56-66
The result field can have one of the following values:
"success": The model completes successfully without any violations."safety failure": The model violates an invariant."liveness failure": The model fails to satisfy a liveness property."deadlock failure": The model encounters a deadlock."assumption failure": The model violates an assumption.
Sources: CONTRIBUTING.md:60-64, README.md:38-39
Below is an example of a model entry from a manifest.json file.
{
"path": "specifications/TLC/TestGraphs.cfg",
"runtime": "00:00:05",
"mode": "exhaustive search",
"result": "success",
"distinctStates": 2790,
"totalStates": 2990,
"stateDepth": 52
}
Sources: specifications/TLC/manifest.json:15-23
Advanced Usage
Statistical Analysis via Simulation
TLC's simulator can be used to generate random execution traces. This is useful for inferring statistical properties of a system that cannot be expressed in standard TLA⁺. For example, the ewd998 specification uses simulation to compare the efficiency of different algorithmic variants by measuring properties like the number of steps between system termination and its detection.
Sources: specifications/ewd998/README.md:31-39, 70-73
Trace Validation
TLC can be used to validate an execution trace from a real implementation against a high-level TLA⁺ specification. This involves defining TLC state and action constraints that match each event in the implementation's log file to a state in a behavior defined by the high-level spec. A trace is considered valid if TLC can match every log entry to a corresponding state transition in the model. This technique is a powerful way to bridge the gap between abstract specification and concrete implementation.
Sources: specifications/ewd998/EWD998ChanTrace.md:23-30
Conclusion
Model checking with TLC is a cornerstone of the quality assurance process in the Examples repository. It provides a robust framework for verifying the correctness of TLA⁺ specifications, from simple algorithms to complex distributed systems. The integration of TLC into the CI pipeline ensures that all contributed specifications are continuously validated, maintaining a high standard of quality and reliability. The repository serves as a rich collection of practical examples for developers looking to apply TLC to their own projects.
Sources: README.md:8-11, CONTRIBUTING.md:6-9