Hacker News new | past | comments | ask | show | jobs | submit login

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.

[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...


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact