Source code for uppaal2jetracer.uppaalmodel.elements

"""UPPAAL elements

This file contains the sub-elements of the system component.

This file can be imported and contains the following classes:

    * UppaalElement:    Abstract base class for all UPPAAL elements.
    * Synchronization:  Channel synchronizations of transitions.
    * Guard:            Condition of a transitions.
    * Update:           Assignments when taking a transition.
    * Transition:       UPPAAL transition from a location to another location.
    * Invariant:        Condition that must be fulfilled in a location.
    * Location:         UPPAAL location in an automaton.
"""

from __future__ import annotations

import copy
from abc import ABC
from typing import List, Optional

from uppaal2jetracer.declarations.declarations_ast import Node


[docs] class UppaalElement(ABC): """ Abstract base class for all UPPAAL components. Serves as the superclass for all elements generated by the UPPAAL parser. """
[docs] class Synchronization: """ Represents a synchronization action in UPPAAL, such as channel communication. :ivar _synchronization: The Synchronization Label :vartype _synchronization: Node :ivar _sending: Indicates whether this is a sending synchronization. :vartype _sending: bool """ __slots__ = ('_synchronization', '_is_sending') def __init__(self, sending: bool, synchronization: Node): self._synchronization = copy.deepcopy(synchronization) self._is_sending = sending @property def synchronization(self) -> Node: """ The synchronisation root node. :return: The synchronisation root node. :rtype: Node """ return copy.deepcopy(self._synchronization) @property def is_sending(self) -> bool: """ The synchronization is sending/receiving. :return: True if synchronization is sending, False if synchronization is receiving. :rtype: bool """ return self._is_sending
[docs] class Guard: """ Represents a guard condition that must be satisfied for a transition to be enabled. :ivar _decision: The condition that must be met. :vartype _decision: Node """ __slots__ = ('_decision',) def __init__(self, decision: Node): self._decision = copy.deepcopy(decision) @property def decision(self) -> Node: """ The guard root node. :return: The guard root node. :rtype: Node """ return copy.deepcopy(self._decision)
[docs] class Update: """ Represents update operations (assignments) performed during a transition. :ivar _assignments: A list of assignment operations. :vartype _assignments: List[Node] """ __slots__ = ('_assignments',) def __init__(self, assignments: List[Node]): if assignments is None: assignments = [] self._assignments = copy.deepcopy(assignments) @property def assignments(self) -> List[Node]: """ The list of assignment root nodes. :return: The List of assignment root nodes. :rtype: List[Node] """ return copy.deepcopy(self._assignments)
[docs] class Transition(UppaalElement): """ Represents a transition between two locations in an automaton. Contains guard conditions, updates, and synchronization actions. :ivar _guard: Condition that must be true for the transition to occur. :vartype _guard: Guard :ivar _update: Updates to execute during the transition. :vartype _update: Update :ivar _synchronization: Synchronization label and type associated with the transition. :vartype synchronization: Synchronization """ __slots__ = ('_source', '_target', '_guard', '_update', '_synchronization') def __init__(self, guard: Optional[Guard] = None, update: Optional[Update] = None, synchronization: Optional[Synchronization] = None): self._guard = guard self._update = update self._synchronization = synchronization self._source = Location self._target = Location self._source = None self._target = None @property def guard(self) -> Optional[Guard]: """ The guard of the transition. :return: The guard of the transition. :rtype: Optional[Guard] """ return self._guard @property def update(self) -> Optional[Update]: """ The update of the transition. :return: The update of the transition. :rtype: Optional[Update] """ return self._update @property def synchronization(self) -> Optional[Synchronization]: """ The synchronization of the transition. :return: The synchronization of the transition. :rtype: Optional[Synchronization] """ return self._synchronization @property def source(self) -> Optional[Location]: """ The source of the transition. :return: The source of the transition, if no source defined return None. :rtype: Optional[Location] """ return self._source @property def target(self) -> Optional[Location]: """ The target of the transition. :return: The target of the transition, if no source defined return None. :rtype: Optional[Location] """ return self._target @source.setter def source(self, location: Location): self._source = location @target.setter def target(self, location: Location): self._target = location
[docs] class Invariant: """ Represents an invariant condition that must hold in a specific state (location). :ivar _decision: The invariant condition. :vartype _decision: Node """ __slots__ = ('_decision',) def __init__(self, decision: Node): self._decision = copy.deepcopy(decision) @property def decision(self) -> Node: """ The invariant root node. :return: The invariant root node. :rtype: Node """ return copy.deepcopy(self._decision)
[docs] class Location(UppaalElement): """ Represents a state (location) in an automaton with an invariant and outgoing transitions. :ivar _identifier: Unique identifier for the location. :vartype _identifier: str :ivar _name: Name of the location. :vartype _name: str :ivar _invariant: Invariant that must be valid in this location. :vartype _invariant: Invariant """ __slots__ = ('_identifier', '_name', '_invariant', '_transitions') def __init__(self, identifier: str, name: str, inv: Optional[Invariant] = None): self._identifier = identifier self._name = name self._invariant = inv self._transitions: List[Transition] = [] @property def identifier(self) -> str: """ The identifier of the location. :return: The identifier of the location. :rtype: str """ return self._identifier @property def name(self) -> str: """ The name of the location. :return: The name of the location. :rtype: str """ return self._name @property def invariant(self) -> Optional[Invariant]: """ The invariant of the location. :return: the invariant of the location. :rtype: Optional[Invariant] """ return self._invariant @property def transitions(self) -> List[Transition]: """ The outgoing transitions of the location. :return: list of all outgoing transitions. :rtype: List[transition] """ return copy.copy(self._transitions)
[docs] def add_transition(self, t: Transition): """ Adds a transition to the location. :param t: The transition to add to the location. :type t: Transition """ self._transitions.append(t)