[PATCH] verification/rvgen: reject ambiguous state/event transitions
DORMANTno replies
From: <hidden>
Date: 2026-10-09 20:59:25
Also in:
lkml
Subsystem:
runtime verification (rv), the rest · Maintainers:
Steven Rostedt, Gabriele Monaco, Linus Torvalds
The rvgen generator builds a transition function indexed by source state and event. If a DOT specification contains different destinations for one key, the generator silently chooses one. Parsed transitions are set-derived, so the choice can vary across Python hash seeds for an unchanged specification. Reject duplicate (state, event) keys after sorting the parsed transitions, before synthesizing a monitor. This uses constant auxiliary memory and does not depend on the INVALID_STATE sentinel. Both deterministic and hybrid monitors require a unique destination for each state/event pair. Add deterministic and hybrid negative fixtures. On the pinned Linux tree, the original rvgen suite passes 30/30 tests and the patched suite passes 32/32; both malformed specifications are rejected across 64 seeded processes. Fifteen existing models retain identical transition matrices. Evidence: https://github.com/metalogiclabs/mathgraph/actions/runs/37983741146 OpenAI GPT-6 assisted in identifying the issue, producing and refining the code and tests, and drafting this submission. I reviewed the patch and accept responsibility for the contribution. Fixes: cad252db78a9 ("verification/rvgen: Switch __create_matrix() to Lark") Assisted-by: LLM Signed-off-by: Heath Sanchez <redacted> ---
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index fd37ce3..1f9a56a 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py@@ -418,6 +418,13 @@ class Automata: transitions.append(Transition(src, dst, event, reset, rule)) transitions.sort(key=lambda t : (t.src, t.event)) + previous_key = None + for transition in transitions: + key = (transition.src, transition.event) + if key == previous_key: + raise AutomataError( + f"Duplicate transition for event {transition.event} in state {transition.src}") + previous_key = key return transitions def __parse_states(self):
diff --git a/tools/verification/rvgen/tests/rvgen_monitor.t b/tools/verification/rvgen/tests/rvgen_monitor.t
index 5f25626..6209c00 100644
--- a/tools/verification/rvgen/tests/rvgen_monitor.t
+++ b/tools/verification/rvgen/tests/rvgen_monitor.t@@ -84,4 +84,14 @@ check "invalid ltl file syntax" \ "$RVGEN monitor -c ltl -s tests/specs/test_invalid.ltl -t per_task" 1 \ "No terminal matches 'i'" "Traceback (most recent call last)" +# Only one transition per source state/event is representable in rvgen's +# generated table, even if one of the transitions has a hybrid guard. +check "reject conflicting deterministic automaton transitions" \ + "$RVGEN monitor -c da -s tests/specs/test_nondeterministic_da.dot -t per_cpu" 1 \ + "Duplicate transition for event event_2 in state state_a" "Traceback" + +check "reject conflicting guarded hybrid transitions" \ + "$RVGEN monitor -c ha -s tests/specs/test_nondeterministic_ha.dot -t per_task" 1 \ + "Duplicate transition for event event2 in state S2" "Traceback" + test_end
diff --git a/tools/verification/rvgen/tests/specs/test_nondeterministic_da.dot b/tools/verification/rvgen/tests/specs/test_nondeterministic_da.dot
new file mode 100644
index 0000000..1b63b5d
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_nondeterministic_da.dot@@ -0,0 +1,16 @@ +digraph state_automaton { + {node [shape = circle] "state_b"}; + {node [shape = plaintext, style=invis, label=""] "__init_state_a"}; + {node [shape = doublecircle] "state_a"}; + {node [shape = circle] "state_a"}; + "__init_state_a" -> "state_a"; + "state_a" [label = "state_a"]; + "state_a" -> "state_a" [ label = "event_2" ]; + "state_a" -> "state_b" [ label = "event_2" ]; + "state_b" [label = "state_b"]; + "state_b" -> "state_a" [ label = "event_2" ]; + { rank = min ; + "__init_state_a"; + "state_a"; + } +}
diff --git a/tools/verification/rvgen/tests/specs/test_nondeterministic_ha.dot b/tools/verification/rvgen/tests/specs/test_nondeterministic_ha.dot
new file mode 100644
index 0000000..d21b91b
--- /dev/null
+++ b/tools/verification/rvgen/tests/specs/test_nondeterministic_ha.dot@@ -0,0 +1,27 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = circle] "S1"}; + {node [shape = plaintext, style=invis, label=""] "__init_S0"}; + {node [shape = doublecircle] "S0"}; + {node [shape = circle] "S0"}; + {node [shape = circle] "S2"}; + {node [shape = circle] "S3"}; + "__init_S0" -> "S0"; + "S0" [label = "S0\nclk < bar_ns()", color = green3]; + "S1" [label = "S1"]; + "S2" [label = "S2\nclk < BAR_NS()"]; + "S3" [label = "S3"]; + "S1" -> "S0" [ label = "event0;reset(clk)" ]; + "S0" -> "S1" [ label = "event1;reset(clk)" ]; + "S0" -> "S0" [ label = "event0;reset(clk)" ]; + "S1" -> "S2" [ label = "event2;env1 == 0;reset(clk)" ]; + "S2" -> "S3" [ label = "event2" ]; + "S2" -> "S2" [ label = "event2;clk < foo_ns" ]; + "S3" -> "S0" [ label = "event0;clk < FOO_NS && env2 == 0" ]; + "S3" -> "S1" [ label = "event1;clk < 5us && env1 == 1;reset(clk)" ]; + { rank = min ; + "__init_S0"; + "S0"; + } +}