Tla

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. ...