[PATCH v3 00/19] rv/rvgen: Robustness, modernization, and fixes

[PATCH v3 00/19] rv/rvgen: Robustness, modernization, and fixes

[Wander Lairson Costa]

This patch series introduces fixes and improvements to the RV Generator
(rvgen) tool in tools/verification. The primary goal is to enhance the
tool's robustness, maintainability, and correctness by addressing
several latent bugs, modernizing the Python codebase, and improving its
overall structure and error handling.

The changes include fixing logic errors in DOT file validation,
resolving unbound variable errors that could lead to runtime crashes,
and improving exception handling by removing dangerous bare except
clauses. The codebase is updated to use contemporary Python idioms such
as f-strings and context managers. Additionally, type annotations are
added to resolve static analysis errors.

Changes in v3:
- Dropped patch "add missing return type annotations" as per Gabriele
  Monaco's feedback that annotations on stub methods are not needed at
  this stage.
- Expanded AutomataError exception class patch to also replace generic
  ValueError exceptions in HA and LTL modules, as suggested by Gabriele
  Monaco.
- Updated typo fix patch to also correct singular/plural inconsistencies
  ("automata" to "automaton"), as noted by Gabriele Monaco.
- Included additional f-string conversion in dot2k.py found by Gabriele
  Monaco after rebase.

Changes in v2:
- Dropped patches related to the @not_implemented decorator and abstract
  method stubs (v1 patches 9, 18, 19) to address class hierarchy
  improvements in a separate series.
- Dropped trivial cleanup patches (boolean simplification, __contains__)
  as they were already fixed after rebasing from
  linux-trace/latency/for-next.
- Merged typo fix patches into a single patch.
- Changed the fix for the unbound loop variable warning in abbreviate_atoms
  pyright report.
- Reworked initial state validation to strictly enforce the presence of
  an initial state.

Wander Lairson Costa (19):
  rv/rvgen: introduce AutomataError exception class
  rv/rvgen: remove bare except clauses in generator
  rv/rvgen: replace % string formatting with f-strings
  rv/rvgen: replace __len__() calls with len()
  rv/rvgen: remove unnecessary semicolons
  rv/rvgen: use context managers for file operations
  rv/rvgen: fix typos in automata and generator docstring and comments
  rv/rvgen: fix PEP 8 whitespace violations
  rv/rvgen: fix DOT file validation logic error
  rv/rvgen: use class constant for init marker
  rv/rvgen: refactor automata.py to use iterator-based parsing
  rv/rvgen: remove unused sys import from dot2c
  rv/rvgen: remove unused __get_main_name method
  rv/rvgen: make monitor arguments required in rvgen
  rv/rvgen: fix isinstance check in Variable.expand()
  rv/rvgen: extract node marker string to class constant
  rv/rvgen: enforce presence of initial state
  rv/rvgen: fix unbound loop variable warning
  rv/rvgen: fix _fill_states() return type annotation

 tools/verification/rvgen/__main__.py        |  19 +--
 tools/verification/rvgen/dot2c              |   1 -
 tools/verification/rvgen/rvgen/automata.py  | 155 ++++++++++++--------
 tools/verification/rvgen/rvgen/dot2c.py     |  58 ++++----
 tools/verification/rvgen/rvgen/dot2k.py     |  61 ++++----
 tools/verification/rvgen/rvgen/generator.py |  91 +++++-------
 tools/verification/rvgen/rvgen/ltl2ba.py    |  11 +-
 tools/verification/rvgen/rvgen/ltl2k.py     |  54 ++++---
 8 files changed, 237 insertions(+), 213 deletions(-)

-- 
2.53.0

[PATCH v3 01/19] rv/rvgen: introduce AutomataError exception class

[Wander Lairson Costa]

Replace the generic except Exception block with a custom AutomataError
class that inherits from Exception. This provides more precise exception
handling for automata parsing and validation errors while avoiding
overly broad exception catches that could mask programming errors like
SyntaxError or TypeError.

The AutomataError class is raised when DOT file processing fails due to
invalid format, I/O errors, or malformed automaton definitions. The
main entry point catches this specific exception and provides a
user-friendly error message to stderr before exiting.

Also, replace generic exceptions raising in HA and LTL with
AutomataError.

Co-authored-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
 tools/verification/rvgen/__main__.py        |  6 ++---
 tools/verification/rvgen/rvgen/automata.py  | 17 ++++++++++----
 tools/verification/rvgen/rvgen/dot2c.py     |  4 ++--
 tools/verification/rvgen/rvgen/dot2k.py     | 26 ++++++++++-----------
 tools/verification/rvgen/rvgen/generator.py |  7 ++----
 tools/verification/rvgen/rvgen/ltl2ba.py    |  9 +++----
 tools/verification/rvgen/rvgen/ltl2k.py     |  8 +++++--
 7 files changed, 43 insertions(+), 34 deletions(-)

diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 9a5a9f08eae21..5a3f090ac3316 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -13,6 +13,7 @@ if __name__ == '__main__':
     from rvgen.generator import Monitor
     from rvgen.container import Container
     from rvgen.ltl2k import ltl2k
+    from rvgen.automata import AutomataError
     import argparse
     import sys
 
@@ -55,9 +56,8 @@ if __name__ == '__main__':
                 sys.exit(1)
         else:
             monitor = Container(vars(params))
-    except Exception as e:
-        print('Error: '+ str(e))
-        print("Sorry : :-(")
+    except AutomataError as e:
+        print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
         sys.exit(1)
 
     print("Writing the monitor into the directory %s" % monitor.name)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 5c1c5597d839f..9cc452305a2aa 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -25,6 +25,13 @@ class _EventConstraintKey(_ConstraintKey, tuple):
     def __new__(cls, state_id: int, event_id: int):
         return super().__new__(cls, (state_id, event_id))
 
