Re: [RFC PATCH 07/12] verification/rvgen: Add golden and spec folders for tests

From: Nam Cao

Date: Mon May 04 2026 - 03:48:47 EST


Gabriele Monaco <gmonaco@xxxxxxxxxx> writes:
> diff --git a/tools/verification/rvgen/tests/specs/test_da2.dot b/tools/verification/rvgen/tests/specs/test_da2.dot
> new file mode 100644
> index 000000000000..bfee6e535cf7
> --- /dev/null
> +++ b/tools/verification/rvgen/tests/specs/test_da2.dot
> @@ -0,0 +1,18 @@
> +digraph state_automaton {
> + {node [shape = circle] "state_b"};
> + {node [shape = circle] "state_c"};
> + {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_b" [ label = "event_1" ];
> + "state_a" -> "state_c" [ label = "event_2" ];
> + "state_b" [label = "state_b"];
> + "state_b" -> "state_a" [ label = "event_2" ];
> + "state_b" -> "state_c" [ label = "event_3" ];
> + { rank = min ;
> + "__init_state_a";
> + "state_a";
> + }
> +}

I am working on converting rvgen to use Lark, a parsing library:
https://github.com/lark-parser/lark

This test case breaks the current version of the new script, because
state_c has no label while the script expects one - the script read the
state's name from the label.

We should define if the label or the node's name is our state's
name. For example, if we have:

"state_c" [label = "state_d"];

Will the state's name be state_c or state_d? Or should that be a parsing error?

I propose using the label if one is provided, otherwise using the node's
name. So

"state_c" [label = "state_d"];

means the state's name is "state_d". But without that statement, the
state's name is "state_c".

What do you think?

(just FYI, my work-in-progress: https://github.com/covanam/linux/commits/rv-lark/)

Nam