There's a few I can think of! First, the TLA+ GitHub repo has a bunch of examples[0]. The best one to start with is the Die Hard puzzle[1], where the heroes must obtain four gallons of water given only three and five gallon jugs. In the spec[2] we set up the system and specify all possible actions; then we model-check the system to see whether it can spit out an execution trace of actions to reach a state where we have four gallons of water in a jug.
The Wikipedia article also has some good example specs[3].
For your own first specification, I personally cut my teeth on a river-crossing puzzle with a farmer, wolf, and sheep.
The Wikipedia article also has some good example specs[3].
For your own first specification, I personally cut my teeth on a river-crossing puzzle with a farmer, wolf, and sheep.
[0] https://github.com/tlaplus/Examples/tree/master/specificatio...
[1] https://www.youtube.com/watch?v=6cAbgAaEOVE
[2] https://github.com/tlaplus/Examples/blob/master/specificatio...
[3]https://en.wikipedia.org/wiki/TLA+