Re: [PATCH v3 09/13] verification/rvgen: Delete __parse_constraint()

[Gabriele Monaco <gmonaco@redhat.com>]

On Wed, 2026-06-17 at 11:59 +0200, Nam Cao wrote:
> Gabriele Monaco <gmonaco@redhat.com> writes:
> > This function used to validate things we are no longer validating,
> > now it's
> > alright to create a model where a clock is never reset, which
> > doesn't fully
> > make sense. Should we add that check somewhere else?
> 
> Theory does not require clock reset, right?

Yeah, I don't see it explicitly mandated in the theory, but the
description (from the sources) states:

  The value of a clock thus denotes the amount of time that has been  
elapsed since its last reset

But it also says (emphasis added by me):

  Clocks /can/ be reset to zero after which they start increasing ...

Nowhere it says clocks /must/ be reset, their value simply won't make
sense (according to the definition).

Now in our implementation we may have some automatic reset when the
monitor starts (I'm planning that to avoid invalid states), which could
make explicit resets superfluous in some cases.

Let's leave that to the user for now and skip this check.

Thanks,
Gabriele

>  This is not some sort of
> hidden issue that trips up unsuspecting people. It is obvious from
> the
> model that the clock is never reset. So I think it's fine to allow
> people to do that, maybe there will be an actual useful model without
> clock reset, you never know.
> 
> The self.env_types check is enforced by the grammar. We do lose the
> self.env_types check, but that is likely redundant anyway because we
> have this:
> 
>         for transition in self.transitions:
>             [...]
>             if transition.reset:
>                 envs.append(transition.reset.env)
>                 self.env_stored.add(transition.reset.env)
> 
> so it is clear that all envs that are reset do have a storage.
> 
> That said, I am fine with keeping these sanity checks, if you are
> paranoid.
> 
> Nam