+class AutomataError(Exception):
+    """Exception raised for errors in automata parsing and validation.
+
+    Raised when DOT file processing fails due to invalid format, I/O errors,
+    or malformed automaton definitions.
+    """
+
 class Automata:
     """Automata class: Reads a dot file and part it as an automata.
 
@@ -72,11 +79,11 @@ class Automata:
         basename = ntpath.basename(self.__dot_path)
         if not basename.endswith(".dot") and not basename.endswith(".gv"):
             print("not a dot file")
-            raise Exception("not a dot file: %s" % self.__dot_path)
+            raise AutomataError("not a dot file: %s" % self.__dot_path)
 
         model_name = ntpath.splitext(basename)[0]
         if model_name.__len__() == 0:
-            raise Exception("not a dot file: %s" % self.__dot_path)
+            raise AutomataError("not a dot file: %s" % self.__dot_path)
 
         return model_name
 
@@ -85,8 +92,8 @@ class Automata:
         dot_lines = []
         try:
             dot_file = open(self.__dot_path)
-        except:
-            raise Exception("Cannot open the file: %s" % self.__dot_path)
+        except OSError as exc:
+            raise AutomataError(exc.strerror) from exc
 
         dot_lines = dot_file.read().splitlines()
         dot_file.close()
@@ -95,7 +102,7 @@ class Automata:
         line = dot_lines[cursor].split()
 
         if (line[0] != "digraph") and (line[1] != "state_automaton"):
-            raise Exception("Not a valid .dot format: %s" % self.__dot_path)
+            raise AutomataError("Not a valid .dot format: %s" % self.__dot_path)
         else:
             cursor += 1
         return dot_lines
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index f779d9528af3f..6878cc79e6f70 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -13,7 +13,7 @@
 # For further information, see:
 #   Documentation/trace/rv/deterministic_automata.rst
 
-from .automata import Automata
+from .automata import Automata, AutomataError
 
 class Dot2c(Automata):
     enum_suffix = ""
@@ -103,7 +103,7 @@ class Dot2c(Automata):
             min_type = "unsigned int"
 
         if self.states.__len__() > 1000000:
-            raise Exception("Too many states: %d" % self.states.__len__())
+            raise AutomataError("Too many states: %d" % self.states.__len__())
 
         return min_type
 
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e7ba68a54c1f8..55222e38323f5 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -11,7 +11,7 @@
 from collections import deque
 from .dot2c import Dot2c
 from .generator import Monitor
-from .automata import _EventConstraintKey, _StateConstraintKey
+from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
 
 
 class dot2k(Monitor, Dot2c):
@@ -166,14 +166,14 @@ class da2k(dot2k):
     def __init__(self, *args, **kwargs):
         super().__init__(*args, **kwargs)
         if self.is_hybrid_automata():
-            raise ValueError("Detected hybrid automata, use the 'ha' class")
+            raise AutomataError("Detected hybrid automata, use the 'ha' class")
 
 class ha2k(dot2k):
     """Hybrid automata only"""
     def __init__(self, *args, **kwargs):
         super().__init__(*args, **kwargs)
         if not self.is_hybrid_automata():
-            raise ValueError("Detected deterministic automata, use the 'da' class")
+            raise AutomataError("Detected deterministic automata, use the 'da' class")
         self.trace_h = self._read_template_file("trace_hybrid.h")
         self.__parse_constraints()
 
@@ -266,22 +266,22 @@ class ha2k(dot2k):
         # state constraints are only used for expirations (e.g. clk<N)
         if self.is_event_constraint(key):
             if not rule and not reset:
-                raise ValueError("Unrecognised event constraint "
-                                 f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
+                raise AutomataError("Unrecognised event constraint "
+                                    f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
             if rule and (rule["env"] in self.env_types and
                          rule["env"] not in self.env_stored):
-                raise ValueError("Clocks in hybrid automata always require a storage"
-                                 f" ({rule["env"]})")
+                raise AutomataError("Clocks in hybrid automata always require a storage"
+                                    f" ({rule["env"]})")
         else:
             if not rule:
-                raise ValueError("Unrecognised state constraint "
-                                 f"({self.states[key]}: {constr})")
+                raise AutomataError("Unrecognised state constraint "
+                                    f"({self.states[key]}: {constr})")
             if rule["env"] not in self.env_stored:
-                raise ValueError("State constraints always require a storage "
-                                 f"({rule["env"]})")
+                raise AutomataError("State constraints always require a storage "
+                                    f"({rule["env"]})")
             if rule["op"] not in ["<", "<="]:
-                raise ValueError("State constraints must be clock expirations like"
-                                 f" clk<N ({rule.string})")
+                raise AutomataError("State constraints must be clock expirations like"
+                                    f" clk<N ({rule.string})")
 
     def __parse_constraints(self) -> None:
         self.guards: dict[_EventConstraintKey, str] = {}
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 5eac12e110dce..571093a92bdc8 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -51,10 +51,7 @@ class RVGenerator:
         raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
 
     def _read_file(self, path):
-        try:
-            fd = open(path, 'r')
-        except OSError:
-            raise Exception("Cannot open the file: %s" % path)
+        fd = open(path, 'r')
 
         content = fd.read()
 
@@ -65,7 +62,7 @@ class RVGenerator:
         try:
             path = os.path.join(self.abs_template_dir, file)
             return self._read_file(path)
-        except Exception:
+        except OSError:
             # Specific template file not found. Try the generic template file in the template/
             # directory, which is one level up
             path = os.path.join(self.abs_template_dir, "..", file)
diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index f14e6760ac3db..f9855dfa3bc1c 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -9,6 +9,7 @@
 
 from ply.lex import lex
 from ply.yacc import yacc
+from .automata import AutomataError
 
 # Grammar:
 # 	ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
@@ -62,7 +63,7 @@ t_ignore_COMMENT = r'\#.*'
 t_ignore = ' \t\n'
 
 def t_error(t):
-    raise ValueError(f"Illegal character '{t.value[0]}'")
+    raise AutomataError(f"Illegal character '{t.value[0]}'")
 
 lexer = lex()
 
@@ -487,7 +488,7 @@ def p_unop(p):
     elif p[1] == "not":
         op = NotOp(p[2])
     else:
-        raise ValueError(f"Invalid unary operator {p[1]}")
+        raise AutomataError(f"Invalid unary operator {p[1]}")
 
     p[0] = ASTNode(op)
 
@@ -507,7 +508,7 @@ def p_binop(p):
     elif p[2] == "imply":
         op = ImplyOp(p[1], p[3])
     else:
-        raise ValueError(f"Invalid binary operator {p[2]}")
+        raise AutomataError(f"Invalid binary operator {p[2]}")
 
     p[0] = ASTNode(op)
 
@@ -526,7 +527,7 @@ def parse_ltl(s: str) -> ASTNode:
             subexpr[assign[0]] = assign[1]
 
     if rule is None:
-        raise ValueError("Please define your specification in the \"RULE = <LTL spec>\" format")
+        raise AutomataError("Please define your specification in the \"RULE = <LTL spec>\" format")
 
     for node in rule:
         if not isinstance(node.op, Variable):
diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index b075f98d50c47..08ad245462e7d 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -4,6 +4,7 @@
 from pathlib import Path
 from . import generator
 from . import ltl2ba
+from .automata import AutomataError
 
 COLUMN_LIMIT = 100
 
@@ -60,8 +61,11 @@ class ltl2k(generator.Monitor):
         if MonitorType != "per_task":
             raise NotImplementedError("Only per_task monitor is supported for LTL")
         super().__init__(extra_params)
-        with open(file_path) as f:
-            self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
+        try:
+            with open(file_path) as f:
+                self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
+        except OSError as exc:
+            raise AutomataError(exc.strerror) from exc
         self.atoms_abbr = abbreviate_atoms(self.atoms)
         self.name = extra_params.get("model_name")
         if not self.name:
-- 
2.53.0

[PATCH v3 02/19] rv/rvgen: remove bare except clauses in generator

[Wander Lairson Costa]

Remove bare except clauses from the generator module that were
catching all exceptions including KeyboardInterrupt and SystemExit.
This follows the same exception handling improvements made in the
previous AutomataError commit and addresses PEP 8 violations.

The bare except clause in __create_directory was silently catching
and ignoring all errors after printing a message, which could mask
serious issues. For __write_file, the bare except created a critical
bug where the file variable could remain undefined if open() failed,
causing a NameError when attempting to write to or close the file.

These methods now let OSError propagate naturally, allowing callers
to handle file system errors appropriately. This provides clearer
error reporting and allows Python's exception handling to show
complete stack traces with proper error types and locations.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/generator.py | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 571093a92bdc8..a2391a4c21ed6 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -198,17 +198,10 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
             os.mkdir(path)
         except FileExistsError:
             return
-        except:
-            print("Fail creating the output dir: %s" % self.name)
 
     def __write_file(self, file_name, content):
-        try:
-            file = open(file_name, 'w')
-        except:
-            print("Fail writing to file: %s" % file_name)
-
+        file = open(file_name, 'w')
         file.write(content)
-
         file.close()
 
     def _create_file(self, file_name, content):
-- 
2.53.0

[PATCH v3 03/19] rv/rvgen: replace % string formatting with f-strings

[Wander Lairson Costa]

Replace all instances of percent-style string formatting with
f-strings across the rvgen codebase. This modernizes the string
formatting to use Python 3.6+ features, providing clearer and more
maintainable code while improving runtime performance.

The conversion handles all formatting cases including simple variable
substitution, multi-variable formatting, and complex format specifiers.
Dynamic width formatting is converted from "%*s" to "{var:>{width}}"
using proper alignment syntax. Template strings for generated C code
properly escape braces using double-brace syntax to produce literal
braces in the output.

F-strings provide approximately 2x performance improvement over percent
formatting and are the recommended approach in modern Python.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/__main__.py        |  6 +--
 tools/verification/rvgen/rvgen/automata.py  |  6 +--
 tools/verification/rvgen/rvgen/dot2c.py     | 38 ++++++-------
 tools/verification/rvgen/rvgen/dot2k.py     | 29 +++++-----
 tools/verification/rvgen/rvgen/generator.py | 59 ++++++++++-----------
 tools/verification/rvgen/rvgen/ltl2k.py     | 30 +++++------
 6 files changed, 83 insertions(+), 85 deletions(-)

diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 5a3f090ac3316..2e5b868535470 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -44,7 +44,7 @@ if __name__ == '__main__':
 
     try:
         if params.subcmd == "monitor":
-            print("Opening and parsing the specification file %s" % params.spec)
+            print(f"Opening and parsing the specification file {params.spec}")
             if params.monitor_class == "da":
                 monitor = da2k(params.spec, params.monitor_type, vars(params))
             elif params.monitor_class == "ha":
@@ -60,11 +60,11 @@ if __name__ == '__main__':
         print(f"There was an error processing {params.spec}: {e}", file=sys.stderr)
         sys.exit(1)
 
-    print("Writing the monitor into the directory %s" % monitor.name)
+    print(f"Writing the monitor into the directory {monitor.name}")
     monitor.print_files()
     print("Almost done, checklist")
     if params.subcmd == "monitor":
-        print("  - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name))
+        print(f"  - Edit the {monitor.name}/{monitor.name}.c to add the instrumentation")
         print(monitor.fill_tracepoint_tooltip())
     print(monitor.fill_makefile_tooltip())
     print(monitor.fill_kconfig_tooltip())
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 9cc452305a2aa..4fed58cfa3c6e 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -79,11 +79,11 @@ class Automata:
         basename = ntpath.basename(self.__dot_path)
         if not basename.endswith(".dot") and not basename.endswith(".gv"):
             print("not a dot file")
-            raise AutomataError("not a dot file: %s" % self.__dot_path)
+            raise AutomataError(f"not a dot file: {self.__dot_path}")
 
         model_name = ntpath.splitext(basename)[0]
         if model_name.__len__() == 0:
-            raise AutomataError("not a dot file: %s" % self.__dot_path)
+            raise AutomataError(f"not a dot file: {self.__dot_path}")
 
         return model_name
 
@@ -102,7 +102,7 @@ class Automata:
         line = dot_lines[cursor].split()
 
         if (line[0] != "digraph") and (line[1] != "state_automaton"):
-            raise AutomataError("Not a valid .dot format: %s" % self.__dot_path)
+            raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
         else:
             cursor += 1
         return dot_lines
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index 6878cc79e6f70..e6a440e1588cd 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -29,17 +29,17 @@ class Dot2c(Automata):
 
     def __get_enum_states_content(self) -> list[str]:
         buff = []
-        buff.append("\t%s%s," % (self.initial_state, self.enum_suffix))
+        buff.append(f"\t{self.initial_state}{self.enum_suffix},")
         for state in self.states:
             if state != self.initial_state:
-                buff.append("\t%s%s," % (state, self.enum_suffix))
-        buff.append("\tstate_max%s," % (self.enum_suffix))
+                buff.append(f"\t{state}{self.enum_suffix},")
+        buff.append(f"\tstate_max{self.enum_suffix},")
 
         return buff
 
     def format_states_enum(self) -> list[str]:
         buff = []
-        buff.append("enum %s {" % self.enum_states_def)
+        buff.append(f"enum {self.enum_states_def} {{")
         buff += self.__get_enum_states_content()
         buff.append("};\n")
 
@@ -48,15 +48,15 @@ class Dot2c(Automata):
     def __get_enum_events_content(self) -> list[str]:
         buff = []
         for event in self.events:
-            buff.append("\t%s%s," % (event, self.enum_suffix))
+            buff.append(f"\t{event}{self.enum_suffix},")
 
-        buff.append("\tevent_max%s," % self.enum_suffix)
+        buff.append(f"\tevent_max{self.enum_suffix},")
 
         return buff
 
     def format_events_enum(self) -> list[str]:
         buff = []
-        buff.append("enum %s {" % self.enum_events_def)
+        buff.append(f"enum {self.enum_events_def} {{")
         buff += self.__get_enum_events_content()
         buff.append("};\n")
 
@@ -103,27 +103,27 @@ class Dot2c(Automata):
             min_type = "unsigned int"
 
         if self.states.__len__() > 1000000:
-            raise AutomataError("Too many states: %d" % self.states.__len__())
+            raise AutomataError(f"Too many states: {self.states.__len__()}")
 
         return min_type
 
     def format_automaton_definition(self) -> list[str]:
         min_type = self.get_minimun_type()
         buff = []
-        buff.append("struct %s {" % self.struct_automaton_def)
-        buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix))
-        buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix))
+        buff.append(f"struct {self.struct_automaton_def} {{")
+        buff.append(f"\tchar *state_names[state_max{self.enum_suffix}];")
+        buff.append(f"\tchar *event_names[event_max{self.enum_suffix}];")
         if self.is_hybrid_automata():
             buff.append(f"\tchar *env_names[env_max{self.enum_suffix}];")
-        buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix))
-        buff.append("\t%s initial_state;" % min_type)
-        buff.append("\tbool final_states[state_max%s];" % (self.enum_suffix))
+        buff.append(f"\t{min_type} function[state_max{self.enum_suffix}][event_max{self.enum_suffix}];")
+        buff.append(f"\t{min_type} initial_state;")
+        buff.append(f"\tbool final_states[state_max{self.enum_suffix}];")
         buff.append("};\n")
         return buff
 
     def format_aut_init_header(self) -> list[str]:
         buff = []
-        buff.append("static const struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def))
+        buff.append(f"static const struct {self.struct_automaton_def} {self.var_automaton_def} = {{")
         return buff
 
     def __get_string_vector_per_line_content(self, entries: list[str]) -> str:
@@ -179,9 +179,9 @@ class Dot2c(Automata):
                     next_state = self.function[x][y] + self.enum_suffix
 
                 if linetoolong:
-                    line += "\t\t\t%s" % next_state
+                    line += f"\t\t\t{next_state}"
                 else:
-                    line += "%*s" % (maxlen, next_state)
+                    line += f"{next_state:>{maxlen}}"
                 if y != nr_events-1:
                     line += ",\n" if linetoolong else ", "
                 else:
@@ -225,7 +225,7 @@ class Dot2c(Automata):
 
     def format_aut_init_final_states(self) -> list[str]:
        buff = []
-       buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states())
+       buff.append(f"\t.final_states = {{ {self.get_aut_init_final_states()} }},")
 
        return buff
 
@@ -241,7 +241,7 @@ class Dot2c(Automata):
 
     def format_invalid_state(self) -> list[str]:
         buff = []
-        buff.append("#define %s state_max%s\n" % (self.invalid_state_str, self.enum_suffix))
+        buff.append(f"#define {self.invalid_state_str} state_max{self.enum_suffix}\n")
 
         return buff
 
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 55222e38323f5..e26f2b47390ab 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -21,7 +21,8 @@ class dot2k(Monitor, Dot2c):
         self.monitor_type = MonitorType
         Monitor.__init__(self, extra_params)
         Dot2c.__init__(self, file_path, extra_params.get("model_name"))
-        self.enum_suffix = "_%s" % self.name
+        self.enum_suffix = f"_{self.name}"
+        self.enum_suffix = f"_{self.name}"
         self.monitor_class = extra_params["monitor_class"]
 
     def fill_monitor_type(self) -> str:
@@ -35,7 +36,7 @@ class dot2k(Monitor, Dot2c):
         buff = []
         buff += self._fill_hybrid_definitions()
         for event in self.events:
-            buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event)
+            buff.append(f"static void handle_{event}(void *data, /* XXX: fill header */)")
             buff.append("{")
             handle = "handle_event"
             if self.is_start_event(event):
@@ -46,13 +47,13 @@ class dot2k(Monitor, Dot2c):
                 handle = "handle_start_run_event"
             if self.monitor_type == "per_task":
                 buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;");
-                buff.append("\tda_%s(p, %s%s);" % (handle, event, self.enum_suffix));
+                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});");
             elif self.monitor_type == "per_obj":
                 buff.append("\tint id = /* XXX: how do I get the id? */;")
                 buff.append("\tmonitor_target t = /* XXX: how do I get t? */;")
                 buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});")
             else:
-                buff.append("\tda_%s(%s%s);" % (handle, event, self.enum_suffix));
+                buff.append(f"\tda_{handle}({event}{self.enum_suffix});");
             buff.append("}")
             buff.append("")
         return '\n'.join(buff)
@@ -60,25 +61,25 @@ class dot2k(Monitor, Dot2c):
     def fill_tracepoint_attach_probe(self) -> str:
         buff = []
         for event in self.events:
-            buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
+            buff.append(f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
         return '\n'.join(buff)
 
     def fill_tracepoint_detach_helper(self) -> str:
         buff = []
         for event in self.events:
-            buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event))
+            buff.append(f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_{event});")
         return '\n'.join(buff)
 
     def fill_model_h_header(self) -> list[str]:
         buff = []
         buff.append("/* SPDX-License-Identifier: GPL-2.0 */")
         buff.append("/*")
-        buff.append(" * Automatically generated C representation of %s automaton" % (self.name))
+        buff.append(f" * Automatically generated C representation of {self.name} automaton")
         buff.append(" * For further information about this format, see kernel documentation:")
         buff.append(" *   Documentation/trace/rv/deterministic_automata.rst")
         buff.append(" */")
         buff.append("")
-        buff.append("#define MONITOR_NAME %s" % (self.name))
+        buff.append(f"#define MONITOR_NAME {self.name}")
         buff.append("")
 
         return buff
@@ -87,11 +88,11 @@ class dot2k(Monitor, Dot2c):
         #
         # Adjust the definition names
         #
-        self.enum_states_def = "states_%s" % self.name
-        self.enum_events_def = "events_%s" % self.name
+        self.enum_states_def = f"states_{self.name}"
+        self.enum_events_def = f"events_{self.name}"
         self.enum_envs_def = f"envs_{self.name}"
-        self.struct_automaton_def = "automaton_%s" % self.name
-        self.var_automaton_def = "automaton_%s" % self.name
+        self.struct_automaton_def = f"automaton_{self.name}"
+        self.var_automaton_def = f"automaton_{self.name}"
 
         buff = self.fill_model_h_header()
         buff += self.format_model()
@@ -135,8 +136,8 @@ class dot2k(Monitor, Dot2c):
             tp_args.insert(0, tp_args_id)
         tp_proto_c = ", ".join([a+b for a,b in tp_args])
         tp_args_c = ", ".join([b for a,b in tp_args])
-        buff.append("	     TP_PROTO(%s)," % tp_proto_c)
-        buff.append("	     TP_ARGS(%s)" % tp_args_c)
+        buff.append(f"	     TP_PROTO({tp_proto_c}),")
+        buff.append(f"	     TP_ARGS({tp_args_c})")
         return '\n'.join(buff)
 
     def _fill_hybrid_definitions(self) -> list:
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index a2391a4c21ed6..61174b139123b 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -40,7 +40,7 @@ class RVGenerator:
         if platform.system() != "Linux":
             raise OSError("I can only run on Linux.")
 
-        kernel_path = os.path.join("/lib/modules/%s/build" % platform.release(), self.rv_dir)
+        kernel_path = os.path.join(f"/lib/modules/{platform.release()}/build", self.rv_dir)
 
         # if the current kernel is from a distro this may not be a full kernel tree
         # verify that one of the files we are going to modify is available
@@ -69,11 +69,11 @@ class RVGenerator:
             return self._read_file(path)
 
     def fill_parent(self):
-        return "&rv_%s" % self.parent if self.parent else "NULL"
+        return f"&rv_{self.parent}" if self.parent else "NULL"
 
     def fill_include_parent(self):
         if self.parent:
-            return "#include <monitors/%s/%s.h>\n" % (self.parent, self.parent)
+            return f"#include <monitors/{self.parent}/{self.parent}.h>\n"
         return ""
 
     def fill_tracepoint_handlers_skel(self):
@@ -119,7 +119,7 @@ class RVGenerator:
         buff = []
         buff.append("	# XXX: add dependencies if there")
         if self.parent:
-            buff.append("	depends on RV_MON_%s" % self.parent.upper())
+            buff.append(f"	depends on RV_MON_{self.parent.upper()}")
             buff.append("	default y")
         return '\n'.join(buff)
 
@@ -145,31 +145,30 @@ class RVGenerator:
         monitor_class_type = self.fill_monitor_class_type()
         if self.auto_patch:
             self._patch_file("rv_trace.h",
-                            "// Add new monitors based on CONFIG_%s here" % monitor_class_type,
-                            "#include <monitors/%s/%s_trace.h>" % (self.name, self.name))
-            return "  - Patching %s/rv_trace.h, double check the result" % self.rv_dir
+                            f"// Add new monitors based on CONFIG_{monitor_class_type} here",
+                            f"#include <monitors/{self.name}/{self.name}_trace.h>")
+            return f"  - Patching {self.rv_dir}/rv_trace.h, double check the result"
 
-        return """  - Edit %s/rv_trace.h:
-Add this line where other tracepoints are included and %s is defined:
-#include <monitors/%s/%s_trace.h>
-""" % (self.rv_dir, monitor_class_type, self.name, self.name)
+        return f"""  - Edit {self.rv_dir}/rv_trace.h:
+Add this line where other tracepoints are included and {monitor_class_type} is defined:
+#include <monitors/{self.name}/{self.name}_trace.h>
+"""
 
     def _kconfig_marker(self, container=None) -> str:
-        return "# Add new %smonitors here" % (container + " "
-                                              if container else "")
+        return f"# Add new {container + ' ' if container else ''}monitors here"
 
     def fill_kconfig_tooltip(self):
         if self.auto_patch:
             # monitors with a container should stay together in the Kconfig
             self._patch_file("Kconfig",
                              self._kconfig_marker(self.parent),
-                            "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name))
-            return "  - Patching %s/Kconfig, double check the result" % self.rv_dir
+                            f"source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"")
+            return f"  - Patching {self.rv_dir}/Kconfig, double check the result"
 
-        return """  - Edit %s/Kconfig:
+        return f"""  - Edit {self.rv_dir}/Kconfig:
 Add this line where other monitors are included:
-source \"kernel/trace/rv/monitors/%s/Kconfig\"
-""" % (self.rv_dir, self.name)
+source \"kernel/trace/rv/monitors/{self.name}/Kconfig\"
+"""
 
     def fill_makefile_tooltip(self):
         name = self.name
@@ -177,18 +176,18 @@ source \"kernel/trace/rv/monitors/%s/Kconfig\"
         if self.auto_patch:
             self._patch_file("Makefile",
                             "# Add new monitors here",
-                            "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name))
-            return "  - Patching %s/Makefile, double check the result" % self.rv_dir
+                            f"obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o")
+            return f"  - Patching {self.rv_dir}/Makefile, double check the result"
 
-        return """  - Edit %s/Makefile:
+        return f"""  - Edit {self.rv_dir}/Makefile:
 Add this line where other monitors are included:
-obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
-""" % (self.rv_dir, name_up, name, name)
+obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
+"""
 
     def fill_monitor_tooltip(self):
         if self.auto_patch:
-            return "  - Monitor created in %s/monitors/%s" % (self.rv_dir, self. name)
-        return "  - Move %s/ to the kernel's monitor directory (%s/monitors)" % (self.name, self.rv_dir)
+            return f"  - Monitor created in {self.rv_dir}/monitors/{self.name}"
+        return f"  - Move {self.name}/ to the kernel's monitor directory ({self.rv_dir}/monitors)"
 
     def __create_directory(self):
         path = self.name
@@ -205,13 +204,13 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
         file.close()
 
     def _create_file(self, file_name, content):
-        path = "%s/%s" % (self.name, file_name)
+        path = f"{self.name}/{file_name}"
         if self.auto_patch:
             path = os.path.join(self.rv_dir, "monitors", path)
         self.__write_file(path, content)
 
     def __get_main_name(self):
-        path = "%s/%s" % (self.name, "main.c")
+        path = f"{self.name}/main.c"
         if not os.path.exists(path):
             return "main.c"
         return "__main.c"
@@ -221,11 +220,11 @@ obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o
 
         self.__create_directory()
 
-        path = "%s.c" % self.name
+        path = f"{self.name}.c"
         self._create_file(path, main_c)
 
         model_h = self.fill_model_h()
-        path = "%s.h" % self.name
+        path = f"{self.name}.h"
         self._create_file(path, model_h)
 
         kconfig = self.fill_kconfig()
@@ -258,5 +257,5 @@ class Monitor(RVGenerator):
     def print_files(self):
         super().print_files()
         trace_h = self.fill_trace_h()
-        path = "%s_trace.h" % self.name
+        path = f"{self.name}_trace.h"
         self._create_file(path, trace_h)
diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index 08ad245462e7d..b6300c38154dc 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -77,7 +77,7 @@ class ltl2k(generator.Monitor):
         ]
 
         for node in self.ba:
-            buf.append("\tS%i," % node.id)
+            buf.append(f"\tS{node.id},")
         buf.append("\tRV_NUM_BA_STATES")
         buf.append("};")
         buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);")
@@ -86,7 +86,7 @@ class ltl2k(generator.Monitor):
     def _fill_atoms(self):
         buf = ["enum ltl_atom {"]
         for a in sorted(self.atoms):
-            buf.append("\tLTL_%s," % a)
+            buf.append(f"\tLTL_{a},")
         buf.append("\tLTL_NUM_ATOM")
         buf.append("};")
         buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);")
@@ -100,7 +100,7 @@ class ltl2k(generator.Monitor):
         ]
 
         for name in self.atoms_abbr:
-            buf.append("\t\t\"%s\"," % name)
+            buf.append(f"\t\t\"{name}\",")
 
         buf.extend([
             "\t};",
@@ -117,19 +117,19 @@ class ltl2k(generator.Monitor):
                 continue
 
             if isinstance(node.op, ltl2ba.AndOp):
-                buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right))
+                buf.append(f"\tbool {node} = {node.op.left} && {node.op.right};")
                 required_values |= {str(node.op.left), str(node.op.right)}
             elif isinstance(node.op, ltl2ba.OrOp):
-                buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right))
+                buf.append(f"\tbool {node} = {node.op.left} || {node.op.right};")
                 required_values |= {str(node.op.left), str(node.op.right)}
             elif isinstance(node.op, ltl2ba.NotOp):
-                buf.append("\tbool %s = !%s;" % (node, node.op.child))
+                buf.append(f"\tbool {node} = !{node.op.child};")
                 required_values.add(str(node.op.child))
 
         for atom in self.atoms:
             if atom.lower() not in required_values:
                 continue
-            buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (atom.lower(), atom))
+            buf.append(f"\tbool {atom.lower()} = test_bit(LTL_{atom}, mon->atoms);")
 
         buf.reverse()
 
@@ -157,7 +157,7 @@ class ltl2k(generator.Monitor):
         ])
 
         for node in self.ba:
-            buf.append("\tcase S%i:" % node.id)
+            buf.append(f"\tcase S{node.id}:")
 
             for o in sorted(node.outgoing):
                 line   = "\t\tif "
@@ -167,7 +167,7 @@ class ltl2k(generator.Monitor):
                 lines = break_long_line(line, indent)
                 buf.extend(lines)
 
-                buf.append("\t\t\t__set_bit(S%i, next);" % o.id)
+                buf.append(f"\t\t\t__set_bit(S{o.id}, next);")
             buf.append("\t\tbreak;")
         buf.extend([
             "\t}",
@@ -201,7 +201,7 @@ class ltl2k(generator.Monitor):
             lines = break_long_line(line, indent)
             buf.extend(lines)
 
-            buf.append("\t\t__set_bit(S%i, mon->states);" % node.id)
+            buf.append(f"\t\t__set_bit(S{node.id}, mon->states);")
         buf.append("}")
         return buf
 
@@ -209,23 +209,21 @@ class ltl2k(generator.Monitor):
         buff = []
         buff.append("static void handle_example_event(void *data, /* XXX: fill header */)")
         buff.append("{")
-        buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.atoms[0])
+        buff.append(f"\tltl_atom_update(task, LTL_{self.atoms[0]}, true/false);")
         buff.append("}")
         buff.append("")
         return '\n'.join(buff)
 
     def fill_tracepoint_attach_probe(self):
-        return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_example_event);" \
-                % self.name
+        return f"\trv_attach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_example_event);"
 
     def fill_tracepoint_detach_helper(self):
-        return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_sample_event);" \
-                % self.name
+        return f"\trv_detach_trace_probe(\"{self.name}\", /* XXX: tracepoint */, handle_sample_event);"
 
     def fill_atoms_init(self):
         buff = []
         for a in self.atoms:
-            buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a)
+            buff.append(f"\tltl_atom_set(mon, LTL_{a}, true/false);")
         return '\n'.join(buff)
 
     def fill_model_h(self):
-- 
2.53.0

[PATCH v3 04/19] rv/rvgen: replace __len__() calls with len()

[Wander Lairson Costa]

Replace all direct calls to the __len__() dunder method with the
idiomatic len() built-in function across the rvgen codebase. This
change eliminates a Python anti-pattern where dunder methods are
called directly instead of using their corresponding built-in
functions.

The changes affect nine instances across two files. In automata.py,
the empty string check is further improved by using truthiness
testing instead of explicit length comparison. In dot2c.py, all
length checks in the get_minimun_type, __get_max_strlen_of_states,
and get_aut_init_function methods now use the standard len()
function. Additionally, spacing around keyword arguments has been
corrected to follow PEP 8 guidelines.

Direct calls to dunder methods like __len__() are discouraged in
Python because they bypass the language's abstraction layer and
reduce code readability. Using len() provides the same functionality
while adhering to Python community standards and making the code more
familiar to Python developers.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/rvgen/automata.py |  2 +-
 tools/verification/rvgen/rvgen/dot2c.py    | 16 ++++++++--------
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 4fed58cfa3c6e..4f5681265ee24 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -82,7 +82,7 @@ class Automata:
             raise AutomataError(f"not a dot file: {self.__dot_path}")
 
         model_name = ntpath.splitext(basename)[0]
-        if model_name.__len__() == 0:
+        if not model_name:
             raise AutomataError(f"not a dot file: {self.__dot_path}")
 
         return model_name
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index e6a440e1588cd..fa44795adef46 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -96,14 +96,14 @@ class Dot2c(Automata):
     def get_minimun_type(self) -> str:
         min_type = "unsigned char"
 
-        if self.states.__len__() > 255:
+        if len(self.states) > 255:
             min_type = "unsigned short"
 
-        if self.states.__len__() > 65535:
+        if len(self.states) > 65535:
             min_type = "unsigned int"
 
-        if self.states.__len__() > 1000000:
-            raise AutomataError(f"Too many states: {self.states.__len__()}")
+        if len(self.states) > 1000000:
+            raise AutomataError(f"Too many states: {len(self.states)}")
 
         return min_type
 
@@ -159,12 +159,12 @@ class Dot2c(Automata):
         return buff
 
     def __get_max_strlen_of_states(self) -> int:
-        max_state_name = max(self.states, key = len).__len__()
-        return max(max_state_name, self.invalid_state_str.__len__())
+        max_state_name = len(max(self.states, key=len))
+        return max(max_state_name, len(self.invalid_state_str))
 
     def get_aut_init_function(self) -> str:
-        nr_states = self.states.__len__()
-        nr_events = self.events.__len__()
+        nr_states = len(self.states)
+        nr_events = len(self.events)
         buff = []
 
         maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix)
-- 
2.53.0

[PATCH v3 05/19] rv/rvgen: remove unnecessary semicolons

[Wander Lairson Costa]

Remove unnecessary semicolons from Python code in the rvgen tool.
Python does not require semicolons to terminate statements, and
their presence goes against PEP 8 style guidelines. These semicolons
were likely added out of habit from C-style languages.

This cleanup improves consistency with Python coding standards and
aligns with the recent improvements to remove other Python
anti-patterns from the codebase.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/dot2k.py | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index e26f2b47390ab..47af9f104a829 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -46,14 +46,14 @@ class dot2k(Monitor, Dot2c):
                 buff.append("\t/* XXX: validate that this event is only valid in the initial state */")
                 handle = "handle_start_run_event"
             if self.monitor_type == "per_task":
-                buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;");
-                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});");
+                buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;")
+                buff.append(f"\tda_{handle}(p, {event}{self.enum_suffix});")
             elif self.monitor_type == "per_obj":
                 buff.append("\tint id = /* XXX: how do I get the id? */;")
                 buff.append("\tmonitor_target t = /* XXX: how do I get t? */;")
                 buff.append(f"\tda_{handle}(id, t, {event}{self.enum_suffix});")
             else:
-                buff.append(f"\tda_{handle}({event}{self.enum_suffix});");
+                buff.append(f"\tda_{handle}({event}{self.enum_suffix});")
             buff.append("}")
             buff.append("")
         return '\n'.join(buff)
-- 
2.53.0

[PATCH v3 06/19] rv/rvgen: use context managers for file operations

[Wander Lairson Costa]

Replace manual file open and close operations with context managers
throughout the rvgen codebase. The previous implementation used
explicit open() and close() calls, which could lead to resource leaks
if exceptions occurred between opening and closing the file handles.

This change affects three file operations: reading DOT specification
files in the automata parser, reading template files in the generator
base class, and writing generated monitor files. All now use the with
statement to ensure proper resource cleanup even in error conditions.

Context managers provide automatic cleanup through the with statement,
which guarantees that file handles are closed when the with block
exits regardless of whether an exception occurred. This follows PEP
343 recommendations and is the standard Python idiom for resource
management. The change also reduces code verbosity while improving
safety and maintainability.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py  |  6 ++----
 tools/verification/rvgen/rvgen/generator.py | 12 ++++--------
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 4f5681265ee24..10146b6061ed2 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -91,13 +91,11 @@ class Automata:
         cursor = 0
         dot_lines = []
         try:
-            dot_file = open(self.__dot_path)
+            with open(self.__dot_path) as dot_file:
+                dot_lines = dot_file.read().splitlines()
         except OSError as exc:
             raise AutomataError(exc.strerror) from exc
 
-        dot_lines = dot_file.read().splitlines()
-        dot_file.close()
-
         # checking the first line:
         line = dot_lines[cursor].split()
 
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 61174b139123b..d932e96dd66d3 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -51,11 +51,8 @@ class RVGenerator:
         raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?")
 
     def _read_file(self, path):
-        fd = open(path, 'r')
-
-        content = fd.read()
-
-        fd.close()
+        with open(path, 'r') as fd:
+            content = fd.read()
         return content
 
     def _read_template_file(self, file):
@@ -199,9 +196,8 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
             return
 
     def __write_file(self, file_name, content):
-        file = open(file_name, 'w')
-        file.write(content)
-        file.close()
+        with open(file_name, 'w') as file:
+            file.write(content)
 
     def _create_file(self, file_name, content):
         path = f"{self.name}/{file_name}"
-- 
2.53.0

[PATCH v3 07/19] rv/rvgen: fix typos in automata and generator docstring and comments

[Wander Lairson Costa]

Fix two typos in the Automata class documentation that have been
present since the initial implementation. Fix the class
docstring: "part it" instead of "parses it". Additionally, a
comment describing transition labels contained the misspelling
"lables" instead of "labels".

Fix a typo in the comment describing the insertion of the initial
state into the states list: "bein og" should be "beginning of".

Fix typo in the module docstring: "Abtract" should be "Abstract".

Fix several occurrences of "automata" where it should be the singular
form "automaton".

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py  | 8 ++++----
 tools/verification/rvgen/rvgen/dot2c.py     | 2 +-
 tools/verification/rvgen/rvgen/dot2k.py     | 4 ++--
 tools/verification/rvgen/rvgen/generator.py | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 10146b6061ed2..b25378e92b16d 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -3,7 +3,7 @@
 #
 # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
 #
-# Automata object: parse an automata in dot file digraph format into a python object
+# Automata class: parse an automaton in dot file digraph format into a python object
 #
 # For further information, see:
 #   Documentation/trace/rv/deterministic_automata.rst
@@ -33,7 +33,7 @@ class AutomataError(Exception):
     """
 
 class Automata:
