Specification Metadata (manifest.json)

Relevant source files

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

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

Each TLA⁺ specification within the specifications directory is accompanied by a manifest.json file. This file serves as a centralized metadata repository, detailing essential information about the specification, its authors, source, and associated TLA⁺ modules and models. The primary purpose of the manifest is to facilitate automated validation through the project's Continuous Integration (CI) pipeline and to aid users in discovering examples with specific characteristics.

The metadata within manifest.json is crucial for a suite of validation scripts that check for correctness, consistency, and feature alignment. For instance, scripts verify that the modules and models listed in the manifest exist as files, and that features tagged in the manifest (like pluscal or proof) are actually present in the corresponding .tla files. This structured metadata also powers the main summary table in the project's README.md, ensuring it accurately reflects the repository's contents.

Sources: README.md, CONTRIBUTING.md, DEVELOPING.md

Manifest Structure and Schema

The manifest.json file adheres to a specific JSON schema. At the root level, it contains properties that apply to the entire specification, such as authorship and tags. The core of the manifest is the modules array, which lists each TLA⁺ module (.tla file) and its associated models (.cfg files).

The following diagram illustrates the entity relationships within a manifest.json file.

Top-Level Properties

These properties provide general information about the specification.

Property	Type	Description
sources	Array	A list of URLs relevant to the source of the specification, such as papers, blog posts, or original repositories.
authors	Array	A list of people who authored the specification. This must match the authors listed in the README.md table.
tags	Array	A list of tags for categorization. A special tag, "beginner", indicates the spec is suitable for TLA⁺ newcomers.
modules	Array	An array of objects, where each object describes a single TLA⁺ module (.tla file) and its associated models.

Sources: CONTRIBUTING.md, specifications/Majority/manifest.json

Module Properties

Each entry in the modules array describes a .tla file.

Property	Type	Description -
path	string	The relative path to the .tla module file. -
features	Array	A list of features used by the module, detected by CI scripts. A common feature is "pluscal", indicating the module contains PlusCal code. -
models	Array	An array of model objects associated with this module. -
proof	object	An object containing metadata about a formal proof contained in the module. It includes a runtime field ("HH:MM:SS") for the approximate time to check the proof. This is used by CI to determine if the proof should be checked in its entirety.

Sources: CONTRIBUTING.md, DEVELOPING.md, specifications/Majority/manifest.json

Model Properties

Each entry in the models array describes a .cfg model checking file.

Property	Type	Description -
path	string	The relative path to the .cfg model file. -
runtime	string	Approximate model runtime on an ordinary workstation, in "HH:MM:SS" format. Models under 30 seconds are run to completion by CI. -
mode	string or object	Defines the model checking mode. Defaults to "exhaustive search". Can be an object for simulation, e.g., {"simulate": {"traceCount": N}}. Other modes include "generate" and "symbolic" (for Apalache).
result	string	The expected outcome of the model check. Possible values are "success", "assumption failure", "safety failure", "liveness failure", and "deadlock failure".
distinctStates	integer	(Optional) The number of distinct states found by TLC. Used as a regression test for TLC performance. Only valid for successful exhaustive searches.
totalStates	integer	(Optional) The total number of states explored by TLC. Used as a regression test. Only valid for successful exhaustive searches.
stateDepth	integer	(Optional) The maximum depth of the state graph. Used as a regression test. Only valid for successful exhaustive searches.

Sources: CONTRIBUTING.md, specifications/ewd687a/manifest.json, specifications/Majority/manifest.json

Example Manifest

The following snippet from specifications/ewd687a/manifest.json demonstrates a multi-module specification with different model types, including an exhaustive search and a simulation model that is expected to fail.

{
  "sources": [],
  "authors": [
    "Leslie Lamport",
    "Markus Kuppe",
    "Stephan Merz"
  ],
  "tags": [
    "ewd",
    "beginner"
  ],
  "modules": [
    {
      "path": "specifications/ewd687a/EWD687a.tla",
      "features": [],
      "models": []
    },
    {
      "path": "specifications/ewd687a/EWD687aPlusCal.tla",
      "features": [
        "pluscal"
      ],
      "models": []
    },
    {
      "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"
        }
      ]
    },
    {
      "path": "specifications/ewd687a/MCEWD687a.tla",
      "features": [],
      "models": [
        {
          "path": "specifications/ewd687a/MCEWD687a.cfg",
          "runtime": "00:01:00",
          "mode": "exhaustive search",
          "result": "success"
        }
      ]
    }
  ]
}

Sources: specifications/ewd687a/manifest.json

Role in Continuous Integration (CI)

The manifest.json files are fundamental to the repository's CI workflow. A series of Python scripts consume these files to perform comprehensive validation checks on every specification.

The diagram below shows the flow of how manifest files are used in the CI validation process.

Key CI scripts that rely on manifest.json:

• check_manifest_schema.py: Validates all manifests against the master manifest-schema.json.
• check_manifest_files.py: Ensures that the path entries for modules and models correspond to actual files in the repository.
• check_manifest_features.py: Parses .tla and .cfg files to verify that features listed in the manifest (e.g., pluscal, view) are correct.
• check_markdown_table.py: Parses README.md to ensure the main specification table is consistent with the data in the manifests.
• check_small_models.py: Runs TLC or Apalache on models with a short runtime and verifies that the result matches the manifest's expectation.
• check_proofs.py: Runs the TLA⁺ Proof Manager (TLAPM) on modules that have a proof object defined.

Sources: DEVELOPING.md

Contribution and Generation

For contributors adding a new specification, creating a manifest.json is a required step. While it can be done manually by referencing existing examples, the repository provides a script to automate most of the process.

The generate_manifest.py script will create a new manifest.json file for a spec, automatically finding TLA⁺ modules and models and detecting features like PlusCal usage by parsing the source files. The contributor then needs to manually fill in fields that cannot be auto-generated, such as authors, sources, model runtime, and expected result.

Sources: CONTRIBUTING.md, DEVELOPING.md

Summary

The manifest.json file is a cornerstone of the TLA⁺ Examples repository. It provides a structured, machine-readable format for specification metadata that is essential for automated quality assurance via the CI pipeline. It also serves as a discovery mechanism, allowing developers and learners to easily find specifications with particular tools, features, or properties. By enforcing consistency between the metadata and the actual code, the manifest system ensures the repository remains a high-quality, reliable, and maintainable resource for the TLA⁺ community.

Sources: README.md, CONTRIBUTING.md, DEVELOPING.md