functional-programming-snake/course/12-property-testing.md

# Module 12 — Testing with properties (bonus)

> **Time:** ~4 h · **You'll edit:** JS `js/src/check.js` · Scala `scala/src/Check.scala` · F# `fsharp/src/Check.fs`
> **Tests:** JS `cd js && node --test "test/m12-*.test.js"` · Scala `cd scala && ./test.sh M12` · F# `cd fsharp && ./test.sh M12`
> **Prerequisites:** Modules 1–5 and Module 10, including the turn queue of Exercise 10.6 (you need `Random`, `update`, `history`, the `Frame` action and `queued`). Modules 6–9 and 11 are not needed.

## Why this module

Every test you have run in this course is an **example**: this state, this action, this expected state. Examples are precise, and they are easy to read. They also have one weakness, which Puzzle 3 of Module 10 showed: an example checks a case that somebody thought of. The first version of this course's speed-up rule had six fixture cases, all green, and still made the snake jump two cells in 25 ms after every third apple. Nobody had written the case "the score changes on this very frame", because nobody had thought of it. That is the kind of bug you are least likely to write an example for.

A **property** is a different kind of test. Instead of one input and its expected output, you state something that must be true for *every* input:

- every state of every game has the snake on the board;
- the snake never overlaps itself;
- the time between two moves is always `movesEvery(score)` frames.

Then you let the computer look for an input that breaks the statement, by trying hundreds of random ones. If it finds one, it hands you a **counterexample**.

Random tests have a bad reputation: they fail on Tuesday, pass on Wednesday, and nobody can reproduce the failure. That reputation comes from *hidden* randomness. You solved that problem in Module 4. A random test input is a value drawn from a `Random<A>` with a seed, so a failing test is reproduced by one number. And because the game is a fold over a list of actions (Module 5), a counterexample is a *replay*: a list you can run again, print, and cut down to the two key presses that matter.

In this module you build a small property-testing library from the parts you already have, about forty lines of code. Then you point it at deliberately broken versions of the game and watch it find each bug and reduce it to its essence. At the end you generate whole game states instead of games, and catch a bug that no statement about a single state can see, by comparing two implementations of the same rule.

## Learning objectives

After this module you can:

- **distinguish** an example-based test from a property, and **state** properties of several kinds (invariants, relations between runs, laws);
- **implement** generators of test data as `Random` values (`elementOf`, `listOf`) and recognise `listOf` as the same pattern as `sequence` from Module 7;
- **implement** a pure test runner `forAll` that returns a report with the counterexample and the seed that reproduces it;
- **implement** shrinking for lists (`removals`, `minimize`) and **explain** what "1-minimal" means and why total rules make shrinking easy;
- **write** an invariant checker for the game state and **explain** how it relates to "making illegal states unrepresentable";
- **judge** whether a property can detect anything at all, using deliberately broken implementations (mutants);
- **implement** a generator of structured data whose parts depend on each other (`genSnake`), and **explain** why the order of the draws is part of its contract;
- **use** a second, independently written implementation as a test oracle (`advanceSpec`), and **explain** which bugs it can and cannot find.

## Concepts

### 1. From examples to properties

Take `dropLast` from Module 1. An example test says:

```
dropLast([1, 2, 3])  is  [1, 2]
```

A property says something about every list `xs`:

```
for every list xs:   dropLast(xs) has length max(0, length(xs) - 1)
for every list xs:   dropLast(xs) is the beginning of xs
```

Neither property mentions a particular list, and together they pin `dropLast` down completely. To *check* a property you need three things: a way to produce many inputs, a way to run the check on each of them and report what happened, and, when it fails, a way to make the failing input small enough to understand. Those are the three parts of this module: **generators**, **`forAll`** and **shrinking**.

> **From everyday programming:** you may know *fuzzing*: throwing large amounts of random input at a parser or a network service to see whether it crashes. A property test is a fuzzer with an opinion. It does not only ask "did it crash?" but "is this statement about the result still true?", and it runs in milliseconds as part of the unit tests.

### 2. A generator is a `Random`

What is "a way to produce test inputs"? A function from a seed to a value and a new seed, so that the next input can be drawn from where the previous one stopped. You built exactly that type in Module 4:

```
Random<A>  =  seed -> [A, seed]
```

So there is no new type in this module. A generator of numbers below 10 is `intBelow(10)`. Two small combinators give you everything else the game needs:

- **`elementOf(xs)`** picks one element of a non-empty list: draw an index with `intBelow(length)` and look it up. That is a `map`.
- **`listOf(gen, n)`** draws `n` values from `gen`, one after another, and collects them in a list. The first draw uses the incoming seed, the second draw the seed the first one left behind, and so on.

`listOf` is worth a second look. "Run these computations one after another and collect the results" is what `sequence` did for `IO` in Module 7, and it is built the same way: from `flatMap` and `pure`, by recursion.

```
listOf(gen, 0)  =  pure([])
listOf(gen, n)  =  flatMap(gen, a => map(listOf(gen, n - 1), rest => [a, ...rest]))
```

Read the second line as: draw one value `a`; then draw the remaining `n - 1` values as a list `rest`; the result is `a` in front of `rest`. Nowhere do you see a seed. `flatMap` threads it, which is the reason you wrote `flatMap` in the first place.

With these two, a generator of random games is one line, and it is given in your stub:

```
genActions(n) = listOf(elementOf([Tick, Tick, Tick, Turn Up, Turn Down, Turn Left, Turn Right]), n)
```

`Tick` appears three times in the list, so about three actions in seven are ticks. Repeating an element is the simplest way to make it more likely.

**Language note.** JS: `listOf(gen, n)`, data first. Scala: `Check.listOf(gen, n)`. F#: `Check.listOf n gen`, data last, so that it reads `gen |> Check.listOf 40`.

### 3. `forAll`: a test runner that is a pure function

`forAll(gen, prop, runs, seed)` draws `runs` values from `gen`, starting from `seed`, and calls the property `prop` (a function from a value to a boolean) on each. It stops at the first value for which `prop` is false.

Most test frameworks report a failure by throwing an exception or printing to the console. Ours **returns a value**:

```
all runs passed:   Passed(runs)
a run failed:      Failed(run, seed, value)
```

- `run` is the number of the failing draw, counted from 0;
- `value` is the counterexample;
- `seed` is the seed *that draw started from*, so drawing from `gen` with `seed` gives `value` again.

