Welcome to the TLA+ Examples Repository

Relevant source files

The following files were used as context for generating this wiki page:

• CONTRIBUTING.md
• DEVELOPING.md
• LICENSE.md
• README.md
• specifications/Chameneos/manifest.json
• specifications/Majority/manifest.json
• specifications/MultiPaxos-SMR/README.md
• specifications/PaxosHowToWinATuringAward/README.txt
• specifications/TwoPhase/manifest.json
• specifications/ewd998/README.md
• specifications/ewd998/EWD998ChanTrace.md

This repository contains a collection of TLA⁺ specifications and models covering a wide range of algorithms and systems. It serves three primary purposes: a comprehensive example library for learning TLA⁺, a diverse test 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. The repository is actively maintained, with a continuous integration (CI) system that validates all included examples to ensure they remain functional and relevant as TLA⁺ and its tools evolve.

Sources: README.md:5-14, CONTRIBUTING.md:4-7

Repository Structure

Each TLA⁺ example is contained within its own directory inside specifications. A standard specification directory includes TLA⁺ source files (.tla), model configuration files (.cfg), a descriptive README.md, and a crucial manifest.json metadata file.

Sources: README.md:13, CONTRIBUTING.md:16-17

This diagram illustrates the typical file structure for a single specification.

The manifest.json File

The manifest.json file is central to the repository's automation and organization. It provides structured metadata about each specification, which is used by the CI scripts to validate the spec's properties and contents. This file can be generated automatically using a provided script or created manually.

Sources: CONTRIBUTING.md:43-48, DEVELOPING.md:10-12

Key fields in the manifest.json include:

Field	Description	Example
sources	A list of URLs to relevant papers, blog posts, or other source materials.	["https://.../paper.pdf"]
authors	A list of the specification's authors.	["Leslie Lamport"]
tags	Keywords describing the spec, such as "beginner" or "ewd".	["beginner"]
modules	An array of objects, each describing a .tla file.	[...]
modules.path	The path to the .tla module file.	"specifications/Majority/Majority.tla"
modules.features	A list of features used in the module, like "pluscal" or "proof".	["pluscal"]
modules.models	An array of model configurations associated with the module.	[...]
models.path	The path to the .cfg model file.	"specifications/Majority/MCMajority.cfg"
models.runtime	Approximate runtime in HH:MM:SS format.	"00:00:05"
models.mode	The checking mode: "exhaustive search", "simulate", "generate", or "symbolic".	"exhaustive search"
models.result	The expected outcome, e.g., "success", "safety failure", "deadlock failure".	"success"
models.state_count	Optional state space information for regression testing.	{ "distinctStates": 2733, ... }

Sources: CONTRIBUTING.md:50-78, specifications/Majority/manifest.json

Below is an example snippet from a manifest.json file:

{
  "sources": [],
  "authors": [
    "Stephan Merz"
  ],
  "tags": [
    "beginner"
  ],
  "modules": [
    {
      "path": "specifications/Majority/MCMajority.tla",
      "features": [],
      "models": [
        {
          "path": "specifications/Majority/MCMajority.cfg",
          "runtime": "00:00:05",
          "mode": "exhaustive search",
          "result": "success",
          "distinctStates": 2733,
          "totalStates": 3459,
          "stateDepth": 6
        }
      ]
    }
  ]
}

Sources: specifications/Majority/manifest.json:1-26

Contributing a Specification

Contributions of new TLA⁺ specifications are highly encouraged. The process involves forking the repository, adding the new spec, and optionally integrating it with the CI system. All contributed specs are preferably licensed under the MIT License for consistency.

Sources: CONTRIBUTING.md:1-13, LICENSE.md:1-3

The following flowchart outlines the contribution process, from adding files to passing CI validation.

Continuous Integration (CI) and Development

The repository employs a robust CI pipeline to automatically validate every specification. This ensures correctness, consistency, and maintainability. The pipeline consists of a series of Python scripts that check everything from metadata format to model-checking results.

Sources: DEVELOPING.md:1-4, CONTRIBUTING.md:8-10

CI Validation Workflow

The CI process runs a sequence of scripts in a specific order to validate changes.

This diagram shows the flow of the main validation scripts as executed in the CI pipeline.

Validation Scripts

Each script in the CI pipeline has a specific role. Developers can run these scripts locally to test their contributions before creating a pull request.

Script	Description
check_manifest_schema.py	Validates manifest.json files against the manifest-schema.json.
check_manifest_files.py	Ensures files listed in manifest.json exist in the repository.
check_manifest_features.py	Uses tree-sitter-tlaplus to verify that features (e.g., pluscal, proof) are correctly tagged in the manifest.
check_markdown_table.py	Validates the main spec table in README.md against the manifests.
unicode_conversion.py	Converts specs to Unicode to test tooling compatibility.
translate_pluscal.py	Runs the PlusCal translator on all modules containing PlusCal.
parse_modules.py	Runs the SANY parser on all .tla files to check for syntax and semantic errors.
check_small_models.py	Runs TLC or Apalache on models expected to complete within 30 seconds and verifies their results.
smoke_test_large_models.py	Runs larger models for 5 seconds to ensure they don't crash immediately.
check_proofs.py	Runs TLAPM to validate formal proofs.

Sources: DEVELOPING.md:9-33

Consuming the Examples

This repository is an excellent source of real-world TLA⁺ specs for testing TLA⁺ tools. The manifest.json files are the primary entry point for consumption, as they provide a structured way to discover specifications and their properties. To ensure stability, it is recommended to consume a specific release of the repository rather than the head of the main branch, as the manifest format may change over time.

Sources: DEVELOPING.md:80-92, README.md:7-8

Conclusion

The TLA⁺ Examples repository is a critical resource for the TLA⁺ community. It provides a curated and validated collection of specifications that aid in learning, serve as practical case studies, and support the development of the TLA⁺ tooling ecosystem. Through its structured organization and automated validation, it maintains a high standard of quality and reliability for all included examples.

Sources: README.md:5-11, CONTRIBUTING.md:4-7