Re: [PATCH v7 05/15] Documentation/rv: Add documentation about hybrid automata

[Juri Lelli <juri.lelli@redhat.com>]

On 13/03/26 14:05, gmonaco@redhat.com 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. :)