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

[Gabriele Monaco <gmonaco@redhat.com>]

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

Hi Heath,

you may find more information in [1], as far as I know, the affiliation is clear
from your email in the signoff.
Often people using personal emails or kernel.org accounts specify their
affiliation in parenthesis.

In short, you either do the following in the signoff:

1. John Doe <jdoe@acme.com>

or

2. John Doe (ACME) <john@doe.org>

your case falls in 1. (@mathgraph.org) I don't think you need extra steps.


Gabriele


[1] - https://www.kernel.org/doc/html/latest/process/submitting-patches.html

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