In JS the report is a plain object, `{ ok: true, runs }` or `{ ok: false, run, seed, value }`. In Scala and F# it is a small sum type, `CheckResult`, given in your stub.

`forAll` has no loop counter and no "current seed" variable. It is a recursion that carries the run number and the seed as arguments, the same way `interval` carried `last` in Module 8.

Because `forAll` is pure, the test of a test runner is an ordinary equality: the same generator, property, number of runs and seed give the same report, every time, on every machine. A failure in one track's test suite can be reproduced in another track with the same seed, because all three tracks draw the same numbers (Module 4).

> **From everyday programming:** a *flaky* test is a test whose result depends on something it does not control: the clock, the order of a hash map, a random number. The usual cure is to hunt down each hidden input and pin it. Here there is nothing to hunt down. The only source of variation is the seed, and the seed is an argument.

### 4. Shrinking: from forty actions to two

Suppose `forAll` reports that this list of 40 random actions breaks a property:

```
Tick, Turn Down, Tick, Tick, Turn Right, Turn Up, Tick, Turn Left, Tick, Tick, Turn Up, Tick, ... (28 more)
```

Somewhere in there is a bug, but which of the 40 actions matter? The idea of **shrinking** is to let the computer find out: try smaller inputs, and keep any that still fails.

For a list, the simplest "smaller input" is the list with one element removed:

```
removals([a, b, c])  =  [[b, c], [a, c], [a, b]]
```

`minimize(xs, fails)` repeats one step: look through `removals(xs)` for the first list that still fails. If there is one, continue from it. If there is none, stop and return `xs`.

The result is called **1-minimal**: it fails, and removing any *single* element makes it pass. Every element of it is needed. It is not always the smallest failing list that exists. Take the (artificial) failure "the list has exactly one or exactly three elements": `minimize` stops at three elements, because every list of two passes, although a list of one would fail too. For bugs in real programs, 1-minimal is almost always good enough, and it is cheap: at most `n` rounds of at most `n` tries.

Why is this so easy for our game? Because of two decisions made long ago:

- **A game is a list of actions** (Module 5). The test input is plain data, so "a smaller input" has an obvious meaning.
- **The rules are total** (Module 3). *Every* list of actions is a valid game. If `turn` threw an exception for an illegal turn, most of the shortened lists would crash for reasons that have nothing to do with the bug, and the shrinker would be led astray. Because "does not apply" means "unchanged", you can delete any action from any game and still have a game.

> **From everyday programming:** this is what you do by hand with a bug report. A user sends twenty steps to reproduce a crash; you leave out a step, try again, and keep going until every remaining step is needed. `git bisect` automates the same search over a list of commits. The technique has a name, *delta debugging*, and `minimize` is its simplest form.

### 5. What to check: invariants

The most useful properties of a program with state are its **invariants**: statements that hold for every state the program can ever reach.

Module 2 was honest about the model: the types rule out some nonsense (a status that is paused *and* over), but a `GameState` can still be built with a snake outside the board, an apple inside the snake, or a snake whose cells are scattered across the board. Types could not exclude those states, at least not conveniently. The *rules* are supposed to: starting from `newGame(seed)`, no sequence of actions should ever produce one.

An invariant checker turns that claim into a function:

```
violations(state)  =  the names of the invariants this state breaks   (an empty list: the state is sane)
```

| Name | The state is sane when... |
|---|---|
| `snake-not-empty` | the snake has at least one cell |
| `snake-in-bounds` | every cell of the snake is on the board |
| `snake-no-overlap` | no two cells of the snake are equal |
| `snake-connected` | each cell of the snake is exactly one step (up, down, left or right) from the one before it |
| `apple-in-bounds` | the apple, if there is one, is on the board |
| `apple-not-on-snake` | the apple, if there is one, is not on a cell of the snake |
| `turn-not-reversed` | `nextDir` is not the opposite of `dir` |
| `queued-not-reversed` | `queued` is none, or is not the opposite of `nextDir` (the turn queue of Module 10) |

`violations` returns the names in this order. It returns names and not a single boolean, so that a failing test says *what* is wrong. Each row is one small predicate; the function is a `filter` over a table of (name, predicate) pairs.

The property is then one line:

```
for every list of 40 random actions:   every state in history(newGame(1), actions) has no violations
```

Think of invariants as the part of "make illegal states unrepresentable" that the type system left over. Where a type can exclude a bad state, use the type: the compiler checks it for all programs, for free. Where it cannot, write the invariant down as a function and check it on thousands of random games.

### 6. What to check: relations and laws

Invariants look at one state at a time. Some requirements are about how states relate to each other.

**A relation between moments of one run.** "Every step of the snake lasts exactly `movesEvery(score)` frames" is a statement about a whole history. To check it, you need the *gaps* between consecutive moves:

```
moveGaps(states)  =  the distances between the positions in the list where the head moved
```

The snake "moves at index `i`" when the head of `states[i]` differs from the head of `states[i - 1]`. If it moves at indices 2, 5 and 12, the gaps are `[3, 7]`. With `moveGaps` the requirement of Module 10 becomes checkable, and the tests of this module run it against the tempting rule of Puzzle 3.

**Laws.** Some equations hold between whole computations, for example the replay law of Module 5:

```
replay(s, a ++ b)  ==  replay(replay(s, a), b)
```

Here is a question that separates a useful property from a useless one: **could this property ever fail?** Look at the replay law again. It follows from the definition of a fold, for *any* step function whatsoever. A game in which the snake teleports, an `update` that ignores every action, a version full of bugs: all of them satisfy it. So a test of this law tests `replay` (is it really a left fold?) and tells you nothing about the game.

There is a practical way to answer "could it fail?": break the program on purpose and see whether the property notices. A deliberately broken copy is called a **mutant**, and a mutant that fails a test is said to be *killed*. The last tests of this module do exactly that, with these mutants:

| Mutant | The bug | Caught by |
|---|---|---|
| `turn` checks against `nextDir` | Puzzle 2 of Module 3: the quick double turn | `turn-not-reversed` |
| `advance` forgets the walls | the snake walks off the board | `snake-in-bounds` |
| `Tick` forgets the turn queue | Exercise 10.6 done in `Frame` but not in `Tick` | `queued-not-reversed` |
| the queue accepts a reversal | Exercise 10.6 without the "not the opposite of `nextDir`" check | `queued-not-reversed` |
| the tempting frame rule | Puzzle 3 of Module 10: steps of uneven length | the gaps of `moveGaps` |
| `advance` checks the *old* snake | Puzzle 1 of Module 3: death by the tail that is moving away | comparison with `advanceSpec` (section 8) |

