Re: [PATCH v7 05/15] Documentation/rv: Add documentation about hybrid automata
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. :)
Re: [PATCH v7 05/15] Documentation/rv: Add documentation about hybrid automata
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
Re: [PATCH v7 05/15] Documentation/rv: Add documentation about hybrid automata
Hello,
On 10/03/26 11:56, Gabriele Monaco wrote:
...
> diff --git a/Documentation/trace/rv/hybrid_automata.rst
> b/Documentation/trace/rv/hybrid_automata.rst
> new file mode 100644
> index ..60f6bccfba38
> --- /dev/null
> +++ b/Documentation/trace/rv/hybrid_automata.rst
> @@ -0,0 +1,341 @@
> +Hybrid Automata
> +===
> +
> +Hybrid automata are an extension of deterministic automata, there are several
> +definitions of hybrid automata in the literature. The adaptation implemented
> +here is formally denoted by G and defined as a 7-tuple:
> +
> +*G* = { *X*, *E*, *V*, *f*, x\ :subscript:`0`, X\ :subscript:`m`,
> *i* }
> +
> +- *X* is the set of states;
> +- *E* is the finite set of events;
> +- *V* is the finite set of environment variables;
> +- x\ :subscript:`0` is the initial state;
> +- X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states.
> +- *f* : *X* x *E* x *C(V)* -> *X* is the transition function.
> + It defines the state transition in the occurrence of an event from *E* in
> the
> + state *X*. Unlike deterministic automata, the transition function also
> + includes guards from the set of all possible constraints (defined as
> *C(V)*).
> + Guards can be true or false with the valuation of *V* when the event
> occurs,
> + and the transition is possible only when constraints are true. Similarly to
> + deterministic automata, the occurrence of the event in *E* in a state in
> *X*
> + has a deterministic next state from *X*, if the guard is true.
> +- *i* : *X* -> *C'(V)* is the invariant assignment function, this is a
> + constraint assigned to each state in *X*, every state in *X* must be left
> + before the invariant turns to false. We can omit the representation of
> + invariants whose value is true regardless of the valuation of *V*.
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.
In any case,
Reviewed-by: Juri Lelli
Thanks,
Juri
