Repository Directory Structure

Relevant source files

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

• README.md
• CONTRIBUTING.md
• DEVELOPING.md
• specifications/ewd687a/manifest.json
• specifications/ewd998/README.md
• specifications/Majority/manifest.json
• specifications/TLC/manifest.json

The TLA⁺ Examples repository is a curated collection of TLA⁺ specifications designed to serve as a comprehensive example library, a test corpus for language tooling, and a set of case studies. The repository's directory structure is strictly organized to facilitate automated validation, maintenance, and easy navigation of the specifications. The core components are the specifications themselves, metadata files that describe them, and a suite of scripts for continuous integration.

This structure ensures that every specification is verifiable and that its features are accurately indexed. Key directories include specifications/ for all TLA⁺ code, and .github/scripts/ for the validation and maintenance automation that underpins the repository's quality standards.

Sources: README.md:1-12, CONTRIBUTING.md:1-7, DEVELOPING.md:8-9

Top-Level Directory Layout

The repository root contains configuration files, documentation, and the main directories for specifications and CI scripts.

This diagram shows the high-level organization of the repository.

Key Files and Directories

Name	Description
specifications/	Contains all TLA⁺ specifications, with each spec in its own subdirectory.
.github/	Contains GitHub-specific files, including CI workflows and validation scripts.
README.md	The main project README, featuring a table of all CI-validated specifications.
CONTRIBUTING.md	Instructions for contributing new specifications to the repository.
DEVELOPING.md	Documentation for developers on running validation scripts locally and maintaining the CI system.
.ciignore	A file listing specification directories to be excluded from automated CI validation.
manifest-schema.json	The JSON schema that defines the structure for all manifest.json files.

Sources: README.md:11, 20, CONTRIBUTING.md:12, 22, DEVELOPING.md:10, 12

specifications/ Directory

This is the primary directory, housing all TLA⁺ example specifications. To maintain organization and enable automated processing, each specification is contained within its own dedicated subdirectory.

Sources: README.md:11, CONTRIBUTING.md:12

Specification Subdirectory Structure

Each subdirectory within specifications/ follows a conventional layout to group related files and provide metadata for the CI system.

This diagram illustrates the typical file structure for a single specification, such as specifications/ewd687a/.

• .tla files: These are the TLA⁺ or PlusCal source files containing the specification logic.
• .cfg files: Configuration files for the TLC model checker. The filename must match or be prefixed by the name of the .tla file it models (e.g., Spec.tla can have models Spec.cfg and Spec_Liveness.cfg).
• manifest.json: A mandatory metadata file that describes the specification, its authors, modules, models, and features. This file is critical for CI validation.
• README.md: An optional file providing context, explanations, and links to relevant publications for the specification.

Sources: CONTRIBUTING.md:13-19, 30, specifications/ewd998/README.md

manifest.json Metadata File

The manifest.json file is the backbone of the repository's automation. It provides structured metadata that CI scripts use to discover specs, models, and their properties, and to validate them correctly.

The following class diagram represents the schema of the manifest.json file.

An example snippet from a manifest.json file:

{
  "path": "specifications/ewd687a/EWD687a_anim.tla",
  "features": [],
  "models": [
    {
      "path": "specifications/ewd687a/EWD687a_anim.cfg",
      "runtime": "00:00:01",
      "mode": {
        "simulate": {
          "traceCount": 100
        }
      },
      "result": "safety failure"
    }
  ]
}

Source: specifications/ewd687a/manifest.json:19-33

.github/scripts/ Directory

This directory contains Python scripts that form the CI pipeline. These scripts are responsible for validating every aspect of a contributed specification, from its file structure and metadata to parsing and model checking.

Sources: DEVELOPING.md:8-9

CI Validation Flow

The CI workflow executes a series of scripts in a specific order to ensure consistency and correctness across the repository.

This flowchart shows the sequence of validation steps performed by the CI scripts.

Key Validation Scripts

Script	Description
check_manifest_schema.py	Validates all manifest.json files against manifest-schema.json.
check_manifest_files.py	Ensures modules and models in manifest.json exist on the filesystem.
check_manifest_features.py	Parses .tla files to verify features like pluscal or proof are correctly tagged in the manifest.
check_markdown_table.py	Validates that the spec table in README.md is consistent with the manifest.json files.
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 outcomes.
smoke_test_large_models.py	Runs larger models for 5 seconds to ensure they do not crash immediately.
check_proofs.py	Runs the TLAPM proof manager against modules containing formal proofs.
generate_manifest.py	A utility script for contributors to auto-generate a manifest.json file for a new spec.

Sources: DEVELOPING.md:10-36, CONTRIBUTING.md:41-42

Conclusion

The directory structure of the TLA⁺ Examples repository is meticulously designed for automation and scalability. By enforcing a standard layout for specifications, mandating detailed manifest.json metadata files, and leveraging a comprehensive suite of validation scripts, the project ensures a high standard of quality and consistency. This systematic approach makes the repository a reliable resource for both learning TLA⁺ and for testing TLA⁺-related tools.

Sources: README.md:1-12, CONTRIBUTING.md:8-11