-    """Automata class: Reads a dot file and part it as an automata.
+    """Automata class: Reads a dot file and parses it as an automaton.
 
     It supports both deterministic and hybrid automata.
 
@@ -153,7 +153,7 @@ class Automata:
         states = sorted(set(states))
         states.remove(initial_state)
 
-        # Insert the initial state at the bein og the states
+        # Insert the initial state at the beginning of the states
         states.insert(0, initial_state)
 
         if not has_final_states:
@@ -175,7 +175,7 @@ class Automata:
                 line = self.__dot_lines[cursor].split()
                 event = "".join(line[line.index("label") + 2:-1]).replace('"', '')
 
-                # when a transition has more than one lables, they are like this
+                # when a transition has more than one labels, they are like this
                 # "local_irq_enable\nhw_local_irq_enable_n"
                 # so split them.
 
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index fa44795adef46..9255cc2153a31 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -3,7 +3,7 @@
 #
 # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
 #
-# dot2c: parse an automata in dot file digraph format into a C
+# dot2c: parse an automaton in dot file digraph format into a C
 #
 # This program was written in the development of this paper:
 #  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index 47af9f104a829..aedc2a7799b32 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -167,14 +167,14 @@ class da2k(dot2k):
     def __init__(self, *args, **kwargs):
         super().__init__(*args, **kwargs)
         if self.is_hybrid_automata():
