Relevant source files

The following files were used as context for generating this wiki page: - [CONTRIBUTING.md](https://github.com/Alonso-pixel/Examples/blob/main/CONTRIBUTING.md) - [DEVELOPING.md](https://github.com/Alonso-pixel/Examples/blob/main/DEVELOPING.md) - [README.md](https://github.com/Alonso-pixel/Examples/blob/main/README.md) - [specifications/ewd687a/manifest.json](https://github.com/Alonso-pixel/Examples/blob/main/specifications/ewd687a/manifest.json) - [specifications/Majority/manifest.json](https://github.com/Alonso-pixel/Examples/blob/main/specifications/Majority/manifest.json)

# Specification Metadata (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](https://github.com/Alonso-pixel/Examples/blob/main/README.md), [CONTRIBUTING.md](https://github.com/Alonso-pixel/Examples/blob/main/CONTRIBUTING.md), [DEVELOPING.md](https://github.com/Alonso-pixel/Examples/blob/main/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. ```mermaid erDiagram SPECIFICATION { string sources string authors string tags } MODULE { string path string features object proof } MODEL { string path string runtime string mode string result int distinctStates int totalStates int stateDepth } SPECIFICATION ||--|{ MODULE : contains MODULE ||--|{ MODEL : has ``` *This ER diagram shows the hierarchical structure of the manifest, where a specification contains one or more modules, and each module can contain one or more models.* Sources: [CONTRIBUTING.md](https://github.com/Alonso-pixel/Examples/blob/main/CONTRIBUTING.md), [specifications/ewd687a/manifest.json](https://github.com/Alonso-pixel/Examples/blob/main/specifications/ewd687a/manifest.json) ### 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