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

[Gabriele Monaco <gmonaco@redhat.com>]

On Tue, 2026-10-13 at 15:51 -0400, heath@mathgraph.org wrote:
> 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>

Thanks for the quick V2. I'm going to take this.

As a side note, I just read ([1], subscription required) that the Maintainers
decided at the 2026 Summit that models used and other LLM details are no longer
to be included in the changelog.

You don't need to send a V3, I'm trimming that paragraph. Anyway this kind of
transparency is largely appreciated, so feel free to include it after the --- on
your next contributions.

Thanks,
Gabriele

[1] - https://lwn.net/Articles/1099594

> ---
> 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";
> +	}
> +}