-            raise AutomataError("Detected hybrid automata, use the 'ha' class")
+            raise AutomataError("Detected hybrid automaton, use the 'ha' class")
 
 class ha2k(dot2k):
     """Hybrid automata only"""
     def __init__(self, *args, **kwargs):
         super().__init__(*args, **kwargs)
         if not self.is_hybrid_automata():
-            raise AutomataError("Detected deterministic automata, use the 'da' class")
+            raise AutomataError("Detected deterministic automaton, use the 'da' class")
         self.trace_h = self._read_template_file("trace_hybrid.h")
         self.__parse_constraints()
 
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index d932e96dd66d3..988ccdc27fa37 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -3,7 +3,7 @@
 #
 # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
 #
-# Abtract class for generating kernel runtime verification monitors from specification file
+# Abstract class for generating kernel runtime verification monitors from specification file
 
 import platform
 import os
-- 
2.53.0

[PATCH v3 08/19] rv/rvgen: fix PEP 8 whitespace violations

[Wander Lairson Costa]

Fix whitespace violations throughout the rvgen codebase to comply
with PEP 8 style guidelines. The changes address missing whitespace
after commas, around operators, and in collection literals that
were flagged by pycodestyle.

The fixes include adding whitespace after commas in string replace
chains and function arguments, adding whitespace around arithmetic
operators, removing extra whitespace in list comprehensions, and
fixing dictionary literal spacing. These changes improve code
readability and consistency with Python coding standards.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/rvgen/automata.py  | 8 ++++----
 tools/verification/rvgen/rvgen/dot2c.py     | 2 +-
 tools/verification/rvgen/rvgen/dot2k.py     | 4 ++--
 tools/verification/rvgen/rvgen/generator.py | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index b25378e92b16d..e54486c69a191 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -135,7 +135,7 @@ class Automata:
             raw_state = line[-1]
 
             #  "enabled_fired"}; -> enabled_fired
