In Generating AX.25 code from the specification I described how the AX.25 v2.2 state-machine figures are held as data and turned into state tables in seven languages. That post ended with a caveat: tests passing doesn’t mean the tables are right.

This post is about closing that gap. The tables are now checked by two separate tools that must agree, the checks are measured for how much of the machine they actually reach, and the meaning of every box in the figures has been written down twice, by two readers who never saw each other’s work.

Two tools that must agree

The first tool is the two-station explorer in ax25sdl. It runs two copies of the generated tables against each other over a simulated channel that can drop, duplicate or reorder frames, and explores every order in which things can happen, up to a fault budget. After every step it checks a set of rules: every frame layer 3 sent is delivered exactly once and in order, the acknowledgement numbers make sense, a link that should come up does, a disconnect is always answered, and so on. When a rule breaks it prints the shortest sequence of steps that breaks it.

The second tool is TLA+ and its model checker TLC. The TLA+ model is generated from the same JSON tables the explorer runs, never hand-written, so it can’t drift from the figures. The two tools are written differently and run on different engines.

Every scenario, which we call a calibration row, runs in both, and CI fails if they disagree on the verdict, the length of the shortest counterexample or the number of distinct states. There are 188 rows. Some are clean runs that must pass. Some reproduce known figure defects and must fail in a stated way, so a fix has to flip its row to prove it. And some run against deliberately broken copies of the tables, to prove that each rule can actually catch something.

Reaching every arm

The first honest measurement was sobering: the scenarios we had reached 39 of the 279 table rows (one row per path through a figure). A defect in any of the other 240 was invisible to both tools, and an independent review showed deliberately broken rows passing both.

So the coverage work added scenarios batch by batch: orderly release, a link that gives up after N2 retries, layer 3 reconnecting, a peer that stays busy, T3 polling, UI frames, frame errors, frames injected as if from another implementation, I frames with the poll bit set, and inputs the figures say to hold until later. Each batch was written by one agent and reviewed by another, whose job was to break the tables on purpose and check that some row noticed. Several times the reviewer found a rule that was too lenient, and every such rule now has its own seeded broken row.

Today 235 of the 280 rows are reached by both tools. Each of the other 45 is listed in a file with its reason, and CI fails if a listed row starts firing or an unlisted one stops:

  • 14 can’t be reached in the specification as transcribed (for example, subroutines that no page calls);
  • 18 can’t be reached in this harness yet (for example, XID and TEST frames aren’t modelled);
  • 13 haven’t been reached yet, and say what they’d need.

Reading the spec twice

Two tools agreeing is good, but they shared one weakness. The figures say things like “Push Old I Frame onto Queue” and “Set Version 2.0”, and someone has to decide what those boxes mean. Both tools took that meaning from the same place, the reference interpreter, so a misreading of the prose would pass both.

To test that, the TLA+ model was split into two parts behind a written interface: a runner, which knows how to walk a table, and a meaning module, which says what each box and each test means. Then a second meaning module was written from scratch, by an author working in a stripped-down copy of the repository. It had the 2025, 2017 and July 1998 editions of the spec, the figures, the list of box names and the interface, and none of the interpreter, the existing meaning or the issue tracker. Every definition it wrote cites the clause it came from.

The two meanings now run side by side in TLC. At every step both are fed the same input, and the run stops at the first difference in what they send, what they tell layer 3, or the sequence numbers and flags they hold. Over the 188 rows that gave six distinct differences. A third reader then checked each one against the 2025 figure at full resolution, the 1998 edition, the transcription and the prose:

  • “Set Version 2.0/2.2” boxes are really calls to subroutines drawn with the wrong symbol, so they set the modulus and the reject mode as well. The interpreter only set a flag; that’s being fixed. The same check found that the 2025 figure sets the v2.0 window to k = 8 at modulo 8, which would stop a v2.0 link ever sending. The 1998 figure said 4 and the 2025 prose says 7 (ax25spec#54).
  • Retransmitted I frames are renumbered if you follow the figures literally, in both editions, and are blocked when the window is full, which is exactly when they’re needed. The prose is clear that they keep their original numbers, which is what the interpreter and packet.net already do (ax25spec#181).
  • A frame put back on the queue because the peer is busy has to go back at the front, or layer 3’s data gets reordered. Here the independent reader took “all queues are first-in, first-out” literally and got it wrong, but the spec never actually says it, so that’s now an editorial issue (ax25spec#182).
  • DL-FLOW-OFF and DL-FLOW-ON draw no N(r) assignment, which section 4.2.2.5 settles, and the 1998 edition shows the surrounding defect (ax25spec#43) only arrived with the 2017 redraw.
  • The other two differences were artefacts of the harness.

None of those changes what packet.net sends on air, but two of them would have caught out anyone implementing straight from the figures.

What the checks found along the way

Reaching more of the machine found more figure problems. The ones confirmed so far, each checked by a second reader against all three editions:

  • In Timer Recovery, a connect request or a frame error sends SABM but stays in Timer Recovery; the 1998 figure went to Awaiting Connection (#167).
  • A poll answered by RNR F=1 costs a retry, so a peer that stays busy gets the link dropped (#168).
  • Swapped Yes/No labels and wrong next states introduced by the 2017 redraw (#170, #175).
  • A busy station answers a polled I frame with RR instead of RNR (#178).
  • A REJ naming V(s) makes the station retransmit the whole modulus (#179).

The checks also found two slips in our own transcription, which is the point of checking it. Both are fixed (#169, #180).

A recurring lesson: when a 2017 or 2025 figure is ambiguous, look at the July 1998 edition first. Its figures are vector drawings with readable labels, and several “defects” turned out to be things the redraw lost.

Getting it

All of this is in ax25sdl. The cross-check runs on every pull request, and the side-by-side run of the two meanings runs weekly and on demand. The tables it checks are published as Packet.Ax25.Sdl 0.13.0 on NuGet and ax25sdl 0.13.0 on npm. The work is tracked in the v2.3 epic.

What isn’t done

The checks cover the Data Link machine only. The Management Data Link, Link Multiplexer, Segmenter and the two physical machines are transcribed but not yet modelled. Both tools check a bounded envelope: two stations, small windows and a small fault budget, so “no violation found” means within that envelope. And none of the new findings has yet been reproduced against a real implementation, which is the next step: checking LinBPQ, XRouter, Dire Wolf and the Linux stack against the same rows.

Transcription and modelling mistakes are mine.