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

[heath]

Thanks, Gabriele! Really appreciate you taking the patch and the 
clarification on LLM disclosures.

One small question- this work is part of MathGraph, developed at 
Metalogic Labs. Is there a conventional way to acknowledge that 
affiliation in the commit? No worries at all if not — I wouldn’t want to 
complicate or delay the patch.

Thanks again!

Heath Sanchez
Metalogic Labs | MathGraph
https://mathgraph.org

On 2026-10-16 03:55, Gabriele Monaco wrote:
> On Tue, 2026-10-13 at 15:51 -0400, heath@xxxxxxxxxxxxx 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@xxxxxxxxxxxxx>
>
> 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";
> > +	}
> > +}