-            state = raw_state.replace('"', '').replace('};', '').replace(',','_')
+            state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
             if state[0:7] == "__init_":
                 initial_state = state[7:]
             else:
@@ -264,7 +264,7 @@ class Automata:
             nr_state += 1
 
         # declare the matrix....
-        matrix = [[ self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
+        matrix = [[self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
         constraints: dict[_ConstraintKey, list[str]] = {}
 
         # and we are back! Let's fill the matrix
@@ -273,8 +273,8 @@ class Automata:
         while self.__dot_lines[cursor].lstrip()[0] == '"':
             if self.__dot_lines[cursor].split()[1] == "->":
                 line = self.__dot_lines[cursor].split()
-                origin_state = line[0].replace('"','').replace(',','_')
-                dest_state = line[2].replace('"','').replace(',','_')
+                origin_state = line[0].replace('"', '').replace(',', '_')
+                dest_state = line[2].replace('"', '').replace(',', '_')
                 possible_events = "".join(line[line.index("label") + 2:-1]).replace('"', '')
                 for event in possible_events.split("\\n"):
                     event, *constr = event.split(";")
diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py
index 9255cc2153a31..fc85ba1f649e7 100644
--- a/tools/verification/rvgen/rvgen/dot2c.py
+++ b/tools/verification/rvgen/rvgen/dot2c.py
@@ -182,7 +182,7 @@ class Dot2c(Automata):
                     line += f"\t\t\t{next_state}"
                 else:
                     line += f"{next_state:>{maxlen}}"
-                if y != nr_events-1:
+                if y != nr_events - 1:
                     line += ",\n" if linetoolong else ", "
                 else:
                     line += ",\n\t\t}," if linetoolong else " },"
diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py
index aedc2a7799b32..e6f476b903b0a 100644
--- a/tools/verification/rvgen/rvgen/dot2k.py
+++ b/tools/verification/rvgen/rvgen/dot2k.py
@@ -134,8 +134,8 @@ class dot2k(Monitor, Dot2c):
         tp_args = tp_args_dict[tp_type]
         if self._is_id_monitor():
             tp_args.insert(0, tp_args_id)
-        tp_proto_c = ", ".join([a+b for a,b in tp_args])
-        tp_args_c = ", ".join([b for a,b in tp_args])
+        tp_proto_c = ", ".join([a + b for a, b in tp_args])
+        tp_args_c = ", ".join([b for a, b in tp_args])
         buff.append(f"	     TP_PROTO({tp_proto_c}),")
         buff.append(f"	     TP_ARGS({tp_args_c})")
         return '\n'.join(buff)
diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 988ccdc27fa37..40d82afb018f5 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -228,7 +228,7 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
 
 
 class Monitor(RVGenerator):
-    monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3, "per_obj" : 4 }
+    monitor_types = {"global": 1, "per_cpu": 2, "per_task": 3, "per_obj": 4}
 
     def __init__(self, extra_params={}):
         super().__init__(extra_params)
-- 
2.53.0

[PATCH v3 09/19] rv/rvgen: fix DOT file validation logic error

[Wander Lairson Costa]

Fix incorrect boolean logic in automata DOT file format validation
that allowed malformed files to pass undetected. The previous
implementation used a logical AND operator where OR was required,
causing the validation to only reject files when both the first
token was not "digraph" AND the second token was not
"state_automaton". This meant a file starting with "digraph" but
having an incorrect second token would incorrectly pass validation.

The corrected logic properly rejects DOT files where either the
first token is not "digraph" or the second token is not
"state_automaton", ensuring that only properly formatted automaton
definition files are accepted for processing. Without this fix,
invalid DOT files could cause downstream parsing failures or
generate incorrect C code for runtime verification monitors.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index e54486c69a191..e4c0335cd0fba 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -99,7 +99,7 @@ class Automata:
         # checking the first line:
         line = dot_lines[cursor].split()
 
-        if (line[0] != "digraph") and (line[1] != "state_automaton"):
+        if (line[0] != "digraph") or (line[1] != "state_automaton"):
             raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
         else:
             cursor += 1
-- 
2.53.0

[PATCH v3 10/19] rv/rvgen: use class constant for init marker

[Wander Lairson Costa]

Replace hardcoded string literal and magic number with a class
constant for the initial state marker in DOT file parsing. The
previous implementation used the magic string "__init_" directly
in the code along with a hardcoded length of 7 for substring
extraction, which made the code less maintainable and harder to
understand.

This change introduces a class constant init_marker to serve as
a single source of truth for the initial state prefix. The code
now uses startswith() for clearer intent and calculates the
substring position dynamically using len(), eliminating the magic
number. If the marker value needs to change in the future, only
the constant definition requires updating rather than multiple
locations in the code.

The refactoring improves code readability and maintainability
while preserving the exact same runtime behavior.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/rvgen/automata.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index e4c0335cd0fba..cdec78a4bbbae 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -42,6 +42,7 @@ class Automata:
     """
 
     invalid_state_str = "INVALID_STATE"
+    init_marker = "__init_"
     # val can be numerical, uppercase (constant or macro), lowercase (parameter or function)
     # only numerical values should have units
     constraint_rule = re.compile(r"""
@@ -136,8 +137,8 @@ class Automata:
 
             #  "enabled_fired"}; -> enabled_fired
             state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
-            if state[0:7] == "__init_":
-                initial_state = state[7:]
+            if state.startswith(self.init_marker):
+                initial_state = state[len(self.init_marker):]
             else:
                 states.append(state)
                 if "doublecircle" in self.__dot_lines[cursor]:
-- 
2.53.0

[PATCH v3 11/19] rv/rvgen: refactor automata.py to use iterator-based parsing

[Wander Lairson Costa]

Refactor the DOT file parsing logic in automata.py to use Python's
iterator-based patterns instead of manual cursor indexing. The previous
implementation relied on while loops with explicit cursor management,
which made the code prone to off-by-one errors and would crash on
malformed input files containing empty lines.

The new implementation uses enumerate and itertools.islice to iterate
over lines, eliminating manual cursor tracking. Functions that search
for specific markers now use for loops with early returns and explicit
AutomataError exceptions for missing markers, rather than assuming the
markers exist. Additional bounds checking ensures that split line
arrays have sufficient elements before accessing specific indices,
preventing IndexError exceptions on malformed DOT files.

The matrix creation and event variable extraction methods now use
functional patterns with map combined with itertools.islice,
making the intent clearer while maintaining the same behavior. Minor
improvements include using extend instead of append in a loop, adding
empty file validation, and replacing enumerate with range where the
enumerated value was unused.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 116 +++++++++++++--------
 1 file changed, 71 insertions(+), 45 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index cdec78a4bbbae..6613a9d6159a9 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -11,6 +11,7 @@
 import ntpath
 import re
 from typing import Iterator
+from itertools import islice
 
 class _ConstraintKey:
     """Base class for constraint keys."""
@@ -89,37 +90,54 @@ class Automata:
         return model_name
 
     def __open_dot(self) -> list[str]:
-        cursor = 0
         dot_lines = []
         try:
             with open(self.__dot_path) as dot_file:
-                dot_lines = dot_file.read().splitlines()
+                dot_lines = dot_file.readlines()
         except OSError as exc:
             raise AutomataError(exc.strerror) from exc
 
+        if not dot_lines:
+            raise AutomataError(f"{self.__dot_path} is empty")
+
         # checking the first line:
-        line = dot_lines[cursor].split()
+        line = dot_lines[0].split()
 
-        if (line[0] != "digraph") or (line[1] != "state_automaton"):
+        if len(line) < 2 or line[0] != "digraph" or line[1] != "state_automaton":
             raise AutomataError(f"Not a valid .dot format: {self.__dot_path}")
-        else:
-            cursor += 1
+
         return dot_lines
 
     def __get_cursor_begin_states(self) -> int:
-        cursor = 0
-        while self.__dot_lines[cursor].split()[0] != "{node":
-            cursor += 1
-        return cursor
+        for cursor, line in enumerate(self.__dot_lines):
+            split_line = line.split()
+
+            if len(split_line) and split_line[0] == "{node":
+                return cursor
+
+        raise AutomataError("Could not find a beginning state")
 
     def __get_cursor_begin_events(self) -> int:
-        cursor = 0
-        while self.__dot_lines[cursor].split()[0] != "{node":
-            cursor += 1
-        while self.__dot_lines[cursor].split()[0] == "{node":
-            cursor += 1
-        # skip initial state transition
-        cursor += 1
+        state = 0
+        cursor = 0 # make pyright happy
+
+        for cursor, line in enumerate(self.__dot_lines):
+            line = line.split()
+            if not line:
+                continue
+
+            if state == 0:
+                if line[0] == "{node":
+                    state = 1
+            elif line[0] != "{node":
+                break
+        else:
+            raise AutomataError("Could not find beginning event")
+
+        cursor += 1 # skip initial state transition
+        if cursor == len(self.__dot_lines):
+            raise AutomataError("Dot file ended after event beginning")
+
         return cursor
 
     def __get_state_variables(self) -> tuple[list[str], str, list[str]]:
@@ -131,9 +149,12 @@ class Automata:
         cursor = self.__get_cursor_begin_states()
 
         # process nodes
-        while self.__dot_lines[cursor].split()[0] == "{node":
-            line = self.__dot_lines[cursor].split()
-            raw_state = line[-1]
+        for line in islice(self.__dot_lines, cursor, None):
+            split_line = line.split()
+            if not split_line or split_line[0] != "{node":
+                break
+
+            raw_state = split_line[-1]
 
             #  "enabled_fired"}; -> enabled_fired
             state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
@@ -141,16 +162,14 @@ class Automata:
                 initial_state = state[len(self.init_marker):]
             else:
                 states.append(state)
-                if "doublecircle" in self.__dot_lines[cursor]:
+                if "doublecircle" in line:
                     final_states.append(state)
                     has_final_states = True
 
-                if "ellipse" in self.__dot_lines[cursor]:
+                if "ellipse" in line:
                     final_states.append(state)
                     has_final_states = True
 
-            cursor += 1
-
         states = sorted(set(states))
         states.remove(initial_state)
 
@@ -163,18 +182,21 @@ class Automata:
         return states, initial_state, final_states
 
     def __get_event_variables(self) -> tuple[list[str], list[str]]:
+        events: list[str] = []
+        envs: list[str] = []
         # here we are at the begin of transitions, take a note, we will return later.
         cursor = self.__get_cursor_begin_events()
 
-        events = []
-        envs = []
-        while self.__dot_lines[cursor].lstrip()[0] == '"':
+        for line in map(str.lstrip, islice(self.__dot_lines, cursor, None)):
+            if not line.startswith('"'):
+                break
+
             # transitions have the format:
             # "all_fired" -> "both_fired" [ label = "disable_irq" ];
             #  ------------ event is here ------------^^^^^
-            if self.__dot_lines[cursor].split()[1] == "->":
-                line = self.__dot_lines[cursor].split()
-                event = "".join(line[line.index("label") + 2:-1]).replace('"', '')
+            split_line = line.split()
+            if len(split_line) > 1 and split_line[1] == "->":
+                event = "".join(split_line[split_line.index("label") + 2:-1]).replace('"', '')
 
                 # when a transition has more than one labels, they are like this
                 # "local_irq_enable\nhw_local_irq_enable_n"
@@ -187,7 +209,7 @@ class Automata:
                     ev, *constr = i.split(";")
                     if constr:
                         if len(constr) > 2:
-                            raise ValueError("Only 1 constraint and 1 reset are supported")
+                            raise AutomataError("Only 1 constraint and 1 reset are supported")
                         envs += self.__extract_env_var(constr)
                     events.append(ev)
             else:
@@ -195,13 +217,12 @@ class Automata:
                 # "enable_fired" [label = "enable_fired\ncondition"];
                 #  ----- label is here -----^^^^^
                 # label and node name must be the same, condition is optional
-                state = self.__dot_lines[cursor].split("label")[1].split('"')[1]
+                state = line.split("label")[1].split('"')[1]
                 _, *constr = state.split("\\n")
                 if constr:
                     if len(constr) > 1:
-                        raise ValueError("Only 1 constraint is supported in the state")
+                        raise AutomataError("Only 1 constraint is supported in the state")
                     envs += self.__extract_env_var([constr[0].replace(" ", "")])
-            cursor += 1
 
         return sorted(set(events)), sorted(set(envs))
 
@@ -265,18 +286,24 @@ class Automata:
             nr_state += 1
 
         # declare the matrix....
-        matrix = [[self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
+        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()
 
-        while self.__dot_lines[cursor].lstrip()[0] == '"':
-            if self.__dot_lines[cursor].split()[1] == "->":
-                line = self.__dot_lines[cursor].split()
-                origin_state = line[0].replace('"', '').replace(',', '_')
-                dest_state = line[2].replace('"', '').replace(',', '_')
-                possible_events = "".join(line[line.index("label") + 2:-1]).replace('"', '')
+        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:
@@ -287,22 +314,21 @@ class Automata:
                             self.self_loop_reset_events.add(event)
                     matrix[states_dict[origin_state]][events_dict[event]] = dest_state
             else:
-                state = self.__dot_lines[cursor].split("label")[1].split('"')[1]
+                state = line.split("label")[1].split('"')[1]
                 state, *constr = state.replace(" ", "").split("\\n")
                 if constr:
                     constraints[_StateConstraintKey(states_dict[state])] = constr
-            cursor += 1
 
         return matrix, constraints
 
     def __store_init_events(self) -> tuple[list[bool], list[bool]]:
         events_start = [False] * len(self.events)
         events_start_run = [False] * len(self.events)
-        for i, _ in enumerate(self.events):
+        for i in range(len(self.events)):
             curr_event_will_init = 0
             curr_event_from_init = False
             curr_event_used = 0
-            for j, _ in enumerate(self.states):
+            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:
-- 
2.53.0

[PATCH v3 12/19] rv/rvgen: remove unused sys import from dot2c

[Wander Lairson Costa]

The sys module was imported in the dot2c frontend script but never
used. This import was likely left over from earlier development or
copied from a template that required sys for exit handling.

Remove the unused import to clean up the code and satisfy linters
that flag unused imports as errors.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/dot2c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tools/verification/rvgen/dot2c b/tools/verification/rvgen/dot2c
index bf0c67c5b66c8..1012becc7fab6 100644
--- a/tools/verification/rvgen/dot2c
+++ b/tools/verification/rvgen/dot2c
@@ -16,7 +16,6 @@
 if __name__ == '__main__':
     from rvgen import dot2c
     import argparse
-    import sys
 
     parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure')
     parser.add_argument('dot_file',  help='The dot file to be converted')
-- 
2.53.0

[PATCH v3 13/19] rv/rvgen: remove unused __get_main_name method

[Wander Lairson Costa]

The __get_main_name() method in the generator module is never called
from anywhere in the codebase. Remove this dead code to improve
maintainability.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/generator.py | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py
index 40d82afb018f5..56f3bd8db8503 100644
--- a/tools/verification/rvgen/rvgen/generator.py
+++ b/tools/verification/rvgen/rvgen/generator.py
@@ -205,12 +205,6 @@ obj-$(CONFIG_RV_MON_{name_up}) += monitors/{name}/{name}.o
             path = os.path.join(self.rv_dir, "monitors", path)
         self.__write_file(path, content)
 
-    def __get_main_name(self):
-        path = f"{self.name}/main.c"
-        if not os.path.exists(path):
-            return "main.c"
-        return "__main.c"
-
     def print_files(self):
         main_c = self.fill_main_c()
 
-- 
2.53.0

[PATCH v3 14/19] rv/rvgen: make monitor arguments required in rvgen

[Wander Lairson Costa]

Add required=True to the monitor subcommand arguments for class, spec,
and monitor_type in rvgen. These arguments are essential for monitor
generation and attempting to run without them would cause AttributeError
exceptions later in the code when the script tries to access them.

Making these arguments explicitly required provides clearer error
messages to users at parse time rather than cryptic exceptions during
execution. This improves the user experience by catching missing
arguments early with helpful usage information.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/__main__.py | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py
index 2e5b868535470..5c923dc10d0f0 100644
--- a/tools/verification/rvgen/__main__.py
+++ b/tools/verification/rvgen/__main__.py
@@ -31,10 +31,11 @@ if __name__ == '__main__':
     monitor_parser.add_argument('-n', "--model_name", dest="model_name")
     monitor_parser.add_argument("-p", "--parent", dest="parent",
                                 required=False, help="Create a monitor nested to parent")
-    monitor_parser.add_argument('-c', "--class", dest="monitor_class",
+    monitor_parser.add_argument('-c', "--class", dest="monitor_class", required=True,
                                 help="Monitor class, either \"da\", \"ha\" or \"ltl\"")
-    monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file")
-    monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type",
+    monitor_parser.add_argument('-s', "--spec", dest="spec", required=True,
+                                help="Monitor specification file")
+    monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True,
                                 help=f"Available options: {', '.join(Monitor.monitor_types.keys())}")
 
     container_parser = subparsers.add_parser("container", parents=[parent_parser])
-- 
2.53.0

[PATCH v3 15/19] rv/rvgen: fix isinstance check in Variable.expand()

[Wander Lairson Costa]

The Variable.expand() method in ltl2ba.py performs contradiction
detection by checking if a negated variable already exists in the
graph node's old set. However, the isinstance check was incorrectly
testing the ASTNode wrapper instead of the wrapped operator, causing
the check to always return False.

The old set contains ASTNode instances which wrap LTL operators via
their .op attribute. The fix changes isinstance(f, NotOp) to
isinstance(f.op, NotOp) to correctly examine the wrapped operator
type. This follows the established pattern used elsewhere in the
file, such as the iteration at lines 572-574 which accesses
o.op.is_temporal() on items from node.old.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Nam Cao <namcao@linutronix.de>
---
 tools/verification/rvgen/rvgen/ltl2ba.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index f9855dfa3bc1c..7f538598a8681 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py
@@ -395,7 +395,7 @@ class Variable:
     @staticmethod
     def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]:
         for f in node.old:
-            if isinstance(f, NotOp) and f.op.child is n:
+            if isinstance(f.op, NotOp) and f.op.child is n:
                 return node_set
         node.old |= {n}
         return node.expand(node_set)
-- 
2.53.0

[PATCH v3 16/19] rv/rvgen: extract node marker string to class constant

[Wander Lairson Costa]

Add a node_marker class constant to the Automata class to replace the
hardcoded "{node" string literal used throughout the DOT file parsing
logic. This follows the existing pattern established by the init_marker
and invalid_state_str class constants in the same class.

The "{node" string is used as a marker to identify node declaration
lines in DOT files during state variable extraction and cursor
positioning. Extracting it to a named constant improves code
maintainability and makes the marker's purpose explicit.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 6613a9d6159a9..fd2a4a0c3f6eb 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -44,6 +44,7 @@ class Automata:
 
     invalid_state_str = "INVALID_STATE"
     init_marker = "__init_"
+    node_marker = "{node"
     # val can be numerical, uppercase (constant or macro), lowercase (parameter or function)
     # only numerical values should have units
     constraint_rule = re.compile(r"""
@@ -112,7 +113,7 @@ class Automata:
         for cursor, line in enumerate(self.__dot_lines):
             split_line = line.split()
 
-            if len(split_line) and split_line[0] == "{node":
+            if len(split_line) and split_line[0] == self.node_marker:
                 return cursor
 
         raise AutomataError("Could not find a beginning state")
@@ -127,9 +128,9 @@ class Automata:
                 continue
 
             if state == 0:
-                if line[0] == "{node":
+                if line[0] == self.node_marker:
                     state = 1
-            elif line[0] != "{node":
+            elif line[0] != self.node_marker:
                 break
         else:
             raise AutomataError("Could not find beginning event")
@@ -151,7 +152,7 @@ class Automata:
         # process nodes
         for line in islice(self.__dot_lines, cursor, None):
             split_line = line.split()
-            if not split_line or split_line[0] != "{node":
+            if not split_line or split_line[0] != self.node_marker:
                 break
 
             raw_state = split_line[-1]
-- 
2.53.0

[PATCH v3 17/19] rv/rvgen: enforce presence of initial state

[Wander Lairson Costa]

The __get_state_variables() method parses DOT files to identify the
automaton's initial state. If the input file lacks a node with the
required initialization prefix, the initial_state variable is referenced
before assignment, causing an UnboundLocalError or a generic error
during the state removal step.

Initialize the variable explicitly and validate that a start node was
found after parsing. Raise a descriptive AutomataError if the definition
is missing to improve debugging and ensure the automaton is valid.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/automata.py | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index fd2a4a0c3f6eb..ac765c9b2dece 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -145,6 +145,7 @@ class Automata:
         # wait for node declaration
         states = []
         final_states = []
+        initial_state = ""
 
         has_final_states = False
         cursor = self.__get_cursor_begin_states()
@@ -171,6 +172,9 @@ class Automata:
                     final_states.append(state)
                     has_final_states = True
 
+        if not initial_state:
+            raise AutomataError("The automaton doesn't have an initial state")
+
         states = sorted(set(states))
         states.remove(initial_state)
 
-- 
2.53.0

[PATCH v3 18/19] rv/rvgen: fix unbound loop variable warning

[Wander Lairson Costa]

Pyright static analysis reports a "possibly unbound variable" warning
for the loop variable `i` in the `abbreviate_atoms` function. The
variable is accessed after the inner loop terminates to slice the atom
string. While the loop logic currently ensures execution, the analyzer
flags the reliance on the loop variable persisting outside its scope.

Refactor the prefix length calculation into a nested `find_share_length`
helper function. This encapsulates the search logic and uses explicit
return statements, ensuring the length value is strictly defined. This
satisfies the type checker and improves code readability without
altering the runtime behavior.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/ltl2k.py | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index b6300c38154dc..b8ac584fe2504 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -44,13 +44,17 @@ def abbreviate_atoms(atoms: list[str]) -> list[str]:
         skip = ["is", "by", "or", "and"]
         return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip])
 
-    abbrs = []
-    for atom in atoms:
+    def find_share_length(atom: str) -> int:
         for i in range(len(atom), -1, -1):
             if sum(a.startswith(atom[:i]) for a in atoms) > 1:
-                break
-        share = atom[:i]
-        unique = atom[i:]
+                return i
+        return 0
+
+    abbrs = []
+    for atom in atoms:
+        share_len = find_share_length(atom)
+        share = atom[:share_len]
+        unique = atom[share_len:]
         abbrs.append((shorten(share) + shorten(unique)))
     return abbrs
 
-- 
2.53.0

[PATCH v3 19/19] rv/rvgen: fix _fill_states() return type annotation

[Wander Lairson Costa]

The _fill_states() method returns a list of strings, but the type
annotation incorrectly specified str. Update the annotation to
list[str] to match the actual return value.

Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
---
 tools/verification/rvgen/rvgen/ltl2k.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index b8ac584fe2504..81fd1f5ea5ea2 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py
@@ -75,7 +75,7 @@ class ltl2k(generator.Monitor):
         if not self.name:
             self.name = Path(file_path).stem
 
-    def _fill_states(self) -> str:
+    def _fill_states(self) -> list[str]:
         buf = [
             "enum ltl_buchi_state {",
         ]
-- 
2.53.0

Re: [PATCH v3 01/19] rv/rvgen: introduce AutomataError exception class

[Gabriele Monaco]

On Mon, 2026-02-23 at 13:17 -0300, Wander Lairson Costa wrote:
> Replace the generic except Exception block with a custom AutomataError
> class that inherits from Exception. This provides more precise exception
> handling for automata parsing and validation errors while avoiding
> overly broad exception catches that could mask programming errors like
> SyntaxError or TypeError.
> 
> The AutomataError class is raised when DOT file processing fails due to
> invalid format, I/O errors, or malformed automaton definitions. The
> main entry point catches this specific exception and provides a
> user-friendly error message to stderr before exiting.
> 
> Also, replace generic exceptions raising in HA and LTL with
> AutomataError.
> 
> Co-authored-by: Gabriele Monaco <gmonaco@redhat.com>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>

All good, thanks!

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

> ---
>  tools/verification/rvgen/__main__.py        |  6 ++---
>  tools/verification/rvgen/rvgen/automata.py  | 17 ++++++++++----
>  tools/verification/rvgen/rvgen/dot2c.py     |  4 ++--
>  tools/verification/rvgen/rvgen/dot2k.py     | 26 ++++++++++-----------
>  tools/verification/rvgen/rvgen/generator.py |  7 ++----
>  tools/verification/rvgen/rvgen/ltl2ba.py    |  9 +++----
>  tools/verification/rvgen/rvgen/ltl2k.py     |  8 +++++--
>  7 files changed, 43 insertions(+), 34 deletions(-)
> 
> diff --git a/tools/verification/rvgen/__main__.py
> b/tools/verification/rvgen/__main__.py
> index 9a5a9f08eae21..5a3f090ac3316 100644
> --- a/tools/verification/rvgen/__main__.py
> +++ b/tools/verification/rvgen/__main__.py
> @@ -13,6 +13,7 @@ if __name__ == '__main__':
>      from rvgen.generator import Monitor
>      from rvgen.container import Container
>      from rvgen.ltl2k import ltl2k
> +    from rvgen.automata import AutomataError
>      import argparse
>      import sys
>  
> @@ -55,9 +56,8 @@ if __name__ == '__main__':
>                  sys.exit(1)
>          else:
>              monitor = Container(vars(params))
> -    except Exception as e:
> -        print('Error: '+ str(e))
> -        print("Sorry : :-(")
> +    except AutomataError as e:
> +        print(f"There was an error processing {params.spec}: {e}",
> file=sys.stderr)
>          sys.exit(1)
>  
>      print("Writing the monitor into the directory %s" % monitor.name)
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 5c1c5597d839f..9cc452305a2aa 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -25,6 +25,13 @@ class _EventConstraintKey(_ConstraintKey, tuple):
>      def __new__(cls, state_id: int, event_id: int):
>          return super().__new__(cls, (state_id, event_id))
>  
> +class AutomataError(Exception):
> +    """Exception raised for errors in automata parsing and validation.
> +
> +    Raised when DOT file processing fails due to invalid format, I/O errors,
> +    or malformed automaton definitions.
> +    """
> +
>  class Automata:
>      """Automata class: Reads a dot file and part it as an automata.
>  
> @@ -72,11 +79,11 @@ class Automata:
>          basename = ntpath.basename(self.__dot_path)
>          if not basename.endswith(".dot") and not basename.endswith(".gv"):
>              print("not a dot file")
> -            raise Exception("not a dot file: %s" % self.__dot_path)
> +            raise AutomataError("not a dot file: %s" % self.__dot_path)
>  
>          model_name = ntpath.splitext(basename)[0]
>          if model_name.__len__() == 0:
> -            raise Exception("not a dot file: %s" % self.__dot_path)
> +            raise AutomataError("not a dot file: %s" % self.__dot_path)
>  
>          return model_name
>  
> @@ -85,8 +92,8 @@ class Automata:
>          dot_lines = []
>          try:
>              dot_file = open(self.__dot_path)
> -        except:
> -            raise Exception("Cannot open the file: %s" % self.__dot_path)
> +        except OSError as exc:
> +            raise AutomataError(exc.strerror) from exc
>  
>          dot_lines = dot_file.read().splitlines()
>          dot_file.close()
> @@ -95,7 +102,7 @@ class Automata:
>          line = dot_lines[cursor].split()
>  
>          if (line[0] != "digraph") and (line[1] != "state_automaton"):
> -            raise Exception("Not a valid .dot format: %s" % self.__dot_path)
> +            raise AutomataError("Not a valid .dot format: %s" %
> self.__dot_path)
>          else:
>              cursor += 1
>          return dot_lines
> diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> b/tools/verification/rvgen/rvgen/dot2c.py
> index f779d9528af3f..6878cc79e6f70 100644
> --- a/tools/verification/rvgen/rvgen/dot2c.py
> +++ b/tools/verification/rvgen/rvgen/dot2c.py
> @@ -13,7 +13,7 @@
>  # For further information, see:
>  #   Documentation/trace/rv/deterministic_automata.rst
>  
> -from .automata import Automata
> +from .automata import Automata, AutomataError
>  
>  class Dot2c(Automata):
>      enum_suffix = ""
> @@ -103,7 +103,7 @@ class Dot2c(Automata):
>              min_type = "unsigned int"
>  
>          if self.states.__len__() > 1000000:
> -            raise Exception("Too many states: %d" % self.states.__len__())
> +            raise AutomataError("Too many states: %d" %
> self.states.__len__())
>  
>          return min_type
>  
> diff --git a/tools/verification/rvgen/rvgen/dot2k.py
> b/tools/verification/rvgen/rvgen/dot2k.py
> index e7ba68a54c1f8..55222e38323f5 100644
> --- a/tools/verification/rvgen/rvgen/dot2k.py
> +++ b/tools/verification/rvgen/rvgen/dot2k.py
> @@ -11,7 +11,7 @@
>  from collections import deque
>  from .dot2c import Dot2c
>  from .generator import Monitor
> -from .automata import _EventConstraintKey, _StateConstraintKey
> +from .automata import _EventConstraintKey, _StateConstraintKey, AutomataError
>  
>  
>  class dot2k(Monitor, Dot2c):
> @@ -166,14 +166,14 @@ class da2k(dot2k):
>      def __init__(self, *args, **kwargs):
>          super().__init__(*args, **kwargs)
>          if self.is_hybrid_automata():
> -            raise ValueError("Detected hybrid automata, use the 'ha' class")
> +            raise AutomataError("Detected hybrid automata, use the 'ha'
> class")
>  
>  class ha2k(dot2k):
>      """Hybrid automata only"""
>      def __init__(self, *args, **kwargs):
>          super().__init__(*args, **kwargs)
>          if not self.is_hybrid_automata():
> -            raise ValueError("Detected deterministic automata, use the 'da'
> class")
> +            raise AutomataError("Detected deterministic automata, use the
> 'da' class")
>          self.trace_h = self._read_template_file("trace_hybrid.h")
>          self.__parse_constraints()
>  
> @@ -266,22 +266,22 @@ class ha2k(dot2k):
>          # state constraints are only used for expirations (e.g. clk<N)
>          if self.is_event_constraint(key):
>              if not rule and not reset:
> -                raise ValueError("Unrecognised event constraint "
> -                                
> f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
> +                raise AutomataError("Unrecognised event constraint "
> +                                   
> f"({self.states[key[0]]}/{self.events[key[1]]}: {constr})")
>              if rule and (rule["env"] in self.env_types and
>                           rule["env"] not in self.env_stored):
> -                raise ValueError("Clocks in hybrid automata always require a
> storage"
> -                                 f" ({rule["env"]})")
> +                raise AutomataError("Clocks in hybrid automata always require
> a storage"
> +                                    f" ({rule["env"]})")
>          else:
>              if not rule:
> -                raise ValueError("Unrecognised state constraint "
> -                                 f"({self.states[key]}: {constr})")
> +                raise AutomataError("Unrecognised state constraint "
> +                                    f"({self.states[key]}: {constr})")
>              if rule["env"] not in self.env_stored:
> -                raise ValueError("State constraints always require a storage
> "
> -                                 f"({rule["env"]})")
> +                raise AutomataError("State constraints always require a
> storage "
> +                                    f"({rule["env"]})")
>              if rule["op"] not in ["<", "<="]:
> -                raise ValueError("State constraints must be clock expirations
> like"
> -                                 f" clk<N ({rule.string})")
> +                raise AutomataError("State constraints must be clock
> expirations like"
> +                                    f" clk<N ({rule.string})")
>  
>      def __parse_constraints(self) -> None:
>          self.guards: dict[_EventConstraintKey, str] = {}
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index 5eac12e110dce..571093a92bdc8 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -51,10 +51,7 @@ class RVGenerator:
>          raise FileNotFoundError("Could not find the rv directory, do you have
> the kernel source installed?")
>  
>      def _read_file(self, path):
> -        try:
> -            fd = open(path, 'r')
> -        except OSError:
> -            raise Exception("Cannot open the file: %s" % path)
> +        fd = open(path, 'r')
>  
>          content = fd.read()
>  
> @@ -65,7 +62,7 @@ class RVGenerator:
>          try:
>              path = os.path.join(self.abs_template_dir, file)
>              return self._read_file(path)
> -        except Exception:
> +        except OSError:
>              # Specific template file not found. Try the generic template file
> in the template/
>              # directory, which is one level up
>              path = os.path.join(self.abs_template_dir, "..", file)
> diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py
> b/tools/verification/rvgen/rvgen/ltl2ba.py
> index f14e6760ac3db..f9855dfa3bc1c 100644
> --- a/tools/verification/rvgen/rvgen/ltl2ba.py
> +++ b/tools/verification/rvgen/rvgen/ltl2ba.py
> @@ -9,6 +9,7 @@
>  
>  from ply.lex import lex
>  from ply.yacc import yacc
> +from .automata import AutomataError
>  
>  # Grammar:
>  # 	ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
> @@ -62,7 +63,7 @@ t_ignore_COMMENT = r'\#.*'
>  t_ignore = ' \t\n'
>  
>  def t_error(t):
> -    raise ValueError(f"Illegal character '{t.value[0]}'")
> +    raise AutomataError(f"Illegal character '{t.value[0]}'")
>  
>  lexer = lex()
>  
> @@ -487,7 +488,7 @@ def p_unop(p):
>      elif p[1] == "not":
>          op = NotOp(p[2])
>      else:
> -        raise ValueError(f"Invalid unary operator {p[1]}")
> +        raise AutomataError(f"Invalid unary operator {p[1]}")
>  
>      p[0] = ASTNode(op)
>  
> @@ -507,7 +508,7 @@ def p_binop(p):
>      elif p[2] == "imply":
>          op = ImplyOp(p[1], p[3])
>      else:
> -        raise ValueError(f"Invalid binary operator {p[2]}")
> +        raise AutomataError(f"Invalid binary operator {p[2]}")
>  
>      p[0] = ASTNode(op)
>  
> @@ -526,7 +527,7 @@ def parse_ltl(s: str) -> ASTNode:
>              subexpr[assign[0]] = assign[1]
>  
>      if rule is None:
> -        raise ValueError("Please define your specification in the \"RULE =
> <LTL spec>\" format")
> +        raise AutomataError("Please define your specification in the \"RULE =
> <LTL spec>\" format")
>  
>      for node in rule:
>          if not isinstance(node.op, Variable):
> diff --git a/tools/verification/rvgen/rvgen/ltl2k.py
> b/tools/verification/rvgen/rvgen/ltl2k.py
> index b075f98d50c47..08ad245462e7d 100644
> --- a/tools/verification/rvgen/rvgen/ltl2k.py
> +++ b/tools/verification/rvgen/rvgen/ltl2k.py
> @@ -4,6 +4,7 @@
>  from pathlib import Path
>  from . import generator
>  from . import ltl2ba
> +from .automata import AutomataError
>  
>  COLUMN_LIMIT = 100
>  
> @@ -60,8 +61,11 @@ class ltl2k(generator.Monitor):
>          if MonitorType != "per_task":
>              raise NotImplementedError("Only per_task monitor is supported for
> LTL")
>          super().__init__(extra_params)
> -        with open(file_path) as f:
> -            self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
> +        try:
> +            with open(file_path) as f:
> +                self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read())
> +        except OSError as exc:
> +            raise AutomataError(exc.strerror) from exc
>          self.atoms_abbr = abbreviate_atoms(self.atoms)
>          self.name = extra_params.get("model_name")
>          if not self.name:

Re: [PATCH v3 07/19] rv/rvgen: fix typos in automata and generator docstring and comments

[Gabriele Monaco]

On Mon, 2026-02-23 at 13:17 -0300, Wander Lairson Costa wrote:
> -                # when a transition has more than one lables, they are like
> this
> +                # when a transition has more than one labels, they are like
> this
>                  # "local_irq_enable\nhw_local_irq_enable_n"
>                  # so split them.
>  

Missing one little thing:

s/labels/label/

I'm going to apply it directly on my tree so you don't need to send a V4 just
for this.

Thanks,
Gabriele

> diff --git a/tools/verification/rvgen/rvgen/dot2c.py
> b/tools/verification/rvgen/rvgen/dot2c.py
> index fa44795adef46..9255cc2153a31 100644
> --- a/tools/verification/rvgen/rvgen/dot2c.py
> +++ b/tools/verification/rvgen/rvgen/dot2c.py
> @@ -3,7 +3,7 @@
>  #
>  # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira
> <bristot@kernel.org>
>  #
> -# dot2c: parse an automata in dot file digraph format into a C
> +# dot2c: parse an automaton in dot file digraph format into a C
>  #
>  # This program was written in the development of this paper:
>  #  de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
> diff --git a/tools/verification/rvgen/rvgen/dot2k.py
> b/tools/verification/rvgen/rvgen/dot2k.py
> index 47af9f104a829..aedc2a7799b32 100644
> --- a/tools/verification/rvgen/rvgen/dot2k.py
> +++ b/tools/verification/rvgen/rvgen/dot2k.py
> @@ -167,14 +167,14 @@ class da2k(dot2k):
>      def __init__(self, *args, **kwargs):
>          super().__init__(*args, **kwargs)
>          if self.is_hybrid_automata():
> -            raise AutomataError("Detected hybrid automata, use the 'ha'
> class")
> +            raise AutomataError("Detected hybrid automaton, use the 'ha'
> class")
>  
>  class ha2k(dot2k):
>      """Hybrid automata only"""
>      def __init__(self, *args, **kwargs):
>          super().__init__(*args, **kwargs)
>          if not self.is_hybrid_automata():
> -            raise AutomataError("Detected deterministic automata, use the
> 'da' class")
> +            raise AutomataError("Detected deterministic automaton, use the
> 'da' class")
>          self.trace_h = self._read_template_file("trace_hybrid.h")
>          self.__parse_constraints()
>  
> diff --git a/tools/verification/rvgen/rvgen/generator.py
> b/tools/verification/rvgen/rvgen/generator.py
> index d932e96dd66d3..988ccdc27fa37 100644
> --- a/tools/verification/rvgen/rvgen/generator.py
> +++ b/tools/verification/rvgen/rvgen/generator.py
> @@ -3,7 +3,7 @@
>  #
>  # Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira
> <bristot@kernel.org>
>  #
> -# Abtract class for generating kernel runtime verification monitors from
> specification file
> +# Abstract class for generating kernel runtime verification monitors from
> specification file
>  
>  import platform
>  import os