[PATCH] verification/rvgen: reject ambiguous state/event transitions

[heath@mathgraph.org]

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 <heath@mathgraph.org>
---
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";
+	}
+}