This page provides some execises you can use when learning tla+ or to brush your memory on the language.
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!
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 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.
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?
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.
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?
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.
A can contains black and white beans. Repeatedly draw two beans:
What determines the color of the final bean?
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.
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.
On an infinite grid of cells, each cell is either alive or dead. At each step:
Study emergent patterns, universality, and computation within the automaton.
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.
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.
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.
Hillel Wayne, author of learntla.com, has also put together a repo with TLA+ exercises: https://github.com/hwayne/tlaplus-exercises