For the first four, the tests also shrink the counterexample, and the results are worth predicting. What is the shortest list of actions that makes a snake reverse into itself if `turn` checks the wrong direction? What is the shortest list that walks the snake of `newGame(1)` off a board without walls? (The head starts at `x = 10` on a board 20 wide, heading `Right`.) Decide before you run the tests; the test titles give the answers.

### 7. Generating states, not only games

Every test input so far has been a list of actions, played from `newGame`. That only reaches the states that random play reaches, and random play is a poor explorer: the snake grows only when it eats, and forty random actions rarely eat more than one apple. A long snake coiled up so that its head is right next to its own tail, the situation of Puzzle 1, practically never happens.

When the function under test takes *one state*, as `advance` does, you can skip the game and generate the state directly. The difficulty is that the parts of a state depend on each other. The snake's cells must be neighbours and must not repeat; `dir` must agree with the first two cells; the apple must be on a free cell. A generator that drew each field independently would produce almost nothing but nonsense, and a test of `advance` on nonsense says nothing about the game.

The way out is to **draw the parts in the order in which they depend on each other**, each draw using what the earlier ones produced. That is exactly what `flatMap` does: the next generator is chosen *from the value of the previous one*. For the snake:

```
genSnake(width, height, maxLen):
  draw the head: x with intBelow(width), then y with intBelow(height)
  then, until the snake has maxLen cells:
    the candidates are the neighbours of the LAST cell, in the order Up, Down, Left, Right,
    that are on the board and not yet in the snake
    if there are none, stop early; otherwise append elementOf(candidates) and go on
```

From seed 0 on a 5 x 5 board with `maxLen` 6, the head is (3,2) and the walk continues up and then left along the top row:

```
        x=0  x=1  x=2  x=3  x=4
  y=0    5    4    3    2    .        snake (head first): (3,2) (3,1) (3,0) (2,0) (1,0) (0,0)
  y=1    .    .    .    1    .        the numbers give the order in which the cells were drawn
  y=2    .    .    .    H    .
  y=3    .    .    .    .    .
  y=4    .    .    .    .    .
```

The order of the draws, and the order Up, Down, Left, Right of the candidates, are part of `genSnake`'s contract, written in the stub. They decide which snake a seed gives. Because all three tracks follow them, a counterexample found from a seed in one track is the same counterexample in the others.

`genState(width, height)` is given in your stub and builds on `genSnake`: a length limit between 1 and `width * height`, a snake, `dir` read off the first two cells (`Right` for a one-cell snake), `nextDir` equal to `dir` or a perpendicular direction, an apple on a random free cell or none, and nothing queued. Read it: it is four `flatMap`s, each one choosing the next generator from what came before.

A generator is code, and code has bugs. If `genState` produced a disconnected snake, every later test would complain about states the game can never reach, and you would hunt for bugs that are not there. So the first test of a generator is a property *of the generator*: `every generated state is sane: 500 states of a 5x5 board have no violations`.

> **From everyday programming:** test-data builders and factories (a `UserFactory` that fills in a valid email, a hashed password and a creation date before an account object is saved) solve the same problem: produce objects whose fields satisfy the constraints between them, so that the test can concentrate on what it wants to check. A property-testing generator is a factory that picks *random* valid objects, and can therefore find the valid object nobody thought of.

### 8. A second implementation as an oracle

Generated states make it possible to test `advance` on hundreds of coiled-up snakes. But test it against *what*? Invariants say whether a state is sane, and the bug of Puzzle 1 produces only sane states: it ends the game one step too early, and a finished game is a perfectly valid state. To catch a result that is valid but *wrong*, you need to know the right result. Something that knows it is called a **test oracle**.

For one hand-written example, the oracle is you: you write the expected state into a fixture. For 500 random states, you need a program. The usual answer is **a second implementation**, written independently, and the property

```
for every generated state s:   advance(s) == advanceSpec(s)
```

The second implementation is only useful if it does not share the first one's mistakes, so it should be written in a different way. Module 3's `advance` decides about the *new head*: compute the body that remains, then ask whether the head lands on the board and outside that body. `advanceSpec` decides about the *resulting snake*: build the whole snake the step would produce (the new head in front, then the old snake without its last cell unless eating), and ask `violations`, the checker you wrote in Exercise 12.4, whether that snake is on the board and free of overlap. If it is not, the step is deadly, and the result is Module 3's game over. It is the rule stated as a requirement on the outcome: "after a step, the snake must still be a legal snake".

Now look at the wrong check of Puzzle 1 again: "the new head must not be on the *old* snake". It is a statement about the old snake, and it disagrees with "the new snake must not overlap" exactly when the head moves onto the cell the tail is leaving. The comparison test finds such a state in the 22nd draw (run 21) from seed 2024:

```
        x=0  x=1  x=2  x=3  x=4
  y=0    1    2    .    .    .        snake (head first): (0,1) (0,0) (1,0) (1,1) (1,2) (1,3) (0,3) (0,2)
  y=1    H    3    .    .    .        heading Down; the head's next cell (0,2) is the tail T
  y=2    T    4    .    .    .        A is the apple
  y=3    6    5    A    .    .
  y=4    .    .    .    .    .
```

The wrong check says "game over"; `advanceSpec` says the snake moves on, its tail having left (0,2) at the same moment. No invariant could have said which one is right, and the test `no invariant sees the wrong collision check of Puzzle 1: every state it produces is sane` shows that, too.

Two caveats. An oracle written by the same person on the same afternoon can share a *misunderstanding* of the rules with the code it checks; then the two agree and are both wrong. That is what the example fixtures, written from the specification, are for: `advanceSpec` must also pass Module 3's twelve `advance` cases. And an oracle has to be simpler or more obviously right than the code it checks, or you have only doubled the code you must trust. `advanceSpec` is simpler in one sense: it delegates the whole question "is this a legal snake?" to a function that was already tested on its own.

> **From everyday programming:** this is *differential testing*. When a team rewrites a slow service, they often run the old and the new version side by side on the same requests and compare the answers before switching. Compiler writers generate random programs and compare the output of two compilers. A refactoring is safe to the extent that the code after it agrees with the code before it, and keeping the old version around as an oracle turns that into a test.

