Browsing and Searching Specifications
Relevant source files
The following files were used as context for generating this wiki page:The TLA⁺ Examples repository provides a structured system for users to browse, search, and discover specifications. This system supports multiple levels of exploration, from a high-level overview table to a detailed, searchable metadata framework. This allows users to find specifications based on various criteria, such as algorithm features, verification tools used, or expected model checking results.
The primary mechanisms for discovery are a summary table in the main README.md for quick browsing, and a system of manifest.json files within each specification directory that enables granular, command-line based searching. For more in-depth understanding, many specifications also include their own detailed README.md files.
Sources: README.md:1-10
Browsing via Summary Table
A quick way to get an overview of the validated specifications in the repository is through the summary table in the main README.md file. This table provides at-a-glance information about each specification.
Sources: README.md:40-42
The table includes the following columns:
| Column | Description |
|---|---|
| Name | The name of the specification, linked to its directory. |
| Author(s) | The author(s) of the specification. |
| Beginner | A checkmark (✔) indicates the spec is considered beginner-friendly. |
| TLAPS Proof | A checkmark (✔) indicates the spec includes a formal proof checkable by TLAPS. |
| PlusCal | A checkmark (✔) indicates the spec is written in or includes PlusCal. A (✔) means it includes a PlusCal variant. |
| TLC Model | A checkmark (✔) indicates the spec can be verified with the TLC model checker. |
| Apalache | A checkmark (✔) indicates the spec can be verified with the Apalache model checker. |
This table is intended to give a high-level summary and is the recommended starting point for browsing the available examples.
Sources: README.md:43-122, CONTRIBUTING.md:126-141
Searching via Specification Manifests
For more detailed and specific searches, the repository utilizes manifest.json files located in each specification's directory. These files contain rich metadata about the specification, its modules, and its models.
Sources: README.md:20-22
Command-Line Searching
The README.md suggests using standard command-line tools like grep to search through all manifest files for specific keywords. This allows users to find specifications that exhibit particular features or behaviors.
An example command for searching manifests is:
ls specifications/*/manifest.json | xargs grep -l $keyword
Sources: README.md:23-24
Similarly, to find models that use specific TLC features, one can search the .cfg files:
ls specifications/*/*.cfg | xargs grep -l $keyword
Sources: README.md:31-32
Searchable Keywords
The following are examples of keywords that can be used for searching:
- Features:
pluscal,proof,action composition - Model Modes:
generate(for trace generation),simulate,symbolic(for Apalache) - Model Results:
deadlock failure,safety failure,liveness failure,assumption failure - TLC Config Features:
SYMMETRY,VIEW,ALIAS,CONSTRAINT,DEADLOCK
Sources: README.md:25-33
Manifest File Structure
The manifest.json file is the core of the search system. Its structure is defined by manifest-schema.json and is designed to capture essential metadata for each specification.
The diagram below illustrates the hierarchical structure of a manifest.json file.
This diagram shows the entity relationships within a manifest.json file, from the top-level specification down to individual models.
Sources: manifest-schema.json, CONTRIBUTING.md:95-124
Key Manifest Fields
The following table describes the key fields within a manifest.json file that are useful for searching and browsing.
| Field Path | Type | Description |
|---|---|---|
authors | string[] | A list of authors who created the specification. |
tags | string[] | A list of tags for categorization, e.g., "beginner", "ewd". |
modules | object[] | An array of TLA+ modules (.tla files) within the specification. |
modules.path | string | The file path to the module. |
modules.features | string[] | A list of features detected in the module, such as "pluscal" or "action composition". |
modules.proof | object | If present, contains metadata about a TLAPS proof, including runtime. |
modules.models | object[] | An array of models (.cfg files) associated with the module. |
modules.models.runtime | string | The approximate runtime of the model in "HH:MM:SS" format. |
modules.models.mode | string or object | The execution mode for the model, e.g., "exhaustive search", "symbolic", or {"simulate": ...}. |
modules.models.result | string | The expected outcome of running the model, e.g., "success", "safety failure". |
modules.models.distinctStates | integer | The number of distinct states found by TLC. |
modules.models.totalStates | integer | The total number of states explored by TLC. |
modules.models.stateDepth | integer | The depth of the state graph. |
Sources: manifest-schema.json, CONTRIBUTING.md:95-124
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"
}
]
}
Sources: specifications/ewd687a/manifest.json:20-34
Manifest Generation and Validation
To ensure the accuracy and consistency of the searchable metadata, the repository includes a CI/CD pipeline with scripts for manifest generation and validation. This guarantees that the information in manifest.json files correctly reflects the content of the TLA+ specifications.
Sources: DEVELOPING.md:6-10, CONTRIBUTING.md:78-83
The workflow for contributing a spec and its manifest is as follows:
This flowchart shows the process from adding a new specification to its validation in the CI pipeline, ensuring metadata quality.
Sources: CONTRIBUTING.md:61-148, DEVELOPING.md:13-43
Advanced Browsing: Specification-Specific READMEs
Beyond the structured metadata, many specifications include their own README.md file. These documents provide a deep dive into the specification, offering context that cannot be captured in the manifest.json.
These READMEs often contain:
- A detailed explanation of the algorithm being specified.
- Links to original papers, blog posts, or publications.
- Descriptions of the different TLA+ modules and their relationships (e.g., refinement mappings).
- Visualizations, such as GIFs or diagrams, illustrating the algorithm's behavior.
- Results of statistical analysis or simulations performed using the TLA+ model.
For example, the ewd998 specification includes a detailed analysis of algorithmic variants, performance statistics, and animated GIFs derived from model traces. The MultiPaxos-SMR README explains how the spec models a practical, real-world implementation and links to a corresponding Rust implementation.
Sources: specifications/ewd998/README.md, specifications/MultiPaxos-SMR/README.md
Conclusion
The TLA⁺ Examples repository employs a multi-faceted approach to specification discovery. A high-level summary table provides a quick entry point for browsing. For targeted discovery, a powerful search system is enabled by detailed manifest.json files, which are programmatically validated for accuracy. Finally, specification-specific README files offer deep, contextual information. This layered system effectively serves both developers looking for specific examples and tool-builders who consume the repository as a test corpus.
Sources: README.md:1-10, DEVELOPING.md:131-137