On Mon, 2026-06-08 at 10:57 +0200, Nam Cao wrote: > Hybrid automata monitors's clock variables have been changed to have > only a single representation. Now there is no need to generate code > to convert between the two representations. > > Delete __fill_convert_inv_guard_func() and its associates. Update > __start_to_invariant_check() to how invariants now work. > > Signed-off-by: Nam Cao <[email protected]>
Reviewed-by: Gabriele Monaco <[email protected]> > --- > tools/verification/rvgen/rvgen/dot2k.py | 96 +---------------------- > -- > 1 file changed, 3 insertions(+), 93 deletions(-) > > diff --git a/tools/verification/rvgen/rvgen/dot2k.py > b/tools/verification/rvgen/rvgen/dot2k.py > index e91717fde30d..6d346a718a39 100644 > --- a/tools/verification/rvgen/rvgen/dot2k.py > +++ b/tools/verification/rvgen/rvgen/dot2k.py > @@ -246,7 +246,9 @@ class ha2k(dot2k): > if inv.unit == "j": > clock_type = "jiffy" > > - return f"return ha_check_invariant_{clock_type}(ha_mon, > {inv.env}_{self.name}, time_ns)" > + value = self.__adjust_value(inv.val, inv.unit) > + > + return f"return ha_check_invariant_{clock_type}(ha_mon, > {inv.env}_{self.name}, time_ns, {value})" > > def __start_to_conv(self, constr: str) -> str: > """ > @@ -383,40 +385,6 @@ f"""static inline bool > ha_verify_invariants(struct ha_monitor *ha_mon, > buff.append("\treturn true;\n}\n") > return buff > > - def __fill_convert_inv_guard_func(self) -> list[str]: > - buff = [] > - if not self.invariants: > - return [] > - > - conflict_guards, conflict_invs = self.__find_inv_conflicts() > - if not conflict_guards and not conflict_invs: > - return [] > - > - buff.append( > -f"""static inline void ha_convert_inv_guard(struct ha_monitor > *ha_mon, > -\t\t\t\t\tenum {self.enum_states_def} curr_state, enum > {self.enum_events_def} event, > -\t\t\t\t\tenum {self.enum_states_def} next_state, u64 time_ns) > -{{""") > - buff.append("\tif (curr_state == next_state)\n\t\treturn;") > - > - _else = "" > - for state, constr in sorted(self.invariants.items()): > - # a state with invariant can reach us without reset > - # multiple conflicts must have the same invariant, > otherwise we cannot > - # know how to reset the value > - conf_i = [start for start, end in conflict_invs if end > == state] > - # we can reach a guard without reset > - conf_g = [e for s, e in conflict_guards if s == state] > - if not conf_i and not conf_g: > - continue > - buff.append(f"\t{_else}if (curr_state == > {self.states[state]}{self.enum_suffix})") > - > - buff.append(f"\t\t{self.__start_to_conv(constr)};") > - _else = "else " > - > - buff.append("}\n") > - return buff > - > def __fill_verify_guards_func(self) -> list[str]: > buff = [] > > @@ -456,54 +424,6 @@ f"""static inline bool ha_verify_guards(struct > ha_monitor *ha_mon, > buff.append("\treturn res;\n}\n") > return buff > > - def __find_inv_conflicts(self) -> tuple[set[tuple[int, > _EventConstraintKey]], > - set[tuple[int, > _StateConstraintKey]]]: > - """ > - Run a breadth first search from all states with an > invariant. > - Find any conflicting constraints reachable from there, this > can be > - another state with an invariant or an edge with a non-reset > guard. > - Stop when we find a reset. > - > - Return the set of conflicting guards and invariants as > tuples of > - conflicting state and constraint key. > - """ > - conflict_guards: set[tuple[int, _EventConstraintKey]] = > set() > - conflict_invs: set[tuple[int, _StateConstraintKey]] = set() > - for start_idx in self.invariants: > - queue = deque([(start_idx, 0)]) # (state_idx, distance) > - env = > self.__get_constraint_env(self.invariants[start_idx]) > - > - while queue: > - curr_idx, distance = queue.popleft() > - > - # Check state condition > - if curr_idx != start_idx and curr_idx in > self.invariants: > - conflict_invs.add((start_idx, > _StateConstraintKey(curr_idx))) > - continue > - > - # Check if we should stop > - if distance > len(self.states): > - break > - if curr_idx != start_idx and distance > 1: > - continue > - > - for event_idx, next_state_name in > enumerate(self.function[curr_idx]): > - if next_state_name == self.invalid_state_str: > - continue > - curr_guard = self.guards.get((curr_idx, > event_idx), "") > - if "reset" in curr_guard and env in curr_guard: > - continue > - > - if env in curr_guard: > - conflict_guards.add((start_idx, > - > _EventConstraintKey(curr_idx, event_idx))) > - continue > - > - next_idx = self.states.index(next_state_name) > - queue.append((next_idx, distance + 1)) > - > - return conflict_guards, conflict_invs > - > def __fill_setup_invariants_func(self) -> list[str]: > if not self.has_invariant: > return [] > @@ -554,16 +474,9 @@ f"""static inline void > ha_setup_invariants(struct ha_monitor *ha_mon, > * the next state has a constraint, cancel it in any other case and > to check > * that it didn't expire before the callback run. Transitions to the > same state > * without a reset never affect timers. > - * Due to the different representations between invariants and > guards, there is > - * a function to convert it in case invariants or guards are > reachable from > - * another invariant without reset. Those are not present if not > required in > - * the model. This is all automatic but is worth checking because it > may show > - * errors in the model (e.g. missing resets). > */""") > > buff += self.__fill_verify_invariants_func() > - inv_conflicts = self.__fill_convert_inv_guard_func() > - buff += inv_conflicts > buff += self.__fill_verify_guards_func() > buff += self.__fill_setup_invariants_func() > > @@ -576,9 +489,6 @@ f"""static bool ha_verify_constraint(struct > ha_monitor *ha_mon, > if self.invariants: > buff.append("\tif (!ha_verify_invariants(ha_mon, > curr_state, " > "event, next_state, time_ns))\n\t\treturn > false;\n") > - if inv_conflicts: > - buff.append("\tha_convert_inv_guard(ha_mon, curr_state, > event, " > - "next_state, time_ns);\n") > > if self.guards: > buff.append("\tif (!ha_verify_guards(ha_mon, curr_state, > event, "
