Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
| learning:exercises [2024/09/28 15:58] – created - external edit 127.0.0.1 | learning:exercises [2025/03/07 21:23] (current) – Grouping both existing exercises under a common theme so we can add more groupings hwayne | ||
|---|---|---|---|
| Line 3: | Line 3: | ||
| This page provides some execises you can use when learning tla+ or to brush your memory on the language. | This page provides some execises you can use when learning tla+ or to brush your memory on the language. | ||
| - | ==== Table Of Contents: | + | ===== 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" | ||
| + | |||
| + | ==== Missionaries And Cannibals | ||
| - | < | ||
| - | <!-- toc --> | ||
| - | </ | ||
| - | ===== Missionaries And Cannibals ===== | ||
| * Difficulty: Easy | * Difficulty: Easy | ||
| Line 18: | Line 18: | ||
| 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. | 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 ===== | + | ==== Cabbage, Goat, and Wolf ==== |
| * Difficulty: Easy | * Difficulty: Easy | ||
127.0.0.1