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 <[email protected]>
Reviewed-by: Gabriele Monaco <[email protected]> > --- > 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
