Nine state machines of increasing difficulty, each posed as the same problem: reconstruct a view from a log. Every machine is a source-derivation-view instance (see =spec.org=) - the source is an append-only event log, the derivation is a pure fold, and the view is a projection. Your job is to implement the fold and reproduce the challenge’s byte-exact oracle. The ladder climbs from a linear chain (trivial as an event stream) to a replicated state machine (Raft), which is the pattern made fault-tolerant and the reason all of these are the same problem: a state machine is a deterministic function of its log.
| # | challenge | structure S | difficulty | source | status |
|---|---|---|---|---|---|
| 1 | order-lifecycle | chain (total order) | 1 | reference | solved |
| 2 | traffic-light | 3-cycle | 2 | classic / TLA+ | solved |
| 3 | elevator | product + request set | 4 | classic | solved |
| 4 | lamp-two-switch | reversible graph ({0,1}^2) | 3 | learntla | solved |
| 5 | login-hierarchy | containment poset (tree) | 4 | learntla | solved |
| 6 | dfa-even-01 | complete DFA (cyclic) | 5 | Hopcroft | solved |
| 7 | lr-parser-fsm | LR automaton + stack | 6 | Graphviz gallery | solved |
| 8 | register-machine | controller + datapath | 7 | SICP §5.1 | solved |
| 9 | raft-replicated-sm | replicated log -> apply | 8 | Raft / C. Troy | solved |
The structure column is the point: a chain has a sound wide-flag projection (down-sets); a cycle or reversible graph does not - there the view must be the current state plus a transition-legality check; a poset (the login tree) restores down-sets in general form; a DFA collapses the view to accept/reject; an LR automaton and a register machine need a stack; Raft replicates the whole thing. Choosing the right projection is half of each challenge.
bin/verify.sh # run every challenge that has a reference
bin/verify.sh challenges/01-order-lifecycle
cat challenges/02-traffic-light/README.org # read a challenge's spec
bin/new-exercise -d /tmp/scratch -n mine ... # stamp a fresh skeleton (see spec §12)Each challenge is challenges/NN-<name>/. A solved one ships fixtures under
data/, a reference under examples/<tag>-<lang>/ whose run.sh prints the
oracle, and examples/oracle-contract.txt; bin/verify.sh diffs them. An open
one ships the spec (states, transitions, structure, what to implement, how it is
judged) - build the fixtures + reference per spec.org §8 and pin the oracle.
| path | what |
|---|---|
challenges/NN-<name>/ | one state machine, easy -> hard |
spec.org | the generator: the source-derivation-view pattern |
.meta/ | operating disciplines and vocabulary |
bin/verify.sh | ladder runner (PASS / FAIL / OPEN per challenge) |
bin/new-exercise | stamp a new challenge skeleton from the §2 parameters |