On 13/03/26 14:05, [email protected] wrote: > 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.
Yeah, probably. As mentioned, feel free to ignore, it was just a thought. :)
