Puzzles and Riddles
Relevant source files
The following files were used as context for generating this wiki page:- README.md
- specifications/N-Queens/manifest.json
- specifications/CarTalkPuzzle/manifest.json
- specifications/EinsteinRiddle/manifest.json
- specifications/Moving_Cat_Puzzle/manifest.json
- specifications/tower_of_hanoi/manifest.json
- specifications/MissionariesAndCannibals/manifest.json
- specifications/Stones/manifest.json
- specifications/SlidingPuzzles/manifest.json
This repository contains a collection of TLA⁺ specifications for various classic puzzles and riddles. These specifications serve as a comprehensive example library, demonstrating how to model and verify algorithmic problems using TLA⁺. Many are marked as beginner-friendly, making them an excellent resource for newcomers to formal specification.
The puzzles are validated using different verification tools, including TLC for model checking and Apalache for symbolic model checking. They showcase various TLA⁺ features and modeling techniques, from simple state machines to more complex problems involving PlusCal. These examples also function as a diverse corpus for developing and testing TLA⁺ language tools.
Sources: README.md:3-8, README.md:21-26
Overview of Puzzles
The repository includes a variety of puzzles, many of which are designed to be accessible to beginners. The following table summarizes some of the puzzles available, their authors, and the verification tools used.
| Name | Author(s) | Beginner | Verification Tool(s) |
|---|---|---|---|
| The N-Queens Puzzle | Stephan Merz | ✔ | TLC |
| The Car Talk Puzzle | Leslie Lamport | ✔ | TLC |
| The Die Hard Problem | Leslie Lamport | ✔ | TLC |
| The Tower of Hanoi Puzzle | Markus Kuppe, Alexander Niederbühl | ✔ | TLC |
| Missionaries and Cannibals | Leslie Lamport | ✔ | TLC |
| Stone Scale Puzzle | Leslie Lamport | ✔ | TLC |
| The Moving Cat Puzzle | Florian Schanda | ✔ | TLC |
| Sliding Block Puzzle | Mariusz Ryndzionek | TLC | |
| Einstein's Riddle | Isaac DeFrain, Giuliano Losa | Apalache |
Sources: README.md:29-61, specifications/N-Queens/manifest.json:5-11, specifications/CarTalkPuzzle/manifest.json:5-11, specifications/tower_of_hanoi/manifest.json:5-11, specifications/MissionariesAndCannibals/manifest.json:5-11, specifications/Stones/manifest.json:5-11, specifications/Moving_Cat_Puzzle/manifest.json:5-9, specifications/SlidingPuzzles/manifest.json:5-7, specifications/EinsteinRiddle/manifest.json:5-9
Individual Puzzle Analysis
Each puzzle is contained within its own directory under specifications/ and includes TLA⁺ modules, configuration files, and a manifest.json file detailing its metadata and verification results.
The N-Queens Puzzle
The N-Queens puzzle is a classic problem of placing N chess queens on an N×N chessboard so that no two queens threaten each other. This specification is marked as beginner-friendly and includes a PlusCal variant.
The diagram below illustrates the structure of the N-Queens specification files and their models.
This diagram shows the TLA+ and PlusCal specifications for N-Queens, both associated with the FourQueens model.
The manifest file indicates that the FourQueens model for both the standard TLA⁺ and PlusCal versions results in a "safety failure", which is a common technique to demonstrate how a model checker finds a solution (or in this case, a state that violates the safety condition, which represents a valid solution to the puzzle).
Sources: README.md:34, specifications/N-Queens/manifest.json
Einstein's Riddle
This specification models the famous logic puzzle attributed to Albert Einstein. Unlike many other puzzles in this repository that use the TLC model checker, this one is verified using the Apalache symbolic model checker.
The model configuration in manifest.json specifies the mode as symbolic and expects a safety failure, which indicates that Apalache successfully finds a state that violates an invariant, thereby finding the solution to the riddle.
{
"path": "specifications/EinsteinRiddle/Einstein.tla",
"features": [],
"models": [
{
"path": "specifications/EinsteinRiddle/Einstein.cfg",
"runtime": "00:00:01",
"mode": "symbolic",
"result": "safety failure"
}
]
}
Sources: README.md:59, specifications/EinsteinRiddle/manifest.json:10-20
The Moving Cat Puzzle
This puzzle involves a cat moving between boxes. The specification includes two distinct models to check the puzzle's properties under different conditions: one with an even number of boxes and one with an odd number. Both models are checked via exhaustive search with TLC and complete successfully.
The results from the model checks highlight how the state space differs based on the initial constants.
| Model Configuration | Result | Distinct States | Total States | State Depth |
|---|---|---|---|---|
CatEvenBoxes.cfg | success | 48 | 128 | 1 |
CatOddBoxes.cfg | success | 30 | 78 | 1 |
Sources: README.md:46, specifications/Moving_Cat_Puzzle/manifest.json:15-23, specifications/Moving_Cat_Puzzle/manifest.json:24-32
Tower of Hanoi Puzzle
This is a specification for the classic Tower of Hanoi puzzle. The implementation is structured across multiple TLA⁺ modules, including Hanoi.tla, HanoiSeq.tla, and Bits.tla. The associated model check is configured to find a "safety failure," which in the context of this puzzle likely means reaching the solved state, which violates a "not-solved" invariant.
{
"path": "specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC.tla",
"features": [],
"models": [
{
"path": "specifications/tower_of_hanoi/Hanoi.toolbox/Model_1/MC.cfg",
"runtime": "00:00:01",
"mode": "exhaustive search",
"result": "safety failure"
}
]
}
Sources: README.md:41, specifications/tower_of_hanoi/manifest.json:28-38
Verification and Tooling
The puzzles in this repository are primarily verified using the TLC model checker and the Apalache symbolic model checker. The manifest.json file in each puzzle's directory specifies the tool, mode, and expected outcome.
The general verification flow is as follows:
This diagram shows that a TLA+ specification is processed by a verification tool like TLC or Apalache, leading to a result such as success or failure.
- Exhaustive Search: Used by TLC to explore all reachable states of a finite model. Most puzzles, like
Moving_Cat_Puzzle, use this mode. - Symbolic: Used by Apalache to check properties over potentially infinite state spaces.
EinsteinRiddleis an example that uses this mode. - Safety Failure: This result often indicates that the model checker has found a state that violates a safety invariant. For many puzzles, this is the desired outcome, as the "violating" state is actually the solution to the puzzle. Examples include
N-Queens,MissionariesAndCannibals, andTower of Hanoi. - Success: This result indicates that no invariant was violated and all properties hold for the given model.
Sources: README.md:13-15, specifications/Moving_Cat_Puzzle/manifest.json:17-18, specifications/EinsteinRiddle/manifest.json:17-18, specifications/N-Queens/manifest.json:20-21, specifications/MissionariesAndCannibals/manifest.json:17-18
Conclusion
The "Puzzles and Riddles" collection within the TLA⁺ Examples repository provides invaluable resources for both learning TLA⁺ and testing its toolchain. By offering a range of beginner-friendly and more advanced problems, these specifications demonstrate practical applications of formal methods in a clear and understandable context. The use of different verification tools and the documentation of expected outcomes in manifest.json files further enhance their utility as a robust test corpus and educational library.
Sources: README.md:3-8