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 <[email protected]>
---
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";
+ }
+}
