Beginner-Friendly Examples
Relevant source files
The following files were used as context for generating this wiki page:The TLA⁺ Examples repository serves as a comprehensive library of specifications, and a key part of its mission is to provide examples that are accessible to newcomers. A curated set of specifications is explicitly marked as "beginner-friendly" to demonstrate how to specify algorithms in TLA⁺ and to serve as case studies for learning. These examples typically cover well-known puzzles or simple algorithms, making them ideal for those new to formal methods and TLA⁺.
These specifications are not just for reading; they are integrated into the repository's continuous integration (CI) system. This ensures they are syntactically correct, and their associated models are checked using tools like TLC. The beginner-friendly examples showcase various features of TLA⁺, including PlusCal, model checking with expected successes and failures, and formal proofs with TLAPS.
Sources: README.md:6-9, README.md:20-25, CONTRIBUTING.md:41-42
Identifying and Contributing Beginner-Friendly Specs
Specifications are designated as beginner-friendly through a specific metadata tag within their manifest.json file. This structured approach allows for easy discovery and automated processing.
Sources: CONTRIBUTING.md:41-42
The beginner Tag
To mark a specification as suitable for beginners, the tags array in its manifest.json file must include the string "beginner".
The following diagram illustrates how a specification is identified as beginner-friendly.
This diagram shows the check performed to classify a spec.
Sources: CONTRIBUTING.md:41-42
For example, the manifest.json for the "Die Hard" puzzle includes this tag:
{
"sources": [],
"authors": [
"Leslie Lamport"
],
"tags": [
"beginner"
],
...
}
Sources: specifications/DieHard/manifest.json:5-8
Contribution Process
Contributors are encouraged to add new examples. The process for adding a beginner-friendly spec involves adding the spec files, creating a manifest.json file with the beginner tag, and updating the main README.md table.
The flow for contributing a new beginner-friendly spec is as follows:
This flowchart outlines the steps for a contributor to add a new beginner-friendly specification to the repository.
Sources: CONTRIBUTING.md:16-25, CONTRIBUTING.md:52-67
Curated Examples
The repository contains a wide variety of beginner-friendly examples. The main README.md file provides a table that serves as a quick reference guide, indicating which specs are for beginners and what features they include.
Sources: README.md:20-25
| Name | Author(s) | PlusCal | TLC Model | TLAPS Proof |
|---|---|---|---|---|
| The Die Hard Problem | Leslie Lamport | ✔ | ||
| The Tower of Hanoi Puzzle | Markus Kuppe, Alexander Niederbühl | ✔ | ||
| Boyer-Moore Majority Vote | Stephan Merz | ✔ | ✔ | |
| The Coffee Can Bean Problem | Andrew Helwer | ✔ | ||
| Missionaries and Cannibals | Leslie Lamport | ✔ |
Sources: README.md:36, README.md:40, README.md:44, README.md:46, README.md:47
The Die Hard Problem
This example models the water jug puzzle from the movie Die Hard. It is a classic state-space exploration problem.
The manifest.json for this specification defines two modules and their corresponding models. Interestingly, both models are expected to result in a safety failure, demonstrating how TLC can be used to find out if a certain state (like measuring exactly 4 gallons) is reachable.
This diagram shows the module and model structure for the Die Hard example, highlighting the expected safety failures.
Sources: specifications/DieHard/manifest.json:10-25
The Tower of Hanoi Puzzle
This specification models the famous Tower of Hanoi puzzle. It is another example of using TLA+ for solving state-space search problems.
The manifest for this example includes multiple TLA+ modules. The model check defined in MC.cfg is configured to find a safety failure, which is a common technique to verify reachability properties by checking if an invariant is violated when the target state is reached.
This diagram shows the modules in the Tower of Hanoi specification and the expected outcome of its model.
Sources: specifications/tower_of_hanoi/manifest.json:10-25
Boyer-Moore Majority Vote
This example specifies the Boyer-Moore majority vote algorithm. It showcases how TLA+ can be used to model and verify algorithms.
This specification is notable because it includes both a TLC model that completes successfully and a formal proof checked by TLAPS. This provides beginners with an example that covers both model checking and deductive verification.
This diagram illustrates that the Majority spec includes both a successful TLC model and a TLAPS-checked proof.
Sources: specifications/Majority/manifest.json:10-26
The Coffee Can Bean Problem
This example models a puzzle involving black and white beans in a coffee can. It's a simple problem that demonstrates how an invariant holds throughout a process.
The manifest for this spec is interesting because it defines three different models with increasing problem sizes (100Beans, 1000Beans, 3000Beans). All models are expected to succeed, and the manifest records state-space statistics for the smaller models, turning them into regression tests for the TLC model checker.
{
"path": "specifications/CoffeeCan/CoffeeCan1000Beans.cfg",
"runtime": "00:00:15",
"mode": "exhaustive search",
"result": "success",
"distinctStates": 501500,
"totalStates": 2000002,
"stateDepth": 1
}
This snippet from the manifest shows the detailed results for one of the models.
Sources: specifications/CoffeeCan/manifest.json:13-21, CONTRIBUTING.md:70-72
Summary
The beginner-friendly examples in this repository are a cornerstone of its educational value. By providing a set of simple, well-documented, and automatically-validated TLA⁺ specifications, the project significantly lowers the barrier to entry for learning formal methods. These examples demonstrate a range of TLA⁺ features, from basic state-machine modeling and model checking to handling expected failures and writing formal proofs, making them an invaluable resource for the TLA⁺ community.
Sources: README.md:6-9