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

[gmonaco@redhat.com]

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