"""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)