Re: [PATCH v3 12/13] verification/rvgen: Remove the old state variables
From: Gabriele Monaco <gmonaco@redhat.com>
Date: 2026-06-10 15:06:54
Also in:
lkml
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 <redacted>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
quoted hunk ↗ jump to hunk
--- 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.pyb/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 = Truediff --git a/tools/verification/rvgen/rvgen/dot2c.pyb/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.pyb/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 boolha_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(structha_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(structha_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