Writing Specifications with PlusCal
Relevant source files
The following files were used as context for generating this wiki page:PlusCal is a high-level language used for writing TLA+ specifications of algorithms. Within this repository, it serves as a way to describe algorithms in a more familiar, imperative style, which is then translated into standard TLA+ for formal verification. Many examples in this repository use PlusCal, either exclusively or as a variant alongside a pure TLA+ specification, to demonstrate its utility in modeling systems ranging from simple sequential algorithms to complex distributed protocols.
The use of PlusCal is a key feature tracked across the repository's specifications. It is often highlighted for beginner-friendly examples, indicating its role in making TLA+ more accessible to newcomers. The project's continuous integration (CI) system is configured to automatically handle PlusCal files, ensuring they are correctly translated and validated.
Sources: README.md, CONTRIBUTING.md, DEVELOPING.md
The PlusCal Development Workflow
Writing and verifying a specification using PlusCal involves a distinct workflow that leverages the TLA+ toolchain. The process begins with writing the algorithm in PlusCal syntax, which is then translated into a standard TLA+ module. This generated module can then be parsed and model-checked using tools like TLC.
The repository's CI pipeline automates this process. A dedicated script, translate_pluscal.py, is responsible for running the PlusCal translator on all modules that contain PlusCal code. This ensures that the PlusCal syntax is valid and that the corresponding TLA+ translation is up-to-date before any further verification steps, such as parsing or model checking, are performed.
Sources: DEVELOPING.md:21-22, DEVELOPING.md:60-61
The following diagram illustrates the typical workflow for a PlusCal specification.
This diagram shows the process of writing a PlusCal spec, translating it to TLA+, and then using TLA+ tools for verification.
Example PlusCal Specifications
Numerous specifications within this repository utilize PlusCal. These examples span a wide range of problem domains and complexity, from classic concurrency problems to practical distributed systems protocols. The main README.md file provides a comprehensive table indicating which specifications include a PlusCal variant.
| Specification Name | Beginner-Friendly | Description |
|---|---|---|
| The Dining Philosophers Problem | ✔ | A classic concurrency problem. The specification uses PlusCal. |
| The Boulangerie Algorithm | A mutual exclusion algorithm for N processes. Includes a PlusCal version. | |
| MultiPaxos in SMR-Style | A practical state machine replication (SMR) style spec of MultiPaxos, written in PlusCal. | |
| Loop Invariance | ✔ | Contains three simple sequential algorithms (SumSequence, BinarySearch, Quicksort) written in PlusCal. |
| The TLC Safety Checking Algorithm | A specification of the TLC algorithm itself, which includes a PlusCal module. | |
| Chang-Roberts Algorithm | An algorithm for leader election in a ring, with a PlusCal implementation. |
Sources: README.md:23-100, specifications/MultiPaxos-SMR/README.md:5-6, specifications/LoopInvariance/README.txt:1-4, specifications/DiningPhilosophers/manifest.json, specifications/Bakery-Boulangerie/manifest.json, specifications/TLC/manifest.json, specifications/chang_roberts/manifest.json
Contributing PlusCal Specifications
When contributing a new specification that uses PlusCal, it must be correctly configured to integrate with the repository's CI system. This involves creating a manifest.json file in the specification's directory.
Manifest Configuration
The manifest.json file contains metadata about the specification. For a module written in PlusCal, the features array must include the "pluscal" tag. The CI script check_manifest_features.py uses tree-sitter-tlaplus to parse the .tla files and verify that this feature is correctly recorded in the manifest.
A utility script, generate_manifest.py, can be used to automatically generate the manifest.json file and detect the presence of PlusCal code.
Sources: CONTRIBUTING.md:49-54, CONTRIBUTING.md:69-72, DEVELOPING.md:16-19
Here is an example snippet from a manifest.json file declaring a module with a PlusCal feature:
{
"modules": [
{
"path": "specifications/DiningPhilosophers/DiningPhilosophers.tla",
"features": [
"pluscal"
],
"models": [
{
"path": "specifications/DiningPhilosophers/DiningPhilosophers.cfg",
"runtime": "00:00:01",
"mode": "exhaustive search",
"result": "success"
}
]
}
]
}
Sources: specifications/DiningPhilosophers/manifest.json:8-24
After creating the manifest, the new specification must be added to the main table in the project's README.md. A checkmark in the "PlusCal" column should be added if and only if the pluscal tag is present in the features field for at least one module in the manifest.json.
Sources: CONTRIBUTING.md:104-106
Summary
PlusCal is an integral part of the TLA+ ecosystem represented in this repository. It provides an alternative, often more approachable, syntax for writing specifications, which are then translated to TLA+ for rigorous verification. The repository contains a rich set of examples and a well-defined contribution process, including automated CI checks, to support the development and maintenance of high-quality PlusCal specifications.
Sources: README.md:4-7, CONTRIBUTING.md:3-6