Re: [PATCH v3 11/13] verification/rvgen: Switch __create_matrix() to Lark

[Gabriele Monaco]

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 <namcao@xxxxxxxxxxxxx>

Reviewed-by: Gabriele Monaco <gmonaco@xxxxxxxxxx>

> ---
>  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(