Re: [PATCH v3 12/13] verification/rvgen: Remove the old state variables

[Gabriele Monaco <gmonaco@redhat.com>]

On Mon, 2026-06-08 at 10:57 +0200, Nam Cao wrote:
> The state variables (states, initial_state, final_states) only
> capture the
> states' names and have less information than their Lark-based
> counterparts.
> 
> Switch to use the new state variables and delete these old ones.
> 
> Signed-off-by: Nam Cao <namcao@linutronix.de>

Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>

> ---
>  tools/verification/rvgen/rvgen/automata.py |  9 ++++-----
>  tools/verification/rvgen/rvgen/dot2c.py    | 10 +++++-----
>  tools/verification/rvgen/rvgen/dot2k.py    |  8 ++++----
>  3 files changed, 13 insertions(+), 14 deletions(-)
> 
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 4c302f5cba68..a3be327c2a73 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -411,8 +411,7 @@ class Automata:
>          self.__dot_lines = self.__open_dot()
>          self.__parse_tree = ParseTree(file_path)
>          self.transitions = self.__parse_transitions()
> -        self._states, self._initial_state, self._final_states =
> self.__parse_states()
> -        self.states, self.initial_state, self.final_states =
> self.__get_state_variables()
> +        self.states, self.initial_state, self.final_states =
> self.__parse_states()
>          self.env_types = {}
>          self.env_stored = set()
>          self.constraint_vars = set()
> @@ -603,7 +602,7 @@ class Automata:
>                      envs.append(c.env)
>                      self.__extract_env_var(c)
>  
> -        for state in self._states:
> +        for state in self.states:
>              if state.inv:
>                  envs.append(state.inv.env)
>                  self.__extract_env_var(state.inv)
> @@ -639,7 +638,7 @@ class Automata:
>      def __create_matrix(self) -> list[list[str]]:
>          # transform the array into a dictionary
>          events = self.events
> -        states = [s.name for s in self._states]
> +        states = [s.name for s in self.states]
>          events_dict = {}
>          states_dict = {}
>          nr_event = 0
> @@ -675,7 +674,7 @@ class Automata:
>              for j in range(len(self.states)):
>                  if self.function[j][i] != self.invalid_state_str:
>                      curr_event_used += 1
> -                if self.function[j][i] == self.initial_state:
> +                if self.function[j][i] == self.initial_state.name:
>                      curr_event_will_init += 1
>              if self.function[0][i] != self.invalid_state_str:
>                  curr_event_from_init = True
> diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> b/tools/verification/rvgen/rvgen/dot2c.py
> index fc85ba1f649e..22938ce1bf6c 100644
> --- a/tools/verification/rvgen/rvgen/dot2c.py
> +++ b/tools/verification/rvgen/rvgen/dot2c.py
> @@ -29,10 +29,10 @@ class Dot2c(Automata):
>  
>      def __get_enum_states_content(self) -> list[str]:
>          buff = []
> -        buff.append(f"\t{self.initial_state}{self.enum_suffix},")
> +       
> buff.append(f"\t{self.initial_state.name}{self.enum_suffix},")
>          for state in self.states:
>              if state != self.initial_state:
> -                buff.append(f"\t{state}{self.enum_suffix},")
> +                buff.append(f"\t{state.name}{self.enum_suffix},")
>          buff.append(f"\tstate_max{self.enum_suffix},")
>  
>          return buff
> @@ -142,7 +142,7 @@ class Dot2c(Automata):
>      def format_aut_init_states_string(self) -> list[str]:
>          buff = []
>          buff.append("\t.state_names = {")
> -       
> buff.append(self.__get_string_vector_per_line_content(self.states))
> +       
> buff.append(self.__get_string_vector_per_line_content([s.name for s
> in self.states]))
>          buff.append("\t},")
>  
>          return buff
> @@ -159,7 +159,7 @@ class Dot2c(Automata):
>          return buff
>  
>      def __get_max_strlen_of_states(self) -> int:
> -        max_state_name = len(max(self.states, key=len))
> +        max_state_name = max((len(s.name) for s in self.states))
>          return max(max_state_name, len(self.invalid_state_str))
>  
>      def get_aut_init_function(self) -> str:
> @@ -199,7 +199,7 @@ class Dot2c(Automata):
>          return buff
>  
>      def get_aut_init_initial_state(self) -> str:
> -        return self.initial_state
> +        return self.initial_state.name
>  
>      def format_aut_init_initial_state(self) -> list[str]:
>          buff = []
> diff --git a/tools/verification/rvgen/rvgen/dot2k.py
> b/tools/verification/rvgen/rvgen/dot2k.py
> index dc6d6f33729b..e4b6c7c09170 100644
> --- a/tools/verification/rvgen/rvgen/dot2k.py
> +++ b/tools/verification/rvgen/rvgen/dot2k.py
> @@ -179,7 +179,7 @@ class ha2k(dot2k):
>          self.trace_h = self._read_template_file("trace_hybrid.h")
>          self.has_invariant = False
>          self.has_guard = False
> -        for state in self._states:
> +        for state in self.states:
>              if state.inv:
>                  self.has_invariant = True
>          for transition in self.transitions:
> @@ -314,7 +314,7 @@ f"""static inline bool
> ha_verify_invariants(struct ha_monitor *ha_mon,
>  {{"""]
>  
>          _else = ""
> -        for state in self._states:
> +        for state in self.states:
>              if not state.inv:
>                  continue
>  
> @@ -382,7 +382,7 @@ f"""static inline void ha_setup_invariants(struct
> ha_monitor *ha_mon,
>          buff.append(f"\tif ({condition_str})\n\t\treturn;")
>  
>          _else = ""
> -        for state in self._states:
> +        for state in self.states:
>              inv = state.inv
>              if not inv:
>                  continue
> @@ -391,7 +391,7 @@ f"""static inline void ha_setup_invariants(struct
> ha_monitor *ha_mon,
>              buff.append(f"\t\t{inv};")
>              _else = "else "
>  
> -        for state in self._states:
> +        for state in self.states:
>              inv = state.inv
>              if not inv:
>                  continue