On Thu, 2026-05-28 at 10:28 +0200, Nam Cao wrote: > The conversion to use Lark left some dead code behind. Remove them. > > Signed-off-by: Nam Cao <[email protected]> > ---
You might want to remove unused imports (linters should help you with that too): * re, typing.Iterator, and itertools.islice from automata.py * deque and ConstraintRule from dot2k Other than that Reviewed-by: Gabriele Monaco <[email protected]> > tools/verification/rvgen/rvgen/automata.py | 154 ------------------- > -- > tools/verification/rvgen/rvgen/dot2k.py | 28 +--- > 2 files changed, 1 insertion(+), 181 deletions(-) > > diff --git a/tools/verification/rvgen/rvgen/automata.py > b/tools/verification/rvgen/rvgen/automata.py > index a3be327c2a73..b6ff5fceb820 100644 > --- a/tools/verification/rvgen/rvgen/automata.py > +++ b/tools/verification/rvgen/rvgen/automata.py > @@ -356,19 +356,6 @@ class State: > self.name = name > self.inv = inv > > -class _ConstraintKey: > - """Base class for constraint keys.""" > - > -class _StateConstraintKey(_ConstraintKey, int): > - """Key for a state constraint. Under the hood just state_id.""" > - def __new__(cls, state_id: int): > - return super().__new__(cls, state_id) > - > -class _EventConstraintKey(_ConstraintKey, tuple): > - """Key for an event constraint. Under the hood just > tuple(state_id,event_id).""" > - def __new__(cls, state_id: int, event_id: int): > - return super().__new__(cls, (state_id, event_id)) > - > class AutomataError(Exception): > """Exception raised for errors in automata parsing and > validation. > > @@ -387,28 +374,10 @@ class Automata: > > invalid_state_str = "INVALID_STATE" > init_marker = "__init_" > - node_marker = "{node" > - # val can be numerical, uppercase (constant or macro), lowercase > (parameter or function) > - # only numerical values should have units > - constraint_rule = re.compile(r""" > - ^ > - (?P<env>[a-zA-Z_][a-zA-Z0-9_]+) # C-like identifier for the > env var > - (?P<op>[!<=>]{1,2}) # operator > - (?P<val> > - [0-9]+ | # numerical value > - [A-Z_]+\(\) | # macro > - [A-Z_]+ | # constant > - [a-z_]+\(\) | # function > - [a-z_]+ # parameter > - ) > - (?P<unit>[a-z]{1,2})? # optional unit for > numerical values > - """, re.VERBOSE) > - constraint_reset = re.compile(r"^reset\((?P<env>[a-zA-Z_][a-zA- > Z0-9_]+)\)") > > def __init__(self, file_path, model_name=None): > self.__dot_path = file_path > self.name = model_name or self.__get_model_name() > - self.__dot_lines = self.__open_dot() > self.__parse_tree = ParseTree(file_path) > self.transitions = self.__parse_transitions() > self.states, self.initial_state, self.final_states = > self.__parse_states() > @@ -435,57 +404,6 @@ class Automata: > > return model_name > > - def __open_dot(self) -> list[str]: > - dot_lines = [] > - try: > - with open(self.__dot_path) as dot_file: > - dot_lines = dot_file.readlines() > - except OSError as exc: > - raise AutomataError(exc.strerror) from exc > - > - if not dot_lines: > - raise AutomataError(f"{self.__dot_path} is empty") > - > - # checking the first line: > - line = dot_lines[0].split() > - > - if len(line) < 2 or line[0] != "digraph" or line[1] != > "state_automaton": > - raise AutomataError(f"Not a valid .dot format: > {self.__dot_path}") > - > - return dot_lines > - > - def __get_cursor_begin_states(self) -> int: > - for cursor, line in enumerate(self.__dot_lines): > - split_line = line.split() > - > - if len(split_line) and split_line[0] == > self.node_marker: > - return cursor > - > - raise AutomataError("Could not find a beginning state") > - > - def __get_cursor_begin_events(self) -> int: > - state = 0 > - cursor = 0 # make pyright happy > - > - for cursor, line in enumerate(self.__dot_lines): > - line = line.split() > - if not line: > - continue > - > - if state == 0: > - if line[0] == self.node_marker: > - state = 1 > - elif line[0] != self.node_marker: > - break > - else: > - raise AutomataError("Could not find beginning event") > - > - cursor += 1 # skip initial state transition > - if cursor == len(self.__dot_lines): > - raise AutomataError("Dot file ended after event > beginning") > - > - return cursor > - > def __parse_transitions(self): > transitions = [] > > @@ -542,51 +460,6 @@ class Automata: > states.insert(0, initial_state) > return states, initial_state, final_states > > - def __get_state_variables(self) -> tuple[list[str], str, > list[str]]: > - # wait for node declaration > - states = [] > - final_states = [] > - initial_state = "" > - > - has_final_states = False > - cursor = self.__get_cursor_begin_states() > - > - # process nodes > - for line in islice(self.__dot_lines, cursor, None): > - split_line = line.split() > - if not split_line or split_line[0] != self.node_marker: > - break > - > - raw_state = split_line[-1] > - > - # "enabled_fired"}; -> enabled_fired > - state = raw_state.replace('"', '').replace('};', > '').replace(',', '_') > - if state.startswith(self.init_marker): > - initial_state = state[len(self.init_marker):] > - else: > - states.append(state) > - if "doublecircle" in line: > - final_states.append(state) > - has_final_states = True > - > - if "ellipse" in line: > - 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) > - > - # Insert the initial state at the beginning of the states > - states.insert(0, initial_state) > - > - if not has_final_states: > - final_states.append(initial_state) > - > - return states, initial_state, final_states > - > def __get_event_variables(self) -> tuple[list[str], list[str]]: > events: list[str] = [] > envs: list[str] = [] > @@ -609,26 +482,6 @@ class Automata: > > return sorted(set(events)), sorted(set(envs)) > > - def _split_constraint_expr(self, constr: list[str]) -> > Iterator[tuple[str, > - > > str | None]]: > - """ > - Get a list of strings of the type constr1 && constr2 and > returns a list of > - constraints and separators: [[constr1,"&&"],[constr2,None]] > - """ > - exprs = [] > - seps = [] > - for c in constr: > - while "&&" in c or "||" in c: > - a = c.find("&&") > - o = c.find("||") > - pos = a if o < 0 or 0 < a < o else o > - exprs.append(c[:pos].replace(" ", "")) > - seps.append(c[pos:pos + 2].replace(" ", "")) > - c = c[pos + 2:].replace(" ", "") > - exprs.append(c) > - seps.append(None) > - return zip(exprs, seps) > - > def __extract_env_var(self, constraint: ConstraintCondition): > if constraint.unit: > self.env_types[constraint.env] = constraint.unit > @@ -697,10 +550,3 @@ class Automata: > > def is_hybrid_automata(self) -> bool: > return bool(self.envs) > - > - def is_event_constraint(self, key: _ConstraintKey) -> bool: > - """ > - Given the key in self.constraints return true if it is an > event > - constraint, false if it is a state constraint > - """ > - return isinstance(key, _EventConstraintKey) > diff --git a/tools/verification/rvgen/rvgen/dot2k.py > b/tools/verification/rvgen/rvgen/dot2k.py > index 49cb3e724a93..d6779ac6b7dd 100644 > --- a/tools/verification/rvgen/rvgen/dot2k.py > +++ b/tools/verification/rvgen/rvgen/dot2k.py > @@ -11,9 +11,7 @@ > from collections import deque > from .dot2c import Dot2c > from .generator import Monitor > -from .automata import _EventConstraintKey, _StateConstraintKey, > AutomataError > -from .automata import ConstraintRule, ConstraintCondition > - > +from .automata import ConstraintRule, ConstraintCondition, > AutomataError > > class dot2k(Monitor, Dot2c): > template_dir = "dot2k" > @@ -217,9 +215,6 @@ class ha2k(dot2k): > value *= 10**9 > return str(value) + "ull" > > - def __parse_single_constraint(self, rule: dict, value: str) -> > str: > - return f"ha_get_env(ha_mon, {rule["env"]}{self.enum_suffix}, > time_ns) {rule["op"]} {value}" > - > def __parse_guard_rule(self, rule) -> list[str]: > buff = [] > for c, sep in rule.rules: > @@ -233,12 +228,6 @@ class ha2k(dot2k): > buff.append(cond) > return buff > > - def __get_constraint_env(self, constr: str) -> str: > - """Extract the second argument from an ha_ function""" > - env = > constr.split("(")[1].split()[1].rstrip(")").rstrip(",") > - assert env.rstrip(f"_{self.name}") in self.envs > - return env > - > def __start_to_invariant_check(self, inv: ConstraintCondition) - > > str: > # by default assume the timer has ns expiration > clock_type = "ns" > @@ -249,21 +238,6 @@ class ha2k(dot2k): > > return f"return ha_check_invariant_{clock_type}(ha_mon, > {inv.env}_{self.name}, time_ns, {value})" > > - def __start_to_conv(self, constr: str) -> str: > - """ > - Undo the storage conversion done by ha_start_timer_ > - """ > - return "ha_inv_to_guard" + constr[constr.find("("):] > - > - def __parse_timer_constraint(self, rule: dict, value: str) -> > str: > - # by default assume the timer has ns expiration > - clock_type = "ns" > - if self.env_types.get(rule["env"]) == "j": > - clock_type = "jiffy" > - > - return (f"ha_start_timer_{clock_type}(ha_mon, > {rule["env"]}{self.enum_suffix}," > - f" {value}, time_ns)") > - > def __parse_invariant(self, inv): > # by default assume the timer has ns expiration > clock_type = "ns"
