Getting Started
Relevant source files
The following files were used as context for generating this wiki page:This repository is a collection of TLA⁺ specifications and models covering applications in various fields. It serves as a comprehensive example library for learning TLA⁺, a diverse corpus for developing and testing TLA⁺ language tools, and a set of case studies on the application of formal specification. All specifications are located in the specifications directory.
Sources: README.md:7-12
This guide will walk you through exploring the existing specifications, running them with the TLA⁺ tools, and contributing your own examples to the collection.
Exploring the Examples
The primary way to explore the available specifications is through the "Validated Examples" table in the main README.md file. This table provides a high-level overview of each specification.
Sources: README.md:21-22
Understanding the Examples Table
The table summarizes key features of each specification, indicating which tools can be used for verification.
| Column | Description |
|---|---|
| Name | The name of the specification, linked to its directory. |
| Author(s) | The original author(s) of the specification. |
| Beginner | A checkmark (✔) indicates the spec is suitable for TLA⁺ newcomers. |
| TLAPS Proof | A checkmark (✔) indicates the spec includes a formal proof checkable by the TLA⁺ Proof System (TLAPS). |
| PlusCal | A checkmark (✔) indicates the spec includes a PlusCal variant. (✔) means it's an additional variant, while a plain ✔ means it uses PlusCal exclusively. |
| TLC Model | A checkmark (✔) indicates the spec can be verified using the TLC model checker. |
| Apalache | A checkmark (✔) indicates the spec can be verified using the Apalache model checker. |
Sources: README.md:14-19, README.md:23-94
Detailed Specification Metadata
For more detailed information, each specification directory contains a manifest.json file. You can search these files to find examples with specific features.
This diagram shows how to find a specification with a desired feature.
Sources: README.md:21-31
For example, to find specs that use the VIEW feature in their models, you can run a command like ls specifications/*/*.cfg | xargs grep -l VIEW.
Sources: README.md:33-34
Running a Specification
To run and check the specifications, you need to install the TLA⁺ Toolbox. The recommended version is a pre-release build available from the nightly products page, as it contains the latest features.
Sources: specifications/PaxosHowToWinATuringAward/README.txt:19-27
Setup and Execution Flow
The following diagram illustrates the steps to open and run a model check on a specification using the TLA⁺ Toolbox.
This process allows you to verify the properties of the algorithm defined in the specification. For instance, the MultiPaxos_MC.cfg model can be run to check for linearizability and deadlocks.
Sources: specifications/PaxosHowToWinATuringAward/README.txt:29-34, specifications/MultiPaxos-SMR/README.md:8-9, specifications/PaxosHowToWinATuringAward/README.txt:51-54
Contributing a Specification
Contributions of new TLA⁺ specifications are highly appreciated. They serve as valuable examples and real-world test cases for TLA⁺ tooling.
Sources: CONTRIBUTING.md:3-6
Basic Contribution Steps
- Fork the repository.
- Create a new directory under
specificationsfor your spec. - Place all TLA⁺ (
.tla) and model configuration (.cfg) files in the directory. - Include a
README.mdfile explaining the specification. - (Optional) To skip automated validation, add your spec's directory to the
.ciignorefile.
Sources: CONTRIBUTING.md:14-25
Adding to Continuous Integration (CI)
For your specification to be fully integrated and validated, you must add it to the CI system. This involves creating a manifest.json file and updating the main README.md table.
The contribution workflow is summarized below.
A helper script is available to automate most of the manifest.json generation.
# First, setup a python environment and install dependencies
pip install -r .github/scripts/requirements.txt
# Then, run the generation script
python .github/scripts/generate_manifest.py
After running the script, you must manually fill in fields like sources, authors, tags, and model runtimes in the generated manifest.json.
Sources: CONTRIBUTING.md:46-52
Development and CI Scripts
For advanced users and maintainers, the repository includes a suite of Python scripts for local development and CI validation. These scripts ensure that all specifications adhere to the repository's quality standards.
Sources: DEVELOPING.md:6-7
CI Validation Pipeline
The CI workflow runs a series of validation scripts in a specific order to check everything from manifest correctness to model execution.
This diagram shows the sequence of CI validation scripts.
Sources: DEVELOPING.md:9-30
Key Scripts
| Script | Purpose |
|---|---|
check_manifest_schema.py | Validates manifest.json files against the schema. |
check_manifest_files.py | Ensures manifest entries match the actual files in the specifications directory. |
check_manifest_features.py | Verifies that features (pluscal, proof, etc.) are correctly recorded in the manifest. |
check_markdown_table.py | Validates the format and content of the README.md spec table against the manifests. |
parse_modules.py | Runs the SANY parser on all .tla files to check for syntax and semantic validity. |
check_small_models.py | Runs TLC or Apalache on models expected to complete within 30 seconds. |
smoke_test_large_models.py | Runs larger models for 5 seconds to ensure they don't crash immediately. |
check_proofs.py | Runs TLAPM against all modules containing formal proofs. |
Sources: DEVELOPING.md:10-30
You can run these scripts locally for a faster development loop. Instructions for setting up the environment and executing each script are detailed in DEVELOPING.md.
Sources: DEVELOPING.md:78-81