### 9. What random testing does not find

Be as honest about this tool as Module 2 was about the model.

- **A property only sees what it states.** The invariants of section 5 cannot see the wrong collision check of Puzzle 1: it ends the game too early, and a game that has ended is still a sane state. Catching it took a different kind of property, the comparison with a second implementation of section 8. That one has its own blind spot: it cannot see a mistake that both implementations make.
- **Random inputs reach the likely states.** Forty random actions from a new game almost never eat three apples. So random play from `newGame` would practically never reach the first speed-up, and would not find the bug of Puzzle 3. The tests therefore start from a hand-made state: a long corridor with the third apple right in front of the head, and a random number of frames already counted. Generating states directly (section 7) is the other answer. Choosing where to start and what to generate is the real craft of property testing.
- **Passing is evidence, not proof.** 300 random games that keep every invariant make a bug less likely. They do not show that there is none. A proof needs reasoning (as in question 3 of Module 5) or a tool that explores *every* reachable state.

## Exercises

> **About test names.** The test titles quoted under "Tests" are the JavaScript ones; the JS runner prints them with the module in front (`m12 listOf threads the seed from each draw to the next`). The Scala and F# suites test the same things one-to-one, in each track's vocabulary (`Passed`/`Failed` instead of `ok`). Failing tests are reported by name when you run the module's tests; to read all titles, open `scala/test/M12Check.test.scala` or `fsharp/tests/M12Check.fs`. Fixture-based tests have the same case names in every track.

All functions are pure: no loops, no reassignment, no mutation. The purity audit checks this file like every other.

### Exercise 12.1 — `elementOf` and `listOf`

**JavaScript**
```js
export const elementOf = (xs) => ...          // Random<A>, for a non-empty array xs
export const listOf = (gen, n) => ...         // Random<A[]>
```
**Scala**
```scala
def elementOf[A](xs: List[A]): Random[A]
def listOf[A](gen: Random[A], n: Int): Random[List[A]]
```
**F#**
```fsharp
let elementOf (xs: 'a list) : Random<'a>
let listOf (n: int) (gen: Random<'a>) : Random<'a list>
```

Tests: `elementOf picks the element at the index drawn by intBelow`, `elementOf of a one-element array always gives that element, and still uses up a draw`, `listOf(gen, 0) is the empty list and leaves the seed alone`, `listOf threads the seed from each draw to the next`, `listOf of a constant generator repeats the value and leaves the seed alone`, `genActions(n) gives n actions, the same ones for the same seed`.

Watch out: write both with `map`, `flatMap` and `pure` from Module 4. If you find yourself unpacking a `[value, seed]` pair, you are doing by hand what `flatMap` does for you.

### Exercise 12.2 — `forAll`

**JavaScript**
```js
export const forAll = (gen, prop, runs, seed) => ...
// { ok: true, runs }  or  { ok: false, run, seed, value }
```
**Scala**
```scala
enum CheckResult[+A]:                 // given
  case Passed(runs: Int)
  case Failed(run: Int, seed: Long, value: A)

def forAll[A](gen: Random[A], runs: Int, seed: Long)(prop: A => Boolean): CheckResult[A]
```
**F#**
```fsharp
type CheckResult<'a> =                // given
    | Passed of runs: int
    | Failed of run: int * seed: uint32 * value: 'a

let forAll (runs: int) (seed: uint32) (prop: 'a -> bool) (gen: Random<'a>) : CheckResult<'a>
```

Tests: `forAll reports success with the number of runs`, `forAll with zero runs succeeds without drawing anything`, `forAll reports the first failing draw, its value and the seed it started from`, `forAll stops at the first failure: the property is not asked about later values`, `forAll is reproducible: same generator, property, runs and seed give the same report`.

Watch out: the `seed` in a failure report is the seed the failing draw *started from*, not the one it left behind. And each draw must continue from the previous draw's leftover seed; if every draw starts from the same seed, you test the same value `runs` times.

### Exercise 12.3 — `removals` and `minimize`

**JavaScript**
```js
export const removals = (xs) => ...           // removals([1, 2, 3]) -> [[2, 3], [1, 3], [1, 2]]
export const minimize = (xs, fails) => ...    // fails: list -> boolean, and fails(xs) is true
```
**Scala**
```scala
def removals[A](xs: List[A]): List[List[A]]
def minimize[A](xs: List[A])(fails: List[A] => Boolean): List[A]
```
**F#**
```fsharp
let removals (xs: 'a list) : 'a list list
let minimize (fails: 'a list -> bool) (xs: 'a list) : 'a list
```

Tests: `removals lists every way to drop one element, in order`, `removals of an empty list is empty, and of a single element is one empty list`, `minimize keeps exactly the elements the failure needs`, `minimize keeps the order and the duplicates the failure needs`, `minimize of a list that fails whatever you remove is the empty list`, `minimize returns a list that still fails and has no failing removal (1-minimal)`.

Watch out: continue with the **first** failing removal, in the order of `removals`. The tracks must agree on which minimal list they report.

### Exercise 12.4 — `violations`

**JavaScript**
```js
export const violations = (state) => ...      // string[], in the order of the table in section 5
```
**Scala**
```scala
def violations(state: GameState): List[String]
```
**F#**
```fsharp
let violations (state: GameState) : string list
```

Fixture: `fixtures/m12-violations.json`, 21 cases: six sane states (`a-sane-state-has-no-violations`, `no-apple-is-fine`, `a-one-cell-snake-is-fine`, `a-queued-turn-is-fine`, ...), one or two cases per invariant (`head-off-the-right-edge`, `snake-with-a-diagonal-step`, `apple-on-the-tail`, `pending-turn-straight-back`, `queued-turn-straight-back-from-the-pending-turn`, ...), `several-violations-are-listed-in-order` and `reversed-pending-turn-and-reversed-queue-are-both-listed`.

Watch out: `snake-no-overlap` and `snake-connected` are different. A snake with the same cell twice in a row (`doubled-cell-counts-as-overlap-and-as-disconnected`) breaks both: the cells overlap, and they are zero steps apart, not one. Reuse `inBounds` from Module 3 and `contains` from Module 1. `queued-not-reversed` compares with `nextDir`, not with `dir`: in `a-queued-turn-is-fine` the snake moves `Right`, `Up` is pending and `Left` is queued, which is fine.

