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

[Gabriele Monaco <gmonaco@redhat.com>]

Hi Heath,

thanks for your contribution! Looks good to me.
I have a couple of minor nits.

On Fri, 2026-10-09 at 16:17 -0400, heath@mathgraph.org wrote:
> 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

I'm not sure this statement above adds much value and the evidence is good but I
wouldn't include it in the commit message. If you want to add more details to a
single patch (without a cover letter), you can append them right after the ---
so they don't get included in the git history.

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

Here you may want to use "Traceback (most recent call last)" for the negative
match: more consistent and robust.

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

The code for DA and HA is shared, I'm not sure we really need both test cases.
I'd keep only the DA, we're already not testing every single error condition and
the test is starting to take longer and longer.
What do you think?

Thanks,
Gabriele


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