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

[heath@mathgraph.org]

The rvgen generator builds a transition table indexed by source state
and event. A DOT specification with different destinations for the same
key is currently accepted, and the selected destination depends on the
iteration order of parsed transitions.

Reject duplicate state/event keys after sorting the transitions, before
generating the monitor. This prevents silently selecting an arbitrary
destination without changing valid automata.

OpenAI GPT-6 assisted in finding the issue, developing the fix and 
tests,
and drafting the changelog. I reviewed the changes and take 
responsibility
for this contribution.

Fixes: cad252db78a9 ("verification/rvgen: Switch __create_matrix() to 
Lark")
Assisted-by: LLM
Signed-off-by: Heath Sanchez <heath@mathgraph.org>
---
Changes in v2:
- Drop the redundant hybrid-automaton regression fixture and test.
- Match the full traceback prefix in the negative assertion.
- Move detailed qualification results outside the permanent changelog.

Verification: original rvgen suite 30/30; revised suite 31/31;
64 deterministic/hybrid hash-seed replays rejected malformed models.
https://github.com/metalogiclabs/mathgraph/actions/runs/38452477359

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..8d635fc 100644
--- a/tools/verification/rvgen/tests/rvgen_monitor.t
+++ b/tools/verification/rvgen/tests/rvgen_monitor.t
@@ -84,4 +84,9 @@ 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)"

+# Reject ambiguous source state/event pairs.
+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 
(most recent call last)"
+
  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";
+	}
+}