### Exercise 12.5 — `moveGaps`

**JavaScript**
```js
export const moveGaps = (states) => ...       // number[]
```
**Scala**
```scala
def moveGaps(states: List[GameState]): List[Int]
```
**F#**
```fsharp
let moveGaps (states: GameState list) : int list
```

Tests: `moveGaps measures the distance between consecutive moves of the head`, `moveGaps of fewer than two moves is empty`.

### Exercise 12.6 — `genSnake`

**JavaScript**
```js
export const genSnake = (width, height, maxLen) => ...   // Random<Point[]>, head first; maxLen >= 1
```
**Scala**
```scala
def genSnake(width: Int, height: Int, maxLen: Int): Random[List[Point]]
```
**F#**
```fsharp
let genSnake (width: int) (height: int) (maxLen: int) : Random<Point list>
```

Draw exactly as section 7 and the stub's doc comment say: the head's `x`, then its `y`, then one `elementOf` per further cell among the free in-bounds neighbours of the *last* cell, in the order Up, Down, Left, Right; stop at `maxLen` cells or when there is no candidate.

Tests: `genSnake draws the head first, then walks from the tail (seed 0, 5x5, at most 6 cells)`, `genSnake is pinned for a few more seeds`, `genSnake with maxLen 1 is just the head, drawn with two draws`, `genSnake stops early when the walk is stuck: a 1x1 board holds one cell`, `genSnake always gives a snake on the board, connected, without overlap, at most maxLen long`, and, through the given `genState`, `every generated state is sane: 500 states of a 5x5 board have no violations` and `generated states are Playing, have nothing queued, and vary in length and apple`.

Watch out: the walk extends the snake at its *tail* (the last cell), and the snake is head first, so new cells go at the end of the list. Stopping early must not use up a draw: when there are no candidates, return the snake with `pure`. And do not draw the head as one random cell from a list of all cells: that is a different draw, and the pinned tests will tell you so.

### Exercise 12.7 — `advanceSpec`

**JavaScript**
```js
export const advanceSpec = (state) => ...      // GameState; must equal advance(state) on every sane state
```
**Scala**
```scala
def advanceSpec(state: GameState): GameState
```
**F#**
```fsharp
let advanceSpec (state: GameState) : GameState
```

Write it as section 8 describes, without calling `advance`: build the snake the step would produce, then let `violations` decide whether it contains `snake-in-bounds` or `snake-no-overlap`.

Tests: `advanceSpec agrees with Module 3's advance fixture: …` (one test per case of `fixtures/m03-advance.json`), `advance and advanceSpec agree on 500 generated states of a 5x5 board`, `no invariant sees the wrong collision check of Puzzle 1: every state it produces is sane`, `comparing with advanceSpec catches the wrong collision check: the head was moving onto the tail`.

Watch out: ask `violations` about the state *with the new snake*, and look only at the two snake invariants. When the step eats, the new head is on the apple, so `apple-not-on-snake` is in the list too, and that does not make the step deadly. Game over keeps the old snake and records `dir = nextDir`, exactly as in Module 3.

### The payoff

When 12.1–12.5 are green, the remaining tests of the module run your library against the game. They need no code from you; read them in the test file, because they show how the pieces are used together:

- `the real game keeps every invariant on 300 random games of 40 actions`;
- `the quick double turn bug is found and shrunk to its two key presses`;
- `a game without walls is found and shrunk to the shortest way off the board: ten ticks`;
- `a Tick that forgets the queued turn is caught by queued-not-reversed and shrunk to four actions`;
- `a queue that accepts a reversal is found and shrunk to its two key presses`;
- `the real game moves exactly every movesEvery(score) frames, also across a speed-up`;
- `counting frames from the start of the game makes some steps too short, and the property finds one`.

If the first of these fails, do not assume that your library is wrong. It may have found a real bug in *your* rules that the fixtures missed. Shrink the counterexample and look at it.

### Run

- JS: `cd js && node --test "test/m12-*.test.js"`
- Scala: `cd scala && ./test.sh M12`
- F#: `cd fsharp && ./test.sh M12`

## Hints

<details><summary>Exercise 12.1 (elementOf, listOf) — nudge</summary>

`elementOf` is "a random index, transformed into the element at that index". `listOf` is recursion on `n`: what is a list of zero draws, and how do you get a list of `n` draws from one draw and a list of `n - 1` draws?

</details>

<details><summary>Exercise 12.1 (elementOf, listOf) — stronger hint</summary>

`elementOf(xs)`: `map` over `intBelow(length of xs)`. `listOf(gen, n)`: if `n` is 0 (or less), `pure` of the empty list. Otherwise `flatMap` over `gen`; inside, you have the first value `a` and need a `Random` of the whole list: `map` over `listOf(gen, n - 1)` and put `a` in front. In F# remember that the function is `bind` and that the data comes last.

</details>

<details><summary>Exercise 12.1 (elementOf, listOf) — near-solution (try the others first)</summary>

```js
export const elementOf = (xs) => map(intBelow(___), (i) => ___)
export const listOf = (gen, n) =>
  n <= 0 ? pure(___) : flatMap(gen, (a) => map(listOf(gen, ___), (rest) => [___, ...___]))
```
```scala
def elementOf[A](xs: List[A]): Random[A] = Random.intBelow(___).map(i => ___)
def listOf[A](gen: Random[A], n: Int): Random[List[A]] =
  if n <= 0 then Random.pure(___)
  else gen.flatMap(a => listOf(gen, ___).map(rest => ___ :: ___))
```
```fsharp
let elementOf (xs: 'a list) : Random<'a> = Random.intBelow ___ |> Random.map (fun i -> List.item i xs)
let rec listOf (n: int) (gen: Random<'a>) : Random<'a list> =
    if n <= 0 then Random.pure ___
    else gen |> Random.bind (fun a -> listOf ___ gen |> Random.map (fun rest -> ___ :: ___))
```

</details>

<details><summary>Exercise 12.2 (forAll) — nudge</summary>

Write a helper that takes the number of the current run and the current seed. It has three outcomes: all runs are done; this value passes, so go on with the next run and the leftover seed; this value fails, so report.

</details>

<details><summary>Exercise 12.2 (forAll) — stronger hint</summary>

