Source code for uppaal2jetracer.uppaalmodel.system

"""System

This file contains the big components of the UPPAAL model.

This file can be imported and contains the following classes:

    * Automaton:    State machine with locations and transitions.
    * System:       Holds many automata and manages them.
"""

from __future__ import annotations

import copy
from typing import List

from uppaal2jetracer.uppaalmodel.frame import Frame
from uppaal2jetracer.uppaalmodel.elements import UppaalElement, Location


[docs] class Automaton(UppaalElement): """ Represents an automaton in UPPAAL containing locations and transitions. :ivar _name: Name of the automaton. :vartype _name: str :ivar _automaton_frame: Local frame storing variables and functions. :vartype _automaton_frame: Frame :ivar _locations: List of all locations in the automaton. :vartype _locations: List[Location] :ivar _initial_location: The initial location of the automaton. :vartype _initial_location: Location """ __slots__ = ('_name', '_automaton_frame', '_locations', '_initial_location') def __init__(self, name: str, af: Frame, loc: List[Location], init: Location): self._name = name self._automaton_frame = af self._locations = copy.copy(loc) self._initial_location = init @property def name(self) -> str: """ The name of the automaton. :return: The name of the automaton. :rtype: str """ return self._name @property def automaton_frame(self) -> Frame: """ The local frame of the automaton. :return: The local frame of the automaton. :rtype: Frame """ return self._automaton_frame @property def locations(self) -> List[Location]: """ The locations inside the automaton. :return: A list of locations inside the automaton. :rtype: List[Location] """ return copy.copy(self._locations) @property def initial_location(self) -> Location: """ The initial location of the automaton. :return: The initial location of the automaton. :rtype: Location """ return self._initial_location
[docs] class System(UppaalElement): """ Represents the entire UPPAAL system with global and system frames and automata. :ivar _global_frame: Global frame for variables and functions. :vartype _global_frame: Frame :ivar _system_frame: System frame for system declarations. :vartype _system_frame: Frame :ivar _automata: List of all automata in the system. :vartype _automata: List[Automaton] """ __slots__ = ('_global_frame', '_system_frame', '_automata') def __init__(self, gf: Frame, sf: Frame, automata: List[Automaton]): self._global_frame = gf self._system_frame = sf self._automata = copy.copy(automata) @property def global_frame(self) -> Frame: """ The frame with the global declarations of the system. :return: The global-frame :rtype: Frame """ return self._global_frame @property def system_frame(self) -> Frame: """ The frame with the system declarations of the system. :return: The system-frame. :rtype: Frame """ return self._system_frame @property def automata(self) -> List[Automaton]: """ The automata inside the system. :return: A list of all automata in the system. :rtype: List[Automaton] """ return copy.copy(self._automata)