uppaal2jetracer.uppaalmodel package
Submodules
uppaal2jetracer.uppaalmodel.elements module
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.
- class Guard(decision: Node)[source]
Bases:
object
Represents a guard condition that must be satisfied for a transition to be enabled.
- Variables:
_decision (Node) – The condition that must be met.
- class Invariant(decision: Node)[source]
Bases:
object
Represents an invariant condition that must hold in a specific state (location).
- Variables:
_decision (Node) – The invariant condition.
- class Location(identifier: str, name: str, inv: Invariant | None = None)[source]
Bases:
UppaalElement
Represents a state (location) in an automaton with an invariant and outgoing transitions.
- Variables:
_identifier (str) – Unique identifier for the location.
_name (str) – Name of the location.
_invariant (Invariant) – Invariant that must be valid in this location.
- add_transition(t: Transition)[source]
Adds a transition to the location.
- Parameters:
t (Transition) – The transition to add to the location.
- property identifier: str
The identifier of the location.
- Returns:
The identifier of the location.
- Return type:
str
- property invariant: Invariant | None
The invariant of the location.
- Returns:
the invariant of the location.
- Return type:
Optional[Invariant]
- property name: str
The name of the location.
- Returns:
The name of the location.
- Return type:
str
- property transitions: List[Transition]
The outgoing transitions of the location.
- Returns:
list of all outgoing transitions.
- Return type:
List[transition]
- class Synchronization(sending: bool, synchronization: Node)[source]
Bases:
object
Represents a synchronization action in UPPAAL, such as channel communication.
- Variables:
_synchronization (Node) – The Synchronization Label
_sending (bool) – Indicates whether this is a sending synchronization.
- property is_sending: bool
The synchronization is sending/receiving.
- Returns:
True if synchronization is sending, False if synchronization is receiving.
- Return type:
bool
- class Transition(guard: Guard | None = None, update: Update | None = None, synchronization: Synchronization | None = None)[source]
Bases:
UppaalElement
Represents a transition between two locations in an automaton. Contains guard conditions, updates, and synchronization actions.
- Variables:
- property guard: Guard | None
The guard of the transition.
- Returns:
The guard of the transition.
- Return type:
Optional[Guard]
- property source: Location | None
The source of the transition.
- Returns:
The source of the transition, if no source defined return None.
- Return type:
Optional[Location]
- property synchronization: Synchronization | None
The synchronization of the transition.
- Returns:
The synchronization of the transition.
- Return type:
Optional[Synchronization]
uppaal2jetracer.uppaalmodel.frame module
Frame
This file contains the frame component of the UPPAAL model.
This file can be imported and contains the following classes:
Frame: Holds all variable and function bindings and represents a scope.
- class Frame(parent: Frame = None)[source]
Bases:
object
Represents a visibility scope for variables and functions in the system.
- Variables:
_parent (Frame) – The parent Frame.
- add_binding(name: str, v: Variable)[source]
Add variable reference to the frame.
- Parameters:
name (str) – The reference name of the variable.
v (Variable) – The variable reference.
- add_function(name: str, n: FuncDef)[source]
Add function root node to the frame.
- Parameters:
name (str) – The reference name of the function.
n (FuncDef) – The root node of the function
- create_temporary_frame(update: Update) Frame [source]
Creates a child frame of this frame, having a copy of all the values assigned in the update.
- Parameters:
update – The assignments the frame needs to contain.
- Returns:
The new frame.
- get_function(name: str) FuncDef | None [source]
Return the function root node if name is found otherwise check parent frame.
- Parameters:
name (str) – Reference name to search for.
- Returns:
Function root node if found, else return None.
- Return type:
Optional[Node]
- get_variable(name: str) Variable | None [source]
Return the variable reference if name is found otherwise check parent frame.
- Parameters:
name (str) – Reference name to search for.
- Returns:
Variable reference if found, else return None.
- Return type:
Optional[Variable]
uppaal2jetracer.uppaalmodel.system module
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.
- class Automaton(name: str, af: Frame, loc: List[Location], init: Location)[source]
Bases:
UppaalElement
Represents an automaton in UPPAAL containing locations and transitions.
- Variables:
- property automaton_frame: Frame
The local frame of the automaton.
- Returns:
The local frame of the automaton.
- Return type:
- property initial_location: Location
The initial location of the automaton.
- Returns:
The initial location of the automaton.
- Return type:
- property locations: List[Location]
The locations inside the automaton.
- Returns:
A list of locations inside the automaton.
- Return type:
List[Location]
- property name: str
The name of the automaton.
- Returns:
The name of the automaton.
- Return type:
str
- class System(gf: Frame, sf: Frame, automata: List[Automaton])[source]
Bases:
UppaalElement
Represents the entire UPPAAL system with global and system frames and automata.
- Variables:
- property automata: List[Automaton]
The automata inside the system.
- Returns:
A list of all automata in the system.
- Return type:
List[Automaton]
uppaal2jetracer.uppaalmodel.variable module
Variable
This file contains the variables defined in the UPPAAL model.
This file can be imported and contains the following classes:
Variable: Abstract base class for all variables.
IntVariable: Integer variable.
StringVariable: String variable.
DoubleVariable: Double variable.
BooleanVariable: Boolean variable.
Array: Array of variables.
Range: Numerical variable bounded by a range.
Clock: Clock variable.
Channel: Channel variable.
- class Array(is_constant: bool, value: List[Variable] = None)[source]
Bases:
Variable
Represents an array of variables
- get_index(i: int) Variable [source]
Retrieves the element at index ‘i’.
- Parameters:
i (int) – The index to retrieve from.
- Returns:
The value at the index.
- Raises:
IndexOutOfRangeError – Raised when index out of range is accessed.
- set_index(i: int, v: Variable)[source]
Sets the variable at index ‘i’ to variable ‘v’.
- Parameters:
i (int) – The index to change.
v (Variable) – The value to set.
- Raises:
IndexOutOfRangeError – Raised when index out of range is accessed.
- property value
The value of the variable.
- Returns:
The value of the variable.
- Return type:
any
- exception BelowRangeError(attempted_value: int, lower_bounds: int)[source]
Bases:
ValueError
Error raised when a value change of a range is below the lower bounds.
- Parameters:
attempted_value (int) – The value that is attempted to be set.
lower_bounds (int) – The lower bounds of the range.
- class BooleanVariable(is_constant: bool, value: bool = None)[source]
Bases:
Variable
Represents a boolean variable.
- class Channel(is_broadcast: bool)[source]
Bases:
Variable
Represents a channel variable
- Variables:
_is_broadcast (bool) – Defines if channel is broadcast channel.
- clean_up(loc: Location)[source]
Removes all transition in internal list that originate of location ‘loc’.
- Parameters:
loc (Location) – The origin of the transitions to remove
- has_pair() bool [source]
Checks if channel has a pair of receiving/sending transitions.
- Returns:
True if pair exists
- Return type:
bool
- property is_broadcast: bool
Defines if a channel is a broadcast channel.
- Returns:
True if the channel is a broadcast channel, otherwise False.
- Return type:
bool
- property receiving_transitions: List[Transition]
The internal list of receiving transitions.
- Returns:
The internal list of receiving transitions.
- Return type:
List[Transition]
- register_receiving(t: Transition)[source]
Add element to internal receiving list.
- Parameters:
t (Transition) – The transition to add.
- register_sending(t: Transition)[source]
Add element to internal sending list.
- Parameters:
t (Transition) – The transition to add.
- property sending_transitions: List[Transition]
The internal list of sending transitions.
- Returns:
The internal list of sending transition.
- Return type:
List[Transition]
- class Clock(value: float = 0.0)[source]
Bases:
Variable
Represents a clock variable
- property value: float
The value of the variable.
- Returns:
The value of the variable.
- Return type:
any
- class DoubleVariable(is_constant: bool, value: float = None)[source]
Bases:
Variable
Represents a double variable.
- exception ExceedsRangeError(attempted_value: int, upper_bounds: int)[source]
Bases:
ValueError
Error raised when a value change of a range exceeds the upper bounds.
- Parameters:
attempted_value (int) – The value that is attempted to be set.
upper_bounds (int) – The upper bounds of the range.
- exception ImmutableValueError[source]
Bases:
ValueError
Error raised when a value change of an immutable variable is attempted.
- exception IndexOutOfRangeError(attempted_value: int, array_size: int)[source]
Bases:
IndexError
Error raised when an index out of range of the array is accessed.
- Parameters:
attempted_value (int) – The value that is attempted to be set.
array_size (int) – The size of the array.
- class IntVariable(is_constant: bool, value: int = None)[source]
Bases:
Variable
Represents an integer variable.
- class Range(is_constant: bool, start: int, end: int, value: int = None)[source]
Bases:
Variable
Represent a range variable.
- Variables:
_start (int) – The start of the range.
_end (int) – the end of the range.
- property end: int
The end of the range.
- Returns:
The end of the range.
- Return type:
int
- property start: int
The start of the range.
- Returns:
The start of the range.
- Return type:
int
- property value
The value of the variable.
- Returns:
The value of the variable.
- Return type:
any
- class StringVariable(is_constant: bool, value: str = None)[source]
Bases:
Variable
Represents a string variable.
- class Variable(is_constant: bool, value=None)[source]
Bases:
ABC
Base class for all variables used in the system.
- Variables:
_is_constant (bool) – Defines if variable is changeable or not.
_value (any) – The value of the variable.
- property is_constant: bool
Defines if a variable is constant.
- Returns:
True if the variable is constant, otherwise False.
- Return type:
bool
- property value: any
The value of the variable.
- Returns:
The value of the variable.
- Return type:
any