Initialize initial_state to None and validate its assignment after
parsing DOT file state nodes. The previous implementation left
initial_state uninitialized if the DOT file contained no state with
the init_marker prefix, which would cause an UnboundLocalError when
the code attempted to use the variable at the end of the function.
This bug was identified by pyright static type checker, which correctly
flagged that initial_state could be referenced before assignment. The
fix adds proper initialization and validation, raising a AutomataError if
no initial state marker is found in the automaton definition. This
ensures that malformed DOT files missing an initial state are caught
early with a clear error message rather than causing cryptic runtime
exceptions.
The change also includes minor code formatting improvements to comply
with PEP 8 style guidelines, including consistent use of double quotes
for string literals and proper line length formatting for improved
readability.
Signed-off-by: Wander Lairson Costa <wander@redhat.com>
---
tools/verification/rvgen/rvgen/automata.py | 26 +++++++++++++++-------
1 file changed, 18 insertions(+), 8 deletions(-)
diff --git a/tools/verification/rvgen/rvgen/automata.py b/tools/verification/rvgen/rvgen/automata.py
index 8548265955570..083d0f5cfb773 100644
--- a/tools/verification/rvgen/rvgen/automata.py
+++ b/tools/verification/rvgen/rvgen/automata.py
@@ -10,6 +10,7 @@
import ntpath
+
class AutomataError(OSError):
"""Exception raised for errors in automata parsing and validation.
@@ -17,6 +18,7 @@ class AutomataError(OSError):
or malformed automaton definitions.
"""
+
class Automata:
"""Automata class: Reads a dot file and parses it as an automata.
@@ -31,7 +33,9 @@ class Automata:
self.__dot_path = file_path
self.name = model_name or self.__get_model_name()
self.__dot_lines = self.__open_dot()
- self.states, self.initial_state, self.final_states = self.__get_state_variables()
+ self.states, self.initial_state, self.final_states = (
+ self.__get_state_variables()
+ )
self.events = self.__get_event_variables()
self.function = self.__create_matrix()
self.events_start, self.events_start_run = self.__store_init_events()
@@ -86,6 +90,7 @@ class Automata:
# wait for node declaration
states = []
final_states = []
+ initial_state = None
has_final_states = False
cursor = self.__get_cursor_begin_states()
@@ -96,9 +101,9 @@ class Automata:
raw_state = line[-1]
# "enabled_fired"}; -> enabled_fired
- state = raw_state.replace('"', '').replace('};', '').replace(',', '_')
+ state = raw_state.replace('"', "").replace("};", "").replace(",", "_")
if state.startswith(self.init_marker):
- initial_state = state[len(self.init_marker):]
+ initial_state = state[len(self.init_marker) :]
else:
states.append(state)
if "doublecircle" in self.__dot_lines[cursor]:
@@ -111,6 +116,9 @@ class Automata:
cursor += 1
+ if initial_state is None:
+ raise AutomataError("The automaton doesn't have a initial state")
+
states = sorted(set(states))
# Insert the initial state at the beginning of the states
@@ -132,7 +140,7 @@ class Automata:
# ------------ event is here ------------^^^^^
if self.__dot_lines[cursor].split()[1] == "->":
line = self.__dot_lines[cursor].split()
- event = line[-2].replace('"', '')
+ event = line[-2].replace('"', "")
# when a transition has more than one labels, they are like this
# "local_irq_enable\nhw_local_irq_enable_n"
@@ -162,7 +170,9 @@ class Automata:
nr_state += 1
# declare the matrix....
- matrix = [[self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)]
+ matrix = [
+ [self.invalid_state_str for x in range(nr_event)] for y in range(nr_state)
+ ]
# and we are back! Let's fill the matrix
cursor = self.__get_cursor_begin_events()
@@ -170,9 +180,9 @@ class Automata:
while self.__dot_lines[cursor].lstrip()[0] == '"':
if self.__dot_lines[cursor].split()[1] == "->":
line = self.__dot_lines[cursor].split()
- origin_state = line[0].replace('"', '').replace(',', '_')
- dest_state = line[2].replace('"', '').replace(',', '_')
- possible_events = line[-2].replace('"', '').replace("\\n", " ")
+ origin_state = line[0].replace('"', "").replace(",", "_")
+ dest_state = line[2].replace('"', "").replace(",", "_")
+ possible_events = line[-2].replace('"', "").replace("\\n", " ")
for event in possible_events.split():
matrix[states_dict[origin_state]][events_dict[event]] = dest_state
cursor += 1
--
2.52.0On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
[...]
> diff --git a/tools/verification/rvgen/rvgen/automata.py
> b/tools/verification/rvgen/rvgen/automata.py
> index 8548265955570..083d0f5cfb773 100644
> --- a/tools/verification/rvgen/rvgen/automata.py
> +++ b/tools/verification/rvgen/rvgen/automata.py
> @@ -10,6 +10,7 @@
>
> import ntpath
>
> +
> class AutomataError(OSError):
> """Exception raised for errors in automata parsing and validation.
>
> @@ -17,6 +18,7 @@ class AutomataError(OSError):
> or malformed automaton definitions.
> """
>
> +
I believe these newlines were added automatically by some tools, not sure if we
really want them but they don't belong in this patch (since 1/26 added this
class).
> class Automata:
> """Automata class: Reads a dot file and parses it as an automata.
>
> @@ -31,7 +33,9 @@ class Automata:
> self.__dot_path = file_path
> self.name = model_name or self.__get_model_name()
> self.__dot_lines = self.__open_dot()
> - self.states, self.initial_state, self.final_states =
> self.__get_state_variables()
> + self.states, self.initial_state, self.final_states = (
> + self.__get_state_variables()
> + )
There is no strict 80 character limit for python code and I personally find this
less readable. Is this again what the tool suggested?
> self.events = self.__get_event_variables()
> self.function = self.__create_matrix()
> self.events_start, self.events_start_run = self.__store_init_events()
> @@ -86,6 +90,7 @@ class Automata:
> # wait for node declaration
> states = []
> final_states = []
> + initial_state = None
>
> has_final_states = False
> cursor = self.__get_cursor_begin_states()
> @@ -96,9 +101,9 @@ class Automata:
> raw_state = line[-1]
>
> # "enabled_fired"}; -> enabled_fired
> - state = raw_state.replace('"', '').replace('};', '').replace(',',
> '_')
> + state = raw_state.replace('"', "").replace("};", "").replace(",",
> "_")
Ok this change is good.
> if state.startswith(self.init_marker):
> - initial_state = state[len(self.init_marker):]
> + initial_state = state[len(self.init_marker) :]
You fixed spacing in 12/26. We could either keep move this change there or just
merge that patch with others touching the same files.
> else:
> states.append(state)
> if "doublecircle" in self.__dot_lines[cursor]:
> @@ -111,6 +116,9 @@ class Automata:
>
> cursor += 1
>
> + if initial_state is None:
> + raise AutomataError("The automaton doesn't have a initial state")
> +
Yeah that's needed.
> states = sorted(set(states))
>
> # Insert the initial state at the beginning of the states
> @@ -132,7 +140,7 @@ class Automata:
> # ------------ event is here ------------^^^^^
> if self.__dot_lines[cursor].split()[1] == "->":
> line = self.__dot_lines[cursor].split()
> - event = line[-2].replace('"', '')
> + event = line[-2].replace('"', "")
>
> # when a transition has more than one labels, they are like
> this
> # "local_irq_enable\nhw_local_irq_enable_n"
> @@ -162,7 +170,9 @@ class Automata:
> nr_state += 1
>
> # declare the matrix....
> - matrix = [[self.invalid_state_str for x in range(nr_event)] for y in
> range(nr_state)]
> + matrix = [
> + [self.invalid_state_str for x in range(nr_event)] for y in
> range(nr_state)
> + ]
>
> # and we are back! Let's fill the matrix
> cursor = self.__get_cursor_begin_events()
> @@ -170,9 +180,9 @@ class Automata:
> while self.__dot_lines[cursor].lstrip()[0] == '"':
> if self.__dot_lines[cursor].split()[1] == "->":
> line = self.__dot_lines[cursor].split()
> - origin_state = line[0].replace('"', '').replace(',', '_')
> - dest_state = line[2].replace('"', '').replace(',', '_')
> - possible_events = line[-2].replace('"', '').replace("\\n", "
> ")
> + origin_state = line[0].replace('"', "").replace(",", "_")
> + dest_state = line[2].replace('"', "").replace(",", "_")
> + possible_events = line[-2].replace('"', "").replace("\\n", "
> ")
All in all looks good, thanks.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> for event in possible_events.split():
> matrix[states_dict[origin_state]][events_dict[event]] =
> dest_state
> cursor += 1
On Tue, Jan 20, 2026 at 09:21:01AM +0100, Gabriele Monaco wrote:
> On Mon, 2026-01-19 at 17:45 -0300, Wander Lairson Costa wrote:
>
>
> [...]
> > diff --git a/tools/verification/rvgen/rvgen/automata.py
> > b/tools/verification/rvgen/rvgen/automata.py
> > index 8548265955570..083d0f5cfb773 100644
> > --- a/tools/verification/rvgen/rvgen/automata.py
> > +++ b/tools/verification/rvgen/rvgen/automata.py
> > @@ -10,6 +10,7 @@
> >
> > import ntpath
> >
> > +
> > class AutomataError(OSError):
> > """Exception raised for errors in automata parsing and validation.
> >
> > @@ -17,6 +18,7 @@ class AutomataError(OSError):
> > or malformed automaton definitions.
> > """
> >
> > +
>
> I believe these newlines were added automatically by some tools, not sure if we
> really want them but they don't belong in this patch (since 1/26 added this
> class).
>
There are python formatting tools that put 2 lines after a type
definition. Anyway, I can remove it in v2.
> > class Automata:
> > """Automata class: Reads a dot file and parses it as an automata.
> >
> > @@ -31,7 +33,9 @@ class Automata:
> > self.__dot_path = file_path
> > self.name = model_name or self.__get_model_name()
> > self.__dot_lines = self.__open_dot()
> > - self.states, self.initial_state, self.final_states =
> > self.__get_state_variables()
> > + self.states, self.initial_state, self.final_states = (
> > + self.__get_state_variables()
> > + )
>
> There is no strict 80 character limit for python code and I personally find this
> less readable. Is this again what the tool suggested?
>
In general, 100 lines is assumed the to a good limit. Anyway, this is
minor and I can remove the change in v2 if desired.
> > self.events = self.__get_event_variables()
> > self.function = self.__create_matrix()
> > self.events_start, self.events_start_run = self.__store_init_events()
> > @@ -86,6 +90,7 @@ class Automata:
> > # wait for node declaration
> > states = []
> > final_states = []
> > + initial_state = None
> >
> > has_final_states = False
> > cursor = self.__get_cursor_begin_states()
> > @@ -96,9 +101,9 @@ class Automata:
> > raw_state = line[-1]
> >
> > # "enabled_fired"}; -> enabled_fired
> > - state = raw_state.replace('"', '').replace('};', '').replace(',',
> > '_')
> > + state = raw_state.replace('"', "").replace("};", "").replace(",",
> > "_")
>
> Ok this change is good.
>
> > if state.startswith(self.init_marker):
> > - initial_state = state[len(self.init_marker):]
> > + initial_state = state[len(self.init_marker) :]
>
> You fixed spacing in 12/26. We could either keep move this change there or just
> merge that patch with others touching the same files.
>
Np, I can move this change to there.
> > else:
> > states.append(state)
> > if "doublecircle" in self.__dot_lines[cursor]:
> > @@ -111,6 +116,9 @@ class Automata:
> >
> > cursor += 1
> >
> > + if initial_state is None:
> > + raise AutomataError("The automaton doesn't have a initial state")
> > +
>
> Yeah that's needed.
>
> > states = sorted(set(states))
> >
> > # Insert the initial state at the beginning of the states
> > @@ -132,7 +140,7 @@ class Automata:
> > # ------------ event is here ------------^^^^^
> > if self.__dot_lines[cursor].split()[1] == "->":
> > line = self.__dot_lines[cursor].split()
> > - event = line[-2].replace('"', '')
> > + event = line[-2].replace('"', "")
> >
> > # when a transition has more than one labels, they are like
> > this
> > # "local_irq_enable\nhw_local_irq_enable_n"
> > @@ -162,7 +170,9 @@ class Automata:
> > nr_state += 1
> >
> > # declare the matrix....
> > - matrix = [[self.invalid_state_str for x in range(nr_event)] for y in
> > range(nr_state)]
> > + matrix = [
> > + [self.invalid_state_str for x in range(nr_event)] for y in
> > range(nr_state)
> > + ]
> >
> > # and we are back! Let's fill the matrix
> > cursor = self.__get_cursor_begin_events()
> > @@ -170,9 +180,9 @@ class Automata:
> > while self.__dot_lines[cursor].lstrip()[0] == '"':
> > if self.__dot_lines[cursor].split()[1] == "->":
> > line = self.__dot_lines[cursor].split()
> > - origin_state = line[0].replace('"', '').replace(',', '_')
> > - dest_state = line[2].replace('"', '').replace(',', '_')
> > - possible_events = line[-2].replace('"', '').replace("\\n", "
> > ")
> > + origin_state = line[0].replace('"', "").replace(",", "_")
> > + dest_state = line[2].replace('"', "").replace(",", "_")
> > + possible_events = line[-2].replace('"', "").replace("\\n", "
> > ")
>
> All in all looks good, thanks.
>
> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
>
> > for event in possible_events.split():
> > matrix[states_dict[origin_state]][events_dict[event]] =
> > dest_state
> > cursor += 1
On Tue, 2026-01-20 at 08:42 -0300, Wander Lairson Costa wrote:
> On Tue, Jan 20, 2026 at 09:21:01AM +0100, Gabriele Monaco wrote:
>
> >
> > I believe these newlines were added automatically by some tools, not sure if
> > we
> > really want them but they don't belong in this patch (since 1/26 added this
> > class).
> >
> There are python formatting tools that put 2 lines after a type
> definition. Anyway, I can remove it in v2.
If that's common practice I'm fine keeping it, I just would create this class
directly with the newlines separators in 1/26 instead of adding these lines
later in the same series. Just to reduce the noise.
>
> > > class Automata:
> > > """Automata class: Reads a dot file and parses it as an automata.
> > >
> > > @@ -31,7 +33,9 @@ class Automata:
> > > self.__dot_path = file_path
> > > self.name = model_name or self.__get_model_name()
> > > self.__dot_lines = self.__open_dot()
> > > - self.states, self.initial_state, self.final_states =
> > > self.__get_state_variables()
> > > + self.states, self.initial_state, self.final_states = (
> > > + self.__get_state_variables()
> > > + )
> >
> > There is no strict 80 character limit for python code and I personally find
> > this
> > less readable. Is this again what the tool suggested?
> >
>
> In general, 100 lines is assumed the to a good limit. Anyway, this is
> minor and I can remove the change in v2 if desired.
Yeah 100 is probably also what checkpatch.pl uses (although I think it skips
python files), since this is below 90 columns, I wouldn't touch it.
Thanks,
Gabriele
>
> > > self.events = self.__get_event_variables()
> > > self.function = self.__create_matrix()
> > > self.events_start, self.events_start_run =
> > > self.__store_init_events()
> > > @@ -86,6 +90,7 @@ class Automata:
> > > # wait for node declaration
> > > states = []
> > > final_states = []
> > > + initial_state = None
> > >
> > > has_final_states = False
> > > cursor = self.__get_cursor_begin_states()
> > > @@ -96,9 +101,9 @@ class Automata:
> > > raw_state = line[-1]
> > >
> > > # "enabled_fired"}; -> enabled_fired
> > > - state = raw_state.replace('"', '').replace('};',
> > > '').replace(',',
> > > '_')
> > > + state = raw_state.replace('"', "").replace("};",
> > > "").replace(",",
> > > "_")
> >
> > Ok this change is good.
> >
> > > if state.startswith(self.init_marker):
> > > - initial_state = state[len(self.init_marker):]
> > > + initial_state = state[len(self.init_marker) :]
> >
> > You fixed spacing in 12/26. We could either keep move this change there or
> > just
> > merge that patch with others touching the same files.
> >
>
> Np, I can move this change to there.
>
> > > else:
> > > states.append(state)
> > > if "doublecircle" in self.__dot_lines[cursor]:
> > > @@ -111,6 +116,9 @@ class Automata:
> > >
> > > cursor += 1
> > >
> > > + if initial_state is None:
> > > + raise AutomataError("The automaton doesn't have a initial
> > > state")
> > > +
> >
> > Yeah that's needed.
> >
> > > states = sorted(set(states))
> > >
> > > # Insert the initial state at the beginning of the states
> > > @@ -132,7 +140,7 @@ class Automata:
> > > # ------------ event is here ------------^^^^^
> > > if self.__dot_lines[cursor].split()[1] == "->":
> > > line = self.__dot_lines[cursor].split()
> > > - event = line[-2].replace('"', '')
> > > + event = line[-2].replace('"', "")
> > >
> > > # when a transition has more than one labels, they are
> > > like
> > > this
> > > # "local_irq_enable\nhw_local_irq_enable_n"
> > > @@ -162,7 +170,9 @@ class Automata:
> > > nr_state += 1
> > >
> > > # declare the matrix....
> > > - matrix = [[self.invalid_state_str for x in range(nr_event)] for y
> > > in
> > > range(nr_state)]
> > > + matrix = [
> > > + [self.invalid_state_str for x in range(nr_event)] for y in
> > > range(nr_state)
> > > + ]
> > >
> > > # and we are back! Let's fill the matrix
> > > cursor = self.__get_cursor_begin_events()
> > > @@ -170,9 +180,9 @@ class Automata:
> > > while self.__dot_lines[cursor].lstrip()[0] == '"':
> > > if self.__dot_lines[cursor].split()[1] == "->":
> > > line = self.__dot_lines[cursor].split()
> > > - origin_state = line[0].replace('"', '').replace(',', '_')
> > > - dest_state = line[2].replace('"', '').replace(',', '_')
> > > - possible_events = line[-2].replace('"',
> > > '').replace("\\n", "
> > > ")
> > > + origin_state = line[0].replace('"', "").replace(",", "_")
> > > + dest_state = line[2].replace('"', "").replace(",", "_")
> > > + possible_events = line[-2].replace('"',
> > > "").replace("\\n", "
> > > ")
> >
> > All in all looks good, thanks.
> >
> > Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
> >
> > > for event in possible_events.split():
> > > matrix[states_dict[origin_state]][events_dict[event]]
> > > =
> > > dest_state
> > > cursor += 1
© 2016 - 2026 Red Hat, Inc.