Hello, On Thu, 2026-03-12 at 11:39 +0100, Juri Lelli wrote: > Very minor nit, feel free to ignore, but ... > > The formal 7-tuple definition includes 'i' (invariant function), but > unlike other elements, 'i' isn't stored in the automaton struct - > it's implemented as generated code in ha_verify_constraint(), IIUC. > Worth a brief note clarifying this design choice so readers don't > expect to find an invariants[] member in the struct? Here or below in > the example C code section.
Thanks for the review! I haven't really thought of that. At this stage we are not mentioning any struct element (it's purely theoretical), so there shouldn't be any expectation from the reader. Later I mention "The function verify_constraint checks guards, performs resets and starts timers to validate invariants according to specification". In fact, also guards are not represented as part of 'function', I may mention after that sentence something like: "those cannot easily be represented in the automaton struct". Not sure if saying more wouldn't make it even more confusing than it already is. Thanks, Gabriele
