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

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

[heath]

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

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

[Gabriele Monaco]

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

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

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

[Gabriele Monaco]

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