====== Exercises ======

This page provides some execises you can use when learning tla+ or to brush your memory on the language.

===== Finder Exercises =====

These exercises ask you to write a spec that finds a solution to a problem, like a path through a maze. You can do this by writing an invariant saying "the goal state is impossible". TLC will then "solve" the problem by breaking the invariant!

==== Missionaries And Cannibals ====


  * Difficulty: Easy
  * Example solution: https:%%//%%github.com/tlaplus/Examples/tree/master/specifications/MissionariesAndCannibals
  * Type: Puzzle

In the missionaries and cannibals problem, three missionaries and three cannibals must cross a river using a boat which can carry at most two people, under the constraint that, for both banks, if there are missionaries present on the bank, they cannot be outnumbered by cannibals (if they were, the cannibals would eat the missionaries). The boat cannot cross the river by itself with no people on board. And, in some variations, one of the cannibals has only one arm and cannot row. From [[https://en.wikipedia.org/wiki/Missionaries_and_cannibals_problem|Wikipedia]].

Hint: You should specify the problem in TLA+ (define all the actors and how they interact with each other), then you can specify an invariant saying that this problem is impossible, and running model checking TLC should give you a sequence of logical steps to follow to solve the quiz.

==== Cabbage, Goat, and Wolf ====

  * Difficulty: Easy
  * Example solution: https:%%//%%muratbuffalo.blogspot.com/2023/10/cabbage-goat-and-wolf-puzzle-in-tla.html
  * Type: Puzzle

A farmer with a wolf, a goat, and a cabbage must cross a river by boat. The boat can carry only the farmer and a single item. If left unattended together, the wolf would eat the goat, or the goat would eat the cabbage. How can they cross the river without anything being eaten?

==== Cabbage, Goat, and Wolf ====
  * Difficulty: Easy
  * Example solution: https:%%//%%muratbuffalo.blogspot.com/2023/10/cabbage-goat-and-wolf-puzzle-in-tla.html
  * Type: Puzzle

A farmer must ferry a wolf, a goat, and a cabbage across a river in a boat that holds the farmer plus one item. If left alone together, the wolf eats the goat or the goat eats the cabbage. Find a crossing sequence that avoids any eating.
  * Explore next: Encode the state space and search for minimal crossings.


==== Car Talk Puzzle: Two Trains and a Fly ====
  * Difficulty: Easy
  * Example solution: https:%%//%%en.wikipedia.org/wiki/Fly_puzzle
  * Type: Puzzle

Two trains start L kilometers apart, heading toward each other at constant speeds v1 and v2. A fly starts on the nose of the first train and flies back and forth between the trains at speed f until the trains meet. How far does the fly travel?
  * Explore next: Generalize to variable speeds or acceleration profiles.

==== Cat in a Box (Schrödinger’s Cat) ====
  * Difficulty: Conceptual
  * Example solution: https:%%//%%en.wikipedia.org/wiki/Schr%C3%B6dinger%27s_cat
  * Type: Thought experiment
  * Commit: Initial commit
  * Date: Jul 30, 2025

A sealed box contains a cat and a quantum device with a 50% chance to trigger a poison release within an hour. Until observation, the cat is considered in a superposition of alive and dead. Discuss interpretation, measurement, and decoherence.
  * Explore next: Model the setup with simple quantum states and projection postulates.

==== Coffee Can Puzzle (Black and White Beans) ====
  * Difficulty: Medium
  * Example solution: https:%%//%%en.wikipedia.org/wiki/Coffee_can_problem
  * Type: Puzzle

A can contains black and white beans. Repeatedly draw two beans:
  * If they are the same color, discard both and add one black bean.
  * If different, discard both and add one white bean.
What determines the color of the final bean?
  * Explore next: Prove invariants and simulate outcomes for random initial counts.

==== Die Hard Water Jugs ====
  * Difficulty: Medium
  * Example solution: https:%%//%%en.wikipedia.org/wiki/Die_Hard_with_a_Vengeance#Water_jug_riddle
  * Type: Puzzle

You have an m-gallon jug and an n-gallon jug with no markings, and a water source. Measure exactly k gallons using filling, emptying, and pouring between jugs. Determine when this is possible and provide a minimal-step procedure.
  * Explore next: Use Bézout’s identity and graph search over jug states.

==== Dining Philosophers ====
  * Difficulty: Medium
  * Example solution: https:%%//%%en.wikipedia.org/wiki/Dining_philosophers_problem
  * Type: Concurrency problem

Five philosophers sit around a table with a fork between each pair. Each alternates thinking and eating; to eat, a philosopher needs both adjacent forks. Devise a protocol that avoids deadlock and starvation while allowing concurrent progress.
  * Explore next: Compare resource hierarchies, arbitrators, and Chandy–Misra solutions.


==== Game of Life ====
  * Difficulty: Open-ended
  * Example solution: https:%%//%%en.wikipedia.org/wiki/Conway%27s_Game_of_Life
  * Type: Cellular automaton

On an infinite grid of cells, each cell is either alive or dead. At each step:
  * A live cell with 2 or 3 neighbors survives.
  * A dead cell with exactly 3 neighbors becomes alive.
  * Otherwise the cell becomes or remains dead.
Study emergent patterns, universality, and computation within the automaton.
  * Explore next: Implement a simulator and search for oscillators, spaceships, and glider guns.

==== 100 Prisoners Problem ====
  * Difficulty: Hard
  * Example solution: https:%%//%%en.wikipedia.org/wiki/100_prisoners_problem
  * Type: Puzzle

100 prisoners each must find their own number inside one of 100 boxes, opening at most 50 boxes, with no communication once the process begins. If any fail, all lose. Describe the cycle-following strategy and analyze success probability.
  * Explore next: Vary box limits and analyze asymptotics with random permutations.

==== River Crossing with a Flashlight (Bridge and Torch) ====
  * Difficulty: Medium
  * Example solution: https:%%//%%en.wikipedia.org/wiki/Bridge_and_torch_problem
  * Type: Puzzle

Four people must cross a bridge at night with one flashlight. At most two can cross at once, moving at the slower person’s speed, and the flashlight must be carried on all crossings. Given crossing times, find the minimal total time.
  * Explore next: Compare the two canonical strategies and prove optimality.

==== Tower of Hanoi ====
  * Difficulty: Easy to Hard
  * Example solution: https:%%//%%en.wikipedia.org/wiki/Tower_of_Hanoi
  * Type: Puzzle

Move a stack of n discs from a source peg to a target peg using an auxiliary peg. Only one disc may be moved at a time, and a larger disc may never be placed on a smaller disc. Derive the recursive strategy and prove the 2^n − 1 move bound.
  * Explore next: Iterative Gray-code solution and parallel variants.


==== Ideas for an exercise? Update this page! ====
Hillel Wayne, author of learntla.com, has also put together a repo with TLA+ exercises: https://github.com/hwayne/tlaplus-exercises