tools/verification/rvgen/rvgen/automata.py

Source file repositories/reference/linux-study-clean/tools/verification/rvgen/rvgen/automata.py

File Facts

System
Linux kernel
Corpus path
tools/verification/rvgen/rvgen/automata.py
Extension
.py
Size
14639 bytes
Lines
369
Domain
Support Tooling And Documentation
Bucket
tools
Inferred role
Support Tooling And Documentation: tools
Status
atlas-only

Why This File Exists

Repository support layer: documentation, build tooling, samples, user-space helper tools, generated initramfs support, licenses, and validation utilities.

Dependency Surface

Detected Declarations

Annotated Snippet

#!/usr/bin/env python3
# SPDX-License-Identifier: GPL-2.0-only
#
# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org>
#
# Automata class: parse an automaton in dot file digraph format into a python object
#
# For further information, see:
#   Documentation/trace/rv/deterministic_automata.rst

import ntpath
import re
from typing import Iterator
from itertools import islice

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.

    Raised when DOT file processing fails due to invalid format, I/O errors,
    or malformed automaton definitions.
    """

class Automata:
    """Automata class: Reads a dot file and parses it as an automaton.

    It supports both deterministic and hybrid automata.

    Attributes:
        dot_file: A dot file with an state_automaton definition.
    """

    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.states, self.initial_state, self.final_states = self.__get_state_variables()
        self.env_types = {}

Annotation

Implementation Notes