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.

property decision: Node

The guard root node.

Returns:

The guard root node.

Return type:

Node

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.

property decision: Node

The invariant root node.

Returns:

The invariant root node.

Return type:

Node

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

property synchronization: Node

The synchronisation root node.

Returns:

The synchronisation root node.

Return type:

Node

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:
  • _guard (Guard) – Condition that must be true for the transition to occur.

  • _update (Update) – Updates to execute during the transition.

  • _synchronization – Synchronization label and type associated with the transition.

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]

property target: Location | None

The target of the transition.

Returns:

The target of the transition, if no source defined return None.

Return type:

Optional[Location]

property update: Update | None

The update of the transition.

Returns:

The update of the transition.

Return type:

Optional[Update]

class Update(assignments: List[Node])[source]

Bases: object

Represents update operations (assignments) performed during a transition.

Variables:

_assignments (List[Node]) – A list of assignment operations.

property assignments: List[Node]

The list of assignment root nodes.

Returns:

The List of assignment root nodes.

Return type:

List[Node]

class UppaalElement[source]

Bases: ABC

Abstract base class for all UPPAAL components. Serves as the superclass for all elements generated by the UPPAAL parser.

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]

property parent: Frame

The parent of the frame.

Returns:

The parent of the frame.

Return type:

Frame

reset()[source]

Resets all variables inside the frame to their starting value.

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:
  • _name (str) – Name of the automaton.

  • _automaton_frame (Frame) – Local frame storing variables and functions.

  • _locations (List[Location]) – List of all locations in the automaton.

  • _initial_location (Location) – The initial location of the automaton.

property automaton_frame: Frame

The local frame of the automaton.

Returns:

The local frame of the automaton.

Return type:

Frame

property initial_location: Location

The initial location of the automaton.

Returns:

The initial location of the automaton.

Return type:

Location

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:
  • _global_frame (Frame) – Global frame for variables and functions.

  • _system_frame (Frame) – System frame for system declarations.

  • _automata (List[Automaton]) – List of all automata in the system.

property automata: List[Automaton]

The automata inside the system.

Returns:

A list of all automata in the system.

Return type:

List[Automaton]

property global_frame: Frame

The frame with the global declarations of the system.

Returns:

The global-frame

Return type:

Frame

property system_frame: Frame

The frame with the system declarations of the system.

Returns:

The system-frame.

Return type:

Frame

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.

reset()[source]

Resets the variable to a starting state.

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.

reset()[source]

Resets the variable to a starting state.

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.

reset()[source]

Resets the variable to a starting state.

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

reset()[source]

Resets the variable to a starting state.

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.

reset()[source]

Resets the variable to a starting state.

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.

reset()[source]

Resets the variable to a starting state.

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

reset()[source]

Resets the variable to a starting state.

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.

reset()[source]

Resets the variable to a starting state.

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

abstract reset()[source]

Resets the variable to a starting state.

property value: any

The value of the variable.

Returns:

The value of the variable.

Return type:

any

Module contents