On Mon, 2026-06-08 at 10:57 +0200, Nam Cao wrote: > Switch __create_matrix() to use the transitions parsed by Lark to > avoid all > the raw text parsing. > > Also stop parsing constraints in __create_matrix(), that is not used > anymore. > > Signed-off-by: Nam Cao <[email protected]>
Reviewed-by: Gabriele Monaco <[email protected]> > --- > tools/verification/rvgen/rvgen/automata.py | 47 ++++++-------------- > -- > tools/verification/rvgen/rvgen/dot2k.py | 2 +- > 2 files changed, 13 insertions(+), 36 deletions(-) > > diff --git a/tools/verification/rvgen/rvgen/automata.py > b/tools/verification/rvgen/rvgen/automata.py > index 2e26bb863245..4c302f5cba68 100644 > --- a/tools/verification/rvgen/rvgen/automata.py > +++ b/tools/verification/rvgen/rvgen/automata.py > @@ -418,7 +418,7 @@ class Automata: > self.constraint_vars = set() > self.self_loop_reset_events = set() > self.events, self.envs = self.__get_event_variables() > - self.function, self.constraints = self.__create_matrix() > + self.function = self.__create_matrix() > self.events_start, self.events_start_run = > self.__store_init_events() > self.env_stored = sorted(self.env_stored) > self.constraint_vars = sorted(self.constraint_vars) > @@ -636,10 +636,10 @@ class Automata: > if constraint.val[0].isalpha(): > self.constraint_vars.add(constraint.val) > > - def __create_matrix(self) -> tuple[list[list[str]], > dict[_ConstraintKey, list[str]]]: > + def __create_matrix(self) -> list[list[str]]: > # transform the array into a dictionary > events = self.events > - states = self.states > + states = [s.name for s in self._states] > events_dict = {} > states_dict = {} > nr_event = 0 > @@ -654,39 +654,16 @@ class Automata: > > # declare the matrix.... > matrix = [[self.invalid_state_str for _ in range(nr_event)] > for _ in range(nr_state)] > - constraints: dict[_ConstraintKey, list[str]] = {} > > - # and we are back! Let's fill the matrix > - cursor = self.__get_cursor_begin_events() > - > - for line in map(str.lstrip, > - islice(self.__dot_lines, cursor, None)): > - > - if not line or line[0] != '"': > - break > - > - split_line = line.split() > - > - if len(split_line) > 2 and split_line[1] == "->": > - origin_state = split_line[0].replace('"', > '').replace(',', '_') > - dest_state = split_line[2].replace('"', > '').replace(',', '_') > - possible_events = > "".join(split_line[split_line.index("label") + 2:-1]).replace('"', > '') > - for event in possible_events.split("\\n"): > - event, *constr = event.split(";") > - if constr: > - key = > _EventConstraintKey(states_dict[origin_state], events_dict[event]) > - constraints[key] = constr > - # those events reset also on self loops > - if origin_state == dest_state and "reset" in > "".join(constr): > - self.self_loop_reset_events.add(event) > - > matrix[states_dict[origin_state]][events_dict[event]] = dest_state > - else: > - state = line.split("label")[1].split('"')[1] > - state, *constr = state.replace(" ", "").split("\\n") > - if constr: > - > constraints[_StateConstraintKey(states_dict[state])] = constr > - > - return matrix, constraints > + for transition in self.transitions: > + src, dst = transition.src, transition.dst > + event = transition.event > + if src == dst and transition.reset: > + # those events reset also on self loops > + self.self_loop_reset_events.add(event) > + matrix[states_dict[src]][events_dict[event]] = dst > + > + return matrix > > def __store_init_events(self) -> tuple[list[bool], list[bool]]: > events_start = [False] * len(self.events) > diff --git a/tools/verification/rvgen/rvgen/dot2k.py > b/tools/verification/rvgen/rvgen/dot2k.py > index a38ef735a861..dc6d6f33729b 100644 > --- a/tools/verification/rvgen/rvgen/dot2k.py > +++ b/tools/verification/rvgen/rvgen/dot2k.py > @@ -403,7 +403,7 @@ f"""static inline void ha_setup_invariants(struct > ha_monitor *ha_mon, > > def __fill_constr_func(self) -> list[str]: > buff = [] > - if not self.constraints: > + if not self.has_invariant and not self.has_guard: > return [] > > buff.append(