`go(i, s)`: if `i` has reached `runs`, the result is the success report. Otherwise run `gen` with `s` to get the value and the next seed. If `prop(value)` holds, the result is `go(i + 1, nextSeed)`. If not, the result is the failure report with `i`, `s` (not `nextSeed`) and the value. `forAll` is `go(0, seed)`. In Scala, mark the helper `@annotation.tailrec`; in F#, `let rec` with the recursive call in tail position.

</details>

<details><summary>Exercise 12.2 (forAll) — near-solution (try the others first)</summary>

```js
export const forAll = (gen, prop, runs, seed) => {
  const go = (i, s) => {
    if (i >= runs) return { ok: true, runs }
    const [value, next] = run(gen, s)
    return prop(value) ? go(___, ___) : { ok: false, run: ___, seed: ___, value }
  }
  return go(0, seed)
}
```
```scala
def forAll[A](gen: Random[A], runs: Int, seed: Long)(prop: A => Boolean): CheckResult[A] =
  @annotation.tailrec
  def go(i: Int, s: Long): CheckResult[A] =
    if i >= runs then CheckResult.Passed(runs)
    else
      val (value, next) = gen.run(s)
      if prop(value) then go(___, ___) else CheckResult.Failed(___, ___, value)
  go(0, seed)
```
```fsharp
let forAll (runs: int) (seed: uint32) (prop: 'a -> bool) (gen: Random<'a>) : CheckResult<'a> =
    let rec go i s =
        if i >= runs then Passed runs
        else
            let (value, next) = Random.run s gen
            if prop value then go ___ ___ else Failed(___, ___, value)
    go 0 seed
```

</details>

<details><summary>Exercise 12.3 (removals, minimize) — nudge</summary>

`removals`: for each index, the list without the element at that index. `minimize`: find the first removal that still fails; what do you do with it, and what do you do when there is none?

</details>

<details><summary>Exercise 12.3 (removals, minimize) — stronger hint</summary>

`removals` in JS: `map` with the index, and build each list from two `slice`s. In Scala, `xs.indices.toList.map(i => xs.patch(i, Nil, 1))`; in F#, `List.mapi` with `List.removeAt` (or recursion on the list: removing from `x :: rest` is either `rest`, or `x` in front of each removal of `rest`). `minimize`: `find` (`List.tryFind`) the first failing removal. If there is one, the answer is `minimize` of it. If not, the answer is `xs`.

</details>

<details><summary>Exercise 12.3 (removals, minimize) — near-solution (try the others first)</summary>

```js
export const removals = (xs) => xs.map((_, i) => [...xs.slice(0, ___), ...xs.slice(___)])
export const minimize = (xs, fails) => {
  const smaller = removals(xs).find(___)
  return smaller === undefined ? ___ : minimize(___, fails)
}
```
```scala
def removals[A](xs: List[A]): List[List[A]] = xs.indices.toList.map(i => xs.patch(i, Nil, ___))
def minimize[A](xs: List[A])(fails: List[A] => Boolean): List[A] =
  removals(xs).find(___) match
    case Some(smaller) => minimize(___)(fails)
    case None          => ___
```
```fsharp
let removals (xs: 'a list) : 'a list list = xs |> List.mapi (fun i _ -> List.removeAt ___ xs)
let rec minimize (fails: 'a list -> bool) (xs: 'a list) : 'a list =
    match removals xs |> List.tryFind ___ with
    | Some smaller -> minimize fails ___
    | None -> ___
```

</details>

<details><summary>Exercise 12.4 (violations) — nudge</summary>

Do not write eight `if`s that push onto a list. Write a table: a list of pairs (name, a function that says whether the state is fine). Then the result is "the names of the pairs whose function says no".

</details>

<details><summary>Exercise 12.4 (violations) — stronger hint</summary>

The predicates, on a state `s`: the snake's length is above 0; every snake cell satisfies `inBounds`; for every cell, the cells *after* it do not contain it; every cell from the second on is a neighbour of the cell before it (the sum of the absolute differences of `x` and `y` is exactly 1); the apple is absent or in bounds; the apple is absent or not contained in the snake; `nextDir` differs from `opposite(dir)`; `queued` is absent or differs from `opposite(nextDir)`. For "each cell and the one before it", pair the snake with itself shifted by one: in JS use the index argument of `every`, in Scala `snake.zip(snake.drop(1))`, in F# `List.pairwise`.

</details>

<details><summary>Exercise 12.4 (violations) — near-solution (try the others first)</summary>

```js
const neighbours = (a, b) => Math.abs(a.x - b.x) + Math.abs(a.y - b.y) === 1
const invariants = [
  ['snake-not-empty', (s) => s.snake.length > 0],
  ['snake-in-bounds', (s) => s.snake.every((p) => ___)],
  ['snake-no-overlap', (s) => s.snake.every((p, i) => !contains(s.snake.slice(___), p, pointEquals))],
  ['snake-connected', (s) => s.snake.slice(1).every((p, i) => neighbours(s.snake[___], p))],
  ['apple-in-bounds', (s) => s.apple === null || ___],
  ['apple-not-on-snake', (s) => s.apple === null || ___],
  ['turn-not-reversed', (s) => ___],
  ['queued-not-reversed', (s) => s.queued === null || ___],
]
export const violations = (state) => invariants.filter(([, holds]) => ___).map(([name]) => name)
```

The Scala and F# versions have the same shape: a `List` of `(String, GameState => Boolean)` pairs, then `filterNot`/`List.filter` and `map`. With `snake.zip(snake.drop(1)).forall { case (a, b) => ... }` or `List.pairwise snake |> List.forall (fun (a, b) -> ...)` for the connected check, and `apple.forall(p => ...)` / `Option.forall (fun p -> ...) apple` for "absent or fine".

</details>

<details><summary>Exercise 12.5 (moveGaps) — nudge</summary>

Two steps. First the list of indices at which the head moved. Then the differences between neighbours in that list.

</details>

<details><summary>Exercise 12.5 (moveGaps) — stronger hint</summary>

