Re: [RFC PATCH 10/17] verification/rvgen: Add support for Hybrid Automata

[Gabriele Monaco <gmonaco@redhat.com>]

On Mon, 2025-08-25 at 12:06 +0200, Nam Cao wrote:
> On Thu, Aug 14, 2025 at 05:08:02PM +0200, Gabriele Monaco wrote:
> > +    def fill_constr_func(self) -> list[str]:
> > +        buff = []
> > +        if self.constraints:
> > +            buff.append(
> > +"""/*
> > + * This function is used to validate state transitions.
> > + *
> > + * It is generated by parsing the model, there is usually no need
> > to change it,
> > + * unless conditions were incorrectly specified
> 
> If the conditions were incorrectly specified, then they should be
> fixed in the automaton, not fixed in this generated C code.

You're right, I should reword or remove that.

> > or too complex for the parser.
> 
> Do you have examples of these "too complex" cases? Is there a plan to
> handle them?

I wrote this before having the function/macro types, now everything
coming to my mind is covered. Anyway the parser is trying to be smart
but may not catch absolutely everything the user wants to specify.

Now the best thing to do would probably be to strictly define a grammar
and not support what isn't included in there, rather than telling the
user they can kind of tweak the function..

Good points, thanks!
Gabriele