Thread (22 messages) 22 messages, 2 authors, 7h ago
HOTtoday
Revisions (3)
  1. v1 [diff vs current]
  2. v2 [diff vs current]
  3. v3 current

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

From: Nam Cao <hidden>
Date: 2026-06-08 08:57:30
Also in: lkml
Subsystem: runtime verification (rv), the rest · Maintainers: Steven Rostedt, Gabriele Monaco, Linus Torvalds

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>
---
 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
-- 
2.47.3
Keyboard shortcuts
hback out one level
jnext message in thread
kprevious message in thread
ldrill in
Escclose help / fold thread tree
?toggle this help