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

[heath@mathgraph.org]

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