Step 1: pair each state with the one before it (JS: `map` with the index, look at `states[i - 1]`; Scala: `states.zip(states.drop(1)).zipWithIndex`; F#: `List.pairwise` and `List.indexed`), keep the indices where the two heads differ. Mind the off-by-one: the pair of states 0 and 1 is a move *at index 1*. Step 2: pair the list of indices with itself shifted by one and subtract.

</details>

<details><summary>Exercise 12.5 (moveGaps) — near-solution (try the others first)</summary>

```js
export const moveGaps = (states) => {
  const moved = states
    .map((s, i) => (i > 0 && !pointEquals(s.snake[0], states[___].snake[0]) ? i : -1))
    .filter((i) => i >= 0)
  return moved.slice(1).map((i, k) => i - moved[___])
}
```
```scala
def moveGaps(states: List[GameState]): List[Int] =
  val moved = states.zip(states.drop(1)).zipWithIndex.collect {
    case ((before, after), i) if before.snake.headOption != after.snake.headOption => ___
  }
  moved.zip(moved.drop(1)).map((a, b) => ___)
```
```fsharp
let moveGaps (states: GameState list) : int list =
    states
    |> List.pairwise
    |> List.indexed
    |> List.filter (fun (_, (before, after)) -> List.tryHead before.Snake <> List.tryHead after.Snake)
    |> List.map (fun (i, _) -> ___)
    |> List.pairwise
    |> List.map (fun (a, b) -> ___)
```

</details>

<details><summary>Exercise 12.6 (genSnake) — nudge</summary>

Write a helper that takes the snake built so far and the number of cells still allowed, and returns a `Random` of the finished snake. It has three outcomes: no cells left to add; no candidate cell; or pick a candidate and continue. `genSnake` draws the head and then calls the helper.

</details>

<details><summary>Exercise 12.6 (genSnake) — stronger hint</summary>

`grow(snake, left)`: if `left` is 0 (or less), `pure(snake)`. Otherwise take the last cell, `move` it in each of Up, Down, Left, Right (in that order), and keep the cells for which `inBounds` holds (it only reads `width` and `height`, so a small record with those two fields will do) and which the snake does not `contain`. No candidates: `pure(snake)`. Otherwise `flatMap` over `elementOf(candidates)` and continue with the snake plus that cell and `left - 1`. `genSnake` is `flatMap` over `intBelow(width)`, inside it `flatMap` over `intBelow(height)`, and inside that `grow([head], maxLen - 1)`.

</details>

<details><summary>Exercise 12.6 (genSnake) — near-solution (try the others first)</summary>

```js
const directions = ['Up', 'Down', 'Left', 'Right']
const grow = (width, height, snake, left) => {
  if (left <= 0) return ___
  const last = snake[snake.length - 1]
  const options = directions
    .map((d) => move(last, d))
    .filter((p) => inBounds({ width, height }, p) && !___)
  return options.length === 0 ? ___ : flatMap(elementOf(options), (p) => grow(width, height, [___, p], ___))
}
export const genSnake = (width, height, maxLen) =>
  flatMap(intBelow(width), (x) => flatMap(intBelow(___), (y) => grow(width, height, [point(x, y)], ___)))
```
```scala
def genSnake(width: Int, height: Int, maxLen: Int): Random[List[Point]] =
  def grow(snake: List[Point], left: Int): Random[List[Point]] =
    val options = List(Direction.Up, Direction.Down, Direction.Left, Direction.Right)
      .map(d => Rules.move(snake.last, d))
      .filter(p => p.x >= 0 && p.x < width && p.y >= 0 && p.y < height && ___)
    if left <= 0 || options.isEmpty then Random.pure(___)
    else elementOf(options).flatMap(p => grow(snake :+ ___, ___))
  Random.intBelow(width).flatMap(x => Random.intBelow(___).flatMap(y => grow(List(Point(x, y)), ___)))
```
```fsharp
let genSnake (width: int) (height: int) (maxLen: int) : Random<Point list> =
    let rec grow (snake: Point list) (left: int) : Random<Point list> =
        let options =
            [ Up; Down; Left; Right ]
            |> List.map (fun d -> Rules.move (List.last snake) d)
            |> List.filter (fun p -> p.X >= 0 && p.X < width && p.Y >= 0 && p.Y < height && ___)
        if left <= 0 || List.isEmpty options then Random.pure ___
        else elementOf options |> Random.bind (fun p -> grow (snake @ [ ___ ]) ___)
    Random.intBelow width |> Random.bind (fun x -> Random.intBelow ___ |> Random.bind (fun y -> grow [ { X = x; Y = y } ] ___))
```

</details>

<details><summary>Exercise 12.7 (advanceSpec) — nudge</summary>

Follow the Module 3 shape of compute, decide, build. Compute the new head, whether it eats, and the whole new snake. Decide by asking `violations` about the state with that snake. Build one of the two results.

</details>

<details><summary>Exercise 12.7 (advanceSpec) — stronger hint</summary>

Not `Playing`: return the state. `head = move(snake[0], nextDir)`; `eating` = the apple is there and equals `head`; `snake' = [head, ...(eating ? snake : dropLast(snake))]`. `broken` = `violations` of the state with `snake'` contains `'snake-in-bounds'` or `'snake-no-overlap'`. If broken: the state with `dir: nextDir` and `status: 'GameOver'`. Otherwise: the state with `snake'`, `dir: nextDir`, the apple gone if eating, and the score plus one if eating.

</details>

<details><summary>Exercise 12.7 (advanceSpec) — near-solution (try the others first)</summary>

```js
export const advanceSpec = (state) => {
  if (state.status !== 'Playing') return state
  const head = move(state.snake[0], state.nextDir)
  const eating = state.apple !== null && pointEquals(head, state.apple)
  const snake = [head, ...(eating ? ___ : ___)]
  const broken = violations({ ...state, snake }).some((v) => v === ___ || v === ___)
  return broken
    ? { ...state, dir: state.nextDir, status: ___ }
    : { ...state, snake, dir: state.nextDir, apple: ___, score: ___ }
}
```
```scala
def advanceSpec(state: GameState): GameState =
  if state.status != Status.Playing then state
  else
    val head = Rules.move(state.snake.head, state.nextDir)
    val eating = state.apple.contains(head)
    val snake = head :: (if eating then ___ else ___)
    val broken = violations(state.copy(snake = snake)).exists(v => v == ___ || v == ___)
    if broken then state.copy(dir = state.nextDir, status = ___)
    else state.copy(snake = snake, dir = state.nextDir, apple = ___, score = ___)
```
```fsharp
let advanceSpec (state: GameState) : GameState =
    if state.Status <> Playing then state
    else
        let head = Rules.move (List.head state.Snake) state.NextDir
        let eating = state.Apple = Some head
        let snake = head :: (if eating then ___ else ___)
        let broken = violations { state with Snake = snake } |> List.exists (fun v -> v = ___ || v = ___)
        if broken then { state with Dir = state.NextDir; Status = ___ }
        else { state with Snake = snake; Dir = state.NextDir; Apple = ___; Score = ___ }
```

</details>

## Check your understanding

1. `forAll` returns a report instead of throwing an exception. Name two things you can do with a report that you could not do if the test runner printed "FAILED" and exited.
2. A colleague's random test fails once a week on the build server and never on their laptop. Which hidden inputs would you look for? Why can that not happen to `forAll(genActions(40), prop, 300, 2024)`?
3. Write `listOf` for `IO` instead of `Random` (on paper): `replicate(io, n) : IO<A[]>`. Which lines change? What does that tell you about `flatMap` and `pure`?
4. Predict, without running anything: `minimize([1, 2, 3, 4], xs => xs.length >= 2)` and `minimize([1, 2, 3], xs => xs.length === 1 || xs.length === 3)`. Which of the two results is the smallest failing list that exists?
5. The replay law `replay(s, a ++ b) == replay(replay(s, a), b)` holds for every `update` function. Explain why, and then decide for each of these whether a *broken game* could fail it: (a) `history(s, as)` ends with `replay(s, as)`; (b) `update(s, Tick)` never changes `width` or `height`; (c) the score never goes down; (d) `update(update(s, TogglePause), TogglePause) == s` for every state `s`. Is (d) even true?
6. The wrong collision check of Puzzle 1 (Module 3), "the new head must not be on the *old* snake", keeps every invariant of this module, and Exercise 12.7 catches it by comparison with `advanceSpec`. Explain why no invariant of a *single* state can catch it. Then design the other kind of property the original version of this question suggested: a sequence of actions from a hand-built start state on a small board that must be survivable. Which of the two would still find the bug if `advanceSpec` had been written with the same mistake?
7. Random play from `newGame` almost never reaches score 3. Describe two different ways to get test games that do: one that changes the *generator*, one that changes the *start state*. Which did the tests of this module choose, and why?
8. `violations` checks eight invariants at run time. Pick one of them and sketch a data model in which a state that breaks it cannot be built at all. What does your model cost in the rest of the code? (Example to start from: a snake stored as a head plus a list of *directions* cannot be disconnected.)
9. In the test `the quick double turn bug is found and shrunk to its two key presses`, the first key is `Up` or `Down` and the second is `Left`. Why can the shrunk list not contain a `Tick`? And why is the second key never `Right`?
10. Trace the counterexample of `a Tick that forgets the queued turn is caught by queued-not-reversed and shrunk to four actions` (`Turn Up`, `Turn Right`, `Tick`, `Turn Left`) state by state: `dir`, `nextDir`, `queued` after each action. Which invariant breaks, and after which action? What would the snake have done on the next step?
11. `genState` never produces a state with something queued. Extend it on paper so that it also produces states with a queued turn that the real game could reach. Which constraint must the queued direction satisfy, and which further constraint links it to `dir`?
12. With `maxLen = 25` on a 5 x 5 board, is the snake from `genSnake` always 25 cells long? Why not? Does the answer matter for the comparison test of Exercise 12.7?
13. Why does the comparison test run on generated states rather than on the states of random games from `newGame`? Estimate roughly how often a random game of 40 actions brings the head next to its own tail with `nextDir` pointing at it.

## In production

- **QuickCheck** (Haskell, 1999) is where this style of testing comes from; its generators are a monad over a splittable random seed, as ours are over a seed. Every mainstream language now has a descendant: [fast-check](https://fast-check.dev/) for JavaScript and TypeScript, [ScalaCheck](https://scalacheck.org/) for Scala, [FsCheck](https://fscheck.github.io/FsCheck/) for F# and C#, [Hypothesis](https://hypothesis.readthedocs.io/) for Python.
- **Shrinking** in those libraries is more refined than `minimize`: they also make numbers smaller and strings shorter, and newer designs such as [Hedgehog](https://hedgehog.qa/) and Hypothesis shrink the *random choices* instead of the generated value, so that a shrunk value is always one the generator could have produced.
- **Mutation testing** tools such as [Stryker](https://stryker-mutator.io/) (JavaScript, C#, Scala) change your code automatically, one operator at a time, and report the changes that no test notices. (This course's own test suite was checked that way; the surviving mutants became new fixture cases, for example the Pong cases `ball-in-column-zero-is-still-in-play` and `player-paddle-catches-the-ball-at-its-first-row`.)
- **Deterministic simulation testing** takes "same seed, same run" to the scale of a distributed database: the whole cluster, with its network and disks, runs inside one deterministic simulation driven by a seed, so that a failure found after millions of simulated hours can be replayed exactly. FoundationDB was built this way ([Simulation and Testing](https://apple.github.io/foundationdb/testing.html)). It is the idea of Module 5, applied to a data centre.
- **Model checkers** explore *every* reachable state of a model instead of a random sample, and are the next step when "300 random games passed" is not enough ([TLA+](https://lamport.azurewebsites.net/tla/tla.html)).

## Further reading

- [Koen Claessen and John Hughes, "QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs"](https://www.cs.tufts.edu/~nr/cs257/archive/john-hughes/quick.pdf) — the original paper (ICFP 2000); sections 1–3 are readable with this course behind you, and its `Gen` is your `Random`.
- [Scott Wlaschin, "Choosing properties for property-based testing"](https://fsharpforfunandprofit.com/posts/property-based-testing-2/) — a catalogue of property shapes ("there and back again", "some things never change", "the test oracle") with pictures.
- [Andreas Zeller, "Reducing Failure-Inducing Inputs" (The Debugging Book)](https://www.debuggingbook.org/html/DeltaDebugger.html) — delta debugging, the general form of `minimize`, by its inventor.
- [fast-check documentation](https://fast-check.dev/docs/introduction/) — what a production library adds: many generators, integrated shrinking, replay of a failure from its seed.
- [Mutation testing (Wikipedia)](https://en.wikipedia.org/wiki/Mutation_testing) and [Metamorphic testing (Wikipedia)](https://en.wikipedia.org/wiki/Metamorphic_testing) — testing the tests, and testing relations between runs when no expected output is known.
- [Philip Wadler, "Theorems for free!"](https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf) — why some properties (like the replay law) hold for every function of a given type, and so cannot fail.
- [Hillel Wayne, "Learn TLA+"](https://learntla.com/) — an introduction to checking all states of a design instead of sampling them.