Advanced TLC Configuration
Relevant source files
The following files were used as context for generating this wiki page:Within the TLA⁺ Examples repository, the TLA⁺ model checker (TLC) is used not just for basic verification but also for advanced tasks such as statistical analysis, implementation trace validation, and performance regression testing. This is achieved through detailed model configurations specified in .cfg files, which are further described by manifest.json metadata files for integration with the project's automated CI pipeline.
Advanced configurations allow TLC to operate in different modes, including exhaustive search, simulation, and trace generation. These configurations leverage specific keywords and constraints to guide TLC's execution, enabling sophisticated analysis that goes far beyond standard safety and liveness checking. The EWD998 specification serves as a primary example of these advanced techniques, demonstrating how to use TLC for statistical property inference and for validating a Java implementation against the formal specification.
Core Configuration Concepts
TLC's behavior for a given TLA⁺ specification is controlled by a model configuration file, which has a .cfg extension. These files define what properties to check, what constraints to apply, and how to initialize constants and variables.
Sources: README.md:33-34, CONTRIBUTING.md:16-19
The .cfg File
The .cfg file is central to running TLC. It specifies the root .tla module, the invariants and properties to be checked, and any constraints on the state space. The repository encourages contributors to include at least one model that completes quickly and, if possible, one that fails in an interesting way.
Sources: CONTRIBUTING.md:13-15
The following diagram illustrates the relationship between the specification, the configuration file, and a TLC execution.
This diagram shows that both the TLA+ specification and a model configuration file are inputs to the TLC model checker.
Key .cfg Keywords
The README.md suggests searching .cfg files for several keywords that indicate the use of advanced TLC features.
| Keyword | Description |
|---|---|
SYMMETRY | Defines a symmetry set to reduce the state space explored by TLC. |
VIEW | Maps a complex state function to a simpler value, used for state comparison. |
ALIAS | Creates a named substitution for a value, which can be useful for regression testing. |
CONSTRAINT | Adds a state constraint, pruning parts of the state space from exploration. |
ACTION_CONSTRAINT | Adds an action constraint, pruning specific state transitions. |
DEADLOCK | Instructs TLC to check for deadlock (states with no possible next state). |
Sources: README.md:33-34
Model Checking Modes
TLC can be run in several modes, which are specified in the manifest.json file for each model. This metadata is used by the CI system to determine how to run the model and what result to expect.
Sources: CONTRIBUTING.md:61-65
Exhaustive Search
This is the default mode where TLC attempts to explore every reachable state. The manifest.json file records the expected result, which can be success, safety failure, liveness failure, deadlock failure, or assumption failure. For successful runs, state space metrics are often recorded to act as a regression test for TLC itself.
Sources: CONTRIBUTING.md:62, CONTRIBUTING.md:66-73
An example from acp/manifest.json for an exhaustive search model:
{
"path": "specifications/acp/ACP_NB_TLC.cfg",
"runtime": "00:00:01",
"mode": "exhaustive search",
"result": "success",
"distinctStates": 4284,
"totalStates": 23988,
"stateDepth": 19
}
Sources: specifications/acp/manifest.json:17-25
Simulation Mode
For specifications with very large or infinite state spaces, TLC can be run in simulation mode. In this mode, TLC generates a specified number of random execution traces. This is particularly useful for statistical analysis of an algorithm's behavior under different conditions, as demonstrated in the EWD998 specification. The manifest.json entry for a simulation model specifies the number of traces to generate.
Sources: specifications/ewd998/README.md:25-30, CONTRIBUTING.md:63
The EWD998_opts specification uses simulation to measure the efficiency of four different variants of the termination detection algorithm by generating random traces and analyzing statistical properties, such as the number of steps between termination and its detection.
Sources: specifications/ewd998/README.md:73-82
Trace Validation
A powerful, advanced use of TLC is to validate an execution trace (e.g., a log file) from a real implementation against a high-level TLA⁺ specification. The EWD998ChanTrace.md file documents this process in detail. The core idea is to use TLC's state and action constraints to ensure that each step in the implementation's trace corresponds to a valid state transition in the TLA⁺ model.
This technique is effective for finding subtle divergences between the specification and the implementation. For example, it helped identify a bug where the implementation did not allow a message to be sent from a node to itself, which was a constraint in the high-level spec.
Sources: specifications/ewd998/EWD998ChanTrace.md:21-31, specifications/ewd998/EWD998ChanTrace.md:83-86
The following diagram shows the general workflow for trace validation.
This diagram illustrates the process of using TLC to validate an implementation log against a formal specification.
Advanced Constraints and Operators
State and Action Constraints with TLCGet/TLCSet
The EWD998 specification demonstrates an advanced technique using action constraints (ACTION_CONSTRAINT) and the TLCGet/TLCSet operators. These operators allow state to be passed between TLC's evaluation of successive states in a trace, which is not possible with standard TLA⁺ variables.
In the EWD998_opts.tla spec, TLCSet(1, TLCGet("level")) is used in an action constraint AtTermination to record the state number (level) when the system terminates. Later, the AtTerminationDetected constraint retrieves this value using TLCGet(1) to calculate the number of steps between termination and its detection, writing the result to a CSV file.
Sources: specifications/ewd998/README.md:84-99
Example constraints from the EWD998 analysis:
AtTermination ==
IF EWD998!Termination # EWD998!Termination'
THEN TLCSet(1, TLCGet("level"))
ELSE TRUE
AtTerminationDetected ==
EWD998!terminationDetected =>
/\ ... CSVWrite("%1$s...%4$s", << ..., TLCGet("level") - TLCGet(1), ... >>)
/\ TLCSet(1, 0)
Sources: specifications/ewd998/README.md:85-99
Configuration for Continuous Integration (CI)
The CI system heavily relies on manifest.json files to automate the validation of all specifications. These files provide the necessary metadata for scripts to run TLC and check if the outcome matches the expected result.
Sources: DEVELOPING.md:10-14, CONTRIBUTING.md:36-41
The manifest.json File
For each specification, a manifest.json file lists all TLA⁺ modules and their associated models. For each model, it defines the expected runtime, checking mode, and result. This allows the CI script check_small_models.py to run TLC and automatically verify the model's correctness.
Sources: DEVELOPING.md:20-24, CONTRIBUTING.md:46-50
The CI process for model checking is depicted below.
This diagram shows the sequence of events when a user pushes changes, triggering a CI workflow that uses TLC and manifest files to validate the models.
Conclusion
Advanced TLC configuration in this repository elevates TLC from a simple model checker to a multifaceted analysis tool. By leveraging .cfg files with features like SIMULATION, CONSTRAINTS, and SYMMETRY, developers can perform statistical analysis, validate implementation traces, and optimize model checking. The integration with the CI pipeline via manifest.json files ensures that all specifications remain correct and that their expected behaviors are continuously verified, turning the collection of examples into a robust and reliable corpus for the TLA⁺ ecosystem.
Sources: README.md:6-9, DEVELOPING.md:6-9