# TLA+ model check of sleep sort

`SleepSort.tla` is a [TLA+](https://lamport.azurewebsites.net/tla/tla.html)
model of the concurrent sleep sort in [`sort/sleep.go`](../../sort/sleep.go),
checked exhaustively by the TLC model checker.

## What this does and does NOT prove

Model checking verifies a **hand-written model**, not the Go source. TLC
explores *every* reachable state of the model and confirms:

- **`OutputSorted`** (safety) — the collected output is always non-decreasing.
- **`PermutationWhenDone`** (safety) — the output is a multiset permutation of
  the input; nothing is dropped, duplicated, or invented.
- **`Terminates`** (liveness) — the collector eventually receives every value:
  no deadlock and no value left sleeping forever.

The gap you keep responsibility for: that the model faithfully abstracts
`sleep.go`. The model represents the sleeps as a discrete clock and the
unbuffered channel + `WaitGroup` as an urgent single-value rendezvous — see the
header comment in `SleepSort.tla`.

Sortedness is **not** assumed. It emerges from one rule: time cannot pass while
a fired-but-unreceived timer waits (`Tick`'s urgency guard). Delete that guard
and TLC finds an unsorted counterexample — proof the check has teeth.

## Running

Needs Java and `tla2tools.jar` (download once):

```sh
mkdir -p ~/tools/tlaplus
curl -fsSL -o ~/tools/tlaplus/tla2tools.jar \
  https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
```

Then, from the repository root:

```sh
make verify-model
```

or directly:

```sh
java -cp ~/tools/tlaplus/tla2tools.jar tlc2.TLC \
  -config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla
```

Expected output ends with:

```
Model checking completed. No error has been found.
```

## The input

`SleepSort.cfg` checks the input `<<3, 1, 4, 1, 2>>` (defined as `InputValue`
in the module, because a `.cfg` cannot hold a sequence literal). It has a
duplicate and is out of order — enough to exercise ordering, ties, and
termination. Edit `InputValue` in `SleepSort.tla` to try others; the state space
stays small because the clock never exceeds the largest input value.