On Wed, 2026-02-04 at 11:42 -0300, Wander Lairson Costa wrote:
> The __get_state_variables() method parses DOT files to identify the
> automaton's initial state. If the input file lacks a node with the
> required initialization prefix, the initial_state variable is referenced
> before assignment, causing an UnboundLocalError or a generic error
> during the state removal step.
>
> Initialize the variable explicitly and validate that a start node was
> found after parsing. Raise a descriptive AutomataError if the definition
> is missing to improve debugging and ensure the automaton is valid.
>
> Signed-off-by: Wander Lairson Costa <wander@redhat.com>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> ---
> tools/verification/rvgen/rvgen/automata.py | 4 ++++
> 1 file changed, 4 insertions(+)
>
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 270a3d0bf4ce7..cf82f04dbc661 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -105,6 +105,7 @@ class Automata:
> # wait for node declaration
> states = []
> final_states = []
> + initial_state = ""
>
> has_final_states = False
> cursor = self.__get_cursor_begin_states()
> @@ -131,6 +132,9 @@ class Automata:
> final_states.append(state)
> has_final_states = True
>
> + if not initial_state:
> + raise AutomataError("The automaton doesn't have an initial
> state")
> +
> states = sorted(set(states))
> states.remove(initial_state)
>