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

[Gabriele Monaco]

On Mon, 2026-06-08 at 10:57 +0200, Nam Cao wrote:
> -    def __validate_constraint(self, key: tuple[int, int] | int,
> constr: str,
> -                              rule, reset) -> None:
> -        # event constrains are tuples and allow both rules and reset
> -        # state constraints are only used for expirations (e.g.
> clk<N)
> -        if self.is_event_constraint(key):
> -            if not rule and not reset:
> -                raise AutomataError("Unrecognised event constraint "
> -                                   
> f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
> -            if rule and (rule["env"] in self.env_types and
> -                         rule["env"] not in self.env_stored):
> -                raise AutomataError("Clocks in hybrid automata
> always require a storage"
> -                                    f" ({rule["env"]})")
> -        else:
> -            if not rule:
> -                raise AutomataError("Unrecognised state constraint "
> -                                    f"({self.states[key]}:
> {constr})")
> -            if rule["env"] not in self.env_stored:
> -                raise AutomataError("State constraints always
> require a storage "
> -                                    f"({rule["env"]})")

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?

Thanks,
Gabriele

> -            if rule["op"] not in ["<", "<="]:
> -                raise AutomataError("State constraints must be clock
> expirations like"
> -                                    f" clk<N ({rule.string})")
> -