Continuous Integration Workflow
Relevant source files
The following files were used as context for generating this wiki page:The Continuous Integration (CI) workflow is an automated system designed to ensure a high standard of quality for all TLA⁺ specifications within this repository. It subjects every contributed spec to a series of validation tests, checking for correctness, consistency, and proper configuration. This process not only serves as a quality gate for new contributions but also provides basic maintenance, ensuring specs remain functional as TLA⁺ tools evolve.
The CI pipeline is built around a series of Python scripts that validate spec files, models, metadata, and documentation. By integrating specs into this system, contributors ensure their examples become robust, real-world test cases for TLA⁺ language tooling. The workflow is defined in .github/workflows/CI.yml and can also be executed locally to facilitate a faster development cycle.
Sources: CONTRIBUTING.md:5-11, DEVELOPING.md:8-10
CI Onboarding for New Specifications
To include a new specification in the CI validation process, a contributor must perform several configuration steps. While specs can be temporarily excluded by adding them to the .ciignore file, full integration is required for inclusion in the main validated examples table.
Sources: CONTRIBUTING.md:12-16, CONTRIBUTING.md:29-32
1. Metadata Manifest (manifest.json)
Each specification directory must contain a manifest.json file. This file stores critical metadata about the spec, its modules, and its models, which is then used by the CI scripts for validation.
Key fields that must be manually filled or verified include:
sources: Links to relevant papers, blog posts, or repositories.authors: A list of the spec's authors.tags: Keywords like"beginner".proof: For modules with formal proofs, the approximate runtime ("HH:MM:SS").models: An array of models with details on runtime, checking mode, and expected result.
A helper script, generate_manifest.py, can be used to auto-generate a skeleton manifest.json file, which then needs to be completed by the contributor.
Sources: CONTRIBUTING.md:37-41, CONTRIBUTING.md:46-51
The following diagram illustrates the relationship between the specification files, the manifest, and the main project README, all of which are cross-validated by the CI.
Sources: DEVELOPING.md:11-20, CONTRIBUTING.md:37-41
2. README Table Update
After creating the manifest.json, the new specification must be added to the main table in the project's README.md. The information in this table is strictly validated against the manifest.json by the check_markdown_table.py script.
The table columns that must be consistent with the manifest are:
| Column | manifest.json Condition |
|---|---|
| Beginner | Checked if "beginner" is in the spec's tags field. |
| TLAPS Proof | Checked if proof runtime details are present for any module. |
| PlusCal | Checked if a "pluscal" tag is in the features field for any module. |
| TLC Model | Checked if "exhaustive search", "generate", or "simulate" is in the mode field for any model. |
| Apalache | Checked if "symbolic" is in the mode field for any model. |
Sources: CONTRIBUTING.md:82-97
CI Validation Scripts
The core of the CI workflow is a set of Python scripts located in the .github/scripts directory. They are executed sequentially to perform a comprehensive set of checks.
Sources: DEVELOPING.md:7-9
Script Execution Flow
The CI pipeline executes the scripts in a specific order to validate different aspects of the repository. The process starts with metadata checks and progresses to parsing, model checking, and proof verification.
This flowchart shows the sequence of scripts run in the CI pipeline.
Sources: DEVELOPING.md:10-33
Script Descriptions
The following table details each validation script and its purpose in the CI pipeline.
| Script | Description |
|---|---|
check_manifest_schema.py | Validates all manifest.json files against the manifest-schema.json schema. |
check_manifest_files.py | Ensures that modules and models listed in each manifest.json exist on the filesystem. |
check_manifest_features.py | Parses .tla and .cfg files to verify that features (e.g., pluscal, proof, view) are correctly recorded in the manifest. |
check_markdown_table.py | Parses README.md and validates the main spec table's content against each manifest.json. |
unicode_conversion.py | Converts specs to Unicode using tlauc to ensure tooling works on both ASCII and Unicode. |
translate_pluscal.py | Runs the PlusCal translator on all modules containing PlusCal code to validate their syntax. |
parse_modules.py | Runs the SANY parser on all .tla files to check for syntactic and semantic validity. |
check_small_models.py | Runs TLC or Apalache to completion on models expected to finish within 30 seconds, verifying their outcome and state space size. |
smoke_test_large_models.py | Runs larger models for 5 seconds to ensure they do not crash immediately. |
check_proofs.py | Runs TLAPM against modules containing formal proofs to ensure they are valid. |
Sources: DEVELOPING.md:11-33, specifications/MultiPaxos-SMR/README.md:10-11
Utility Scripts
In addition to validation scripts, the repository provides utilities to aid developers.
| Script | Description |
|---|---|
generate_manifest.py | Auto-generates a manifest.json file for a new spec by parsing its files. |
record_model_state_space.py | Runs small models and records their state space information into the corresponding manifest.json. |
format_markdown_table.py | A helper script for programmatically formatting the README.md table. |
Sources: DEVELOPING.md:36-46
Local Development and Execution
All CI validation scripts can be run locally to speed up the development and contribution process. This allows contributors to verify their changes before opening a pull request. The process involves setting up a Python virtual environment, installing dependencies from .github/scripts/requirements.txt, and downloading TLA⁺ tool dependencies.
After setup, each script can be executed from the command line. Most scripts accept --skip and --only parameters to target specific files, which is useful for iterating quickly on changes.
Sources: DEVELOPING.md:51-78, CONTRIBUTING.md:99-100
Trace Validation
Beyond static analysis and model checking, the CI philosophy extends to validating implementation traces against a high-level TLA+ specification. As demonstrated with the EWD998 specification, a trace from a real implementation (e.g., a JSON log file) can be checked by TLC. This is achieved by creating a TLA+ specification that reads the trace and asserts that each step in the trace corresponds to a valid state transition in the high-level model. This powerful technique helps find divergences between a specification and its implementation.
Sources: specifications/ewd998/EWD998ChanTrace.md:18-28
Summary
The CI workflow is a cornerstone of the TLA⁺ Examples repository, enforcing a high degree of quality, correctness, and consistency across all contributed specifications. By automating a wide range of checks—from metadata validation and parsing to model checking and proof verification—the CI system ensures that the repository remains a reliable and valuable resource for the TLA⁺ community. The ability to run these checks locally and use advanced techniques like trace validation further empowers developers to contribute high-quality, well-vetted specifications.
Sources: CONTRIBUTING.md:5-8, README.md:8-10