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