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 000000000000..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 <[email protected]>
Thanks,
Juri
