Contributing a New Specification

Relevant source files

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

• CONTRIBUTING.md
• DEVELOPING.md
• README.md
• manifest-schema.json
• specifications/Majority/manifest.json

Contributing a TLA⁺ specification to this repository is highly encouraged. Your spec will serve as a valuable example for the community, act as a real-world test case for TLA⁺ language tooling, and receive ongoing maintenance to ensure it remains functional as the TLA⁺ ecosystem evolves.

To maintain a high standard of quality, all specifications are subject to automated continuous integration (CI) tests. This guide outlines the process for preparing and submitting a new specification, including the necessary configuration for it to be validated by the CI system.

Sources: CONTRIBUTING.md:1-12

Contribution Workflow

A contribution can be a basic submission of spec files or a full submission integrated with the project's CI system. While full integration is preferred, maintainers can assist with the CI setup if needed.

The diagram below shows the two main paths for contributing a new specification.

Basic Contribution Steps

This is the simplest way to contribute a specification, without integrating it into the automated validation system.

1. Fork the repository.
2. Create a new directory for your spec under the specifications/ directory.
3. Add TLA⁺ files: Place all .tla files and their corresponding .cfg model files in the new directory.
4. Naming Convention: Ensure .cfg files match the name of the .tla file they model, or use it as a prefix (e.g., Spec.tla can have models Spec.cfg and SpecLiveness.cfg).
5. Add a README.md: Include a README.md file in the spec directory explaining its significance and linking to any relevant publications or websites.
6. (Optional) Exclude from CI: If you are not proceeding with CI integration, add your spec's directory path to the .ciignore file.

Following these steps allows you to contribute the specification files, though they will not be included in the CI-validated table in the main README.md.

Sources: CONTRIBUTING.md:14-36

Onboarding to Continuous Integration

To have your specification validated by the CI system, you must provide metadata in a manifest.json file and update the main project README.md. This ensures your spec is tested and correctly listed.

Sources: CONTRIBUTING.md:28-44

Step 1: Create and Configure manifest.json

Every CI-validated spec requires a manifest.json file in its root directory. This file contains metadata about the spec, its authors, modules, models, and proofs. You can create this file manually by referencing existing examples, or use a script to automate most of the process.

Sources: CONTRIBUTING.md:40-44

Generating the Manifest

The repository provides a script to auto-generate the manifest.json file.

1. Ensure Python 3.11+ is installed.
2. Install dependencies: pip install -r .github/scripts/requirements.txt
3. Run the script: python .github/scripts/generate_manifest.py

After generation, you must manually fill in certain fields like authors, sources, and model runtimes.

Sources: CONTRIBUTING.md:46-54

Manifest Structure

The manifest.json file adheres to a specific schema. The diagram below illustrates the relationship between the main components.

This diagram shows the nested structure of a manifest.json file.

Sources: manifest-schema.json, specifications/Majority/manifest.json

Key Manifest Fields

The following tables describe the essential fields you need to configure in your manifest.json.

Field	Description	Example
sources	An array of URLs relevant to the spec (papers, blog posts).	["https://..."]
authors	An array of strings listing the spec authors.	["Leslie Lamport"]
tags	An array of tags. Use "beginner" if appropriate for newcomers.	["beginner", "ewd"]
modules	An array of objects, one for each .tla module.	See below.

Sources: CONTRIBUTING.md:55-60, manifest-schema.json

Module Properties:

Field	Description
path	The path to the .tla file.
features	Auto-detected features like "pluscal" or "action composition".
models	An array of model objects associated with the module.
proof	An object containing proof runtime if the module has TLAPS proofs.

Sources: CONTRIBUTING.md:61-64, manifest-schema.json

Model Properties:

Field	Description	Example
path	Path to the .cfg file.	"specifications/Majority/MCMajority.cfg"
runtime	Approximate runtime in "HH:MM:SS" format. Models under 30s are run completely by CI.	"00:00:05"
mode	The checking mode. See table below.	"exhaustive search"
result	The expected outcome of the model check. See table below.	"success"
distinctStates	(Optional) The number of distinct states found by TLC.	2733
totalStates	(Optional) The total number of states explored by TLC.	3459
stateDepth	(Optional) The depth of the state graph.	6

Sources: CONTRIBUTING.md:65-81, manifest-schema.json

Model mode Options:

Mode	Description
"exhaustive search"	Default mode for standard TLC model checking.
{"simulate": {"traceCount": N}}	For simulation models, where N is the number of traces.
"generate"	For model trace generation.
"symbolic"	For models checked with the Apalache model checker.

Sources: CONTRIBUTING.md:69-72

Model result Options:

Result	Description
"success"	The model completes successfully.
"assumption failure"	The model violates an assumption.
"safety failure"	The model violates an invariant.
"liveness failure"	The model fails to satisfy a liveness property.
"deadlock failure"	The model encounters a deadlock.

Sources: CONTRIBUTING.md:73-78

Example manifest.json

{
  "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
        }
      ]
    },
    {
      "path": "specifications/Majority/MajorityProof.tla",
      "features": [],
      "models": [],
      "proof": {
        "runtime": "00:00:01"
      }
    }
  ]
}

Sources: specifications/Majority/manifest.json

Step 2: Update the README.md Table

After creating the manifest.json, you must add an entry for your specification to the main table in the project's README.md. The CI script check_markdown_table.py validates that the table's contents are consistent with the metadata in manifest.json.

Sources: CONTRIBUTING.md:83-85, DEVELOPING.md:16-17

The table has several columns that are populated based on the manifest data:

README.md Column	manifest.json Condition
Name	Link to the spec's directory.
Author(s)	Must match the authors list in the manifest.
Beginner	Checked if "beginner" is in the tags array.
TLAPS Proof	Checked if a proof object with a runtime is present in any module.
PlusCal	Checked if "pluscal" is in the features array of any module.
TLC Model	Checked if exhaustive search, generate, or simulate is present in the mode of any model.
Apalache	Checked if "symbolic" is in the mode of any model.

Sources: CONTRIBUTING.md:86-100, README.md:19-25

Step 3: Submitting the Pull Request

Once the manifest.json is complete and the README.md is updated, you can open a pull request. The CI system will automatically run all validation scripts against your changes and report any inconsistencies or failures. For a faster development loop, you can run these validation scripts locally.

Sources: CONTRIBUTING.md:102-104, DEVELOPING.md:41-44

Licensing

For consistency, contributing your specification under the MIT license is preferred. However, other compatible permissive licenses are also accepted.

Sources: CONTRIBUTING.md:10-12, README.md:310-312