lwn.git/tools/verification/rvgen/main.py, branch master

rv/rvgen: make monitor arguments required in rvgen

2026-04-01T08:16:19+00:00

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 Reviewed-by: Gabriele Monaco Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260223162407.147003-15-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: replace % string formatting with f-strings

2026-03-31T14:47:51+00:00

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 Reviewed-by: Nam Cao Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260223162407.147003-4-wander@redhat.com Signed-off-by: Gabriele Monaco

rv/rvgen: introduce AutomataError exception class

2026-03-31T14:47:50+00:00

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 Signed-off-by: Wander Lairson Costa Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260223162407.147003-2-wander@redhat.com Signed-off-by: Gabriele Monaco

verification/rvgen: Add support for Hybrid Automata

2026-03-31T14:47:16+00:00

Add the possibility to parse dot files as hybrid automata and generate the necessary code from rvgen. Hybrid automata are very similar to deterministic ones and most functionality is shared, the dot files include also constraints together with event names (separated by ;) and state names (separated by \n). The tool can now generate the appropriate code to validate constraints at runtime according to the dot specification. Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260330111010.153663-5-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

verification/rvgen: Add support for linear temporal logic

2025-07-24T14:42:47+00:00

Add support for generating RV monitors from linear temporal logic, similar to the generation of deterministic automaton monitors. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Link: https://lore.kernel.org/f3c63b363ff9c5af3302ba2b5d92a26a98700eaf.1751634289.git.namcao@linutronix.de Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

verification/rvgen: Restructure the classes to prepare for LTL inclusion

2025-07-24T14:42:46+00:00

Both container generation and DA monitor generation is implemented in the class dot2k. That requires some ugly "if is_container ... else ...". If linear temporal logic support is added at the current state, the "if else" chain is longer and uglier. Furthermore, container generation is irrevelant to .dot files. It is therefore illogical to be implemented in class "dot2k". Clean it up, restructure the dot2k class into the following class hierarchy: (RVGenerator) /\ / \ / \ / \ / \ (Container) (Monitor) /\ / \ / \ / \ (dot2k) [ltl2k] <- intended This allows a simple and clean integration of LTL. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/692137a581ba6bee7a64d37fb7173ae137c47bbd.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

verification/dot2k: Prepare the frontend for LTL inclusion

2025-07-24T14:42:46+00:00

The dot2k tool has some code that can be reused for linear temporal logic monitor. Prepare its frontend for LTL inclusion: 1. Rename to be generic: rvgen 2. Replace the parameter --dot with 2 parameters: --class: to specific the monitor class, can be 'da' or 'ltl' --spec: the monitor specification file, .dot file for DA, and .ltl file for LTL The old command: python3 dot2/dot2k monitor -d wip.dot -t per_cpu is equivalent to the new commands: python3 rvgen monitor -c da -s wip.dot -t per_cpu Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

lwn.git/tools/verification/rvgen/__main__.py, branch master

rv/rvgen: make monitor arguments required in rvgen

rv/rvgen: replace % string formatting with f-strings

rv/rvgen: introduce AutomataError exception class

verification/rvgen: Add support for Hybrid Automata

verification/rvgen: Add support for linear temporal logic

verification/rvgen: Restructure the classes to prepare for LTL inclusion

verification/dot2k: Prepare the frontend for LTL inclusion

lwn.git/tools/verification/rvgen/main.py, branch master