User API

pyuppaal.umodel

umodel

class pyuppaal.umodel.UModel(model_path: Optional[str] = None)[source]

Bases: object

Load UPPAAL model for analysis, editing, verification and other operations. If you want to modify the model, you should from pyuppaal.nta import Template, Location, Edge.

property declaration: str
property templates: List[Template]
property system: str
property queries: Optional[List[str]]
property Element: Element

xml contents of self, including 1. declaration 2. template(s) 3. system 4. query(s)

property ElementTree: ElementTree
property model_path: str

Current model path.

Returns:

str – Current model path.

property max_location_id: int

Get the maximum location_id so as to make it easier to create a new template, because the id of Location is unique.

Returns:

int – max location id of self.

property broadcast_chan: List[str]

Get broadcast channels in declaration.

Returns:

List[str] – List of broadcast channels.

property xml: str
static new(model_path: str) → UModel[source]

创建一个新的uppaal xml文件

Parameters:

file_name (str) – file name

Returns:

UModel – a new UModel instance.

save_as(new_path: str) → UModel[source]

Save the model to a new path with self.model_path changed to new_model_path.

Parameters:

new_path (str) – target model path.

Returns:

UModel – self.

save() → UModel[source]

Save the current model.

Returns:

UModel – self.

copy_as(new_path: str) → UModel[source]

Make a copy of the current model and return the copied instance.

Parameters:

new_path (str) – target copy file path.

Returns:

UModel – new copied instance.

verify(trace_path: Optional[str] = None, verify_options: Optional[str] = None, keep_tmp_file: bool = True) → str[source]

Verify and return the verify result. If trace_path is not given, it wll return the terminal result.

Parameters:

  • trace_path (str, optional) – the path to save the trace file. Defaults to None.

  • verify_options (str, optional) – options for verifyta, such as ` -t 0 -o 0`. Defaults to None.

  • keep_tmp_file (bool, optional) – whether to keep the temp file such as xtr or in-process xml. Defaults to True.

Returns:

str – terminal verify results for self.

easy_verify(verify_options: str = '-t 1', keep_tmp_file=True) → pyuppaal.tracer.SimTrace | None[source]

Easily verify current model, create a .xtr trace file that has the same name as self.model_path, and return parsed counter example as SimTrace (if exists). You can do easy_verify with only ONE query each time.

Parameters:

  • verify_options (str, optional) – verify options, and -t must be set because returning a SimTrace requires a .xtr trace file. Defaults to ‘-t 1’, returning the shortest trace.

  • keep_tmp_file (bool, optional) – whether to keep the temp file such as xtr or in-process xml. Defaults to True.

Returns:

SimTrace | None – if exists a counter example, return a SimTrace, else return None.

get_communication_graph(save_path=None, is_beautify=True) → Mermaid[source]

Get the communication graph of the UPPAAL model, and return a Mermaid instance.

Parameters:

  • save_path (_type_, optional) – <.md | .svg | .pdf | .png>, the path to save the file. Defaults to None.

  • is_beautify (bool, optional) – whether beautify the mermaid file by merging edges. Defaults to True.

Returns:

Mermaid – a Mermaid instance.

remove_template(template_name: str) → bool[source]

Delete the template according to template_name.

Parameters:

template_name (str) – the name of template you want to delte.

Returns:

bool – True when succeed, False when fail.

add_observer_monitor(observations: List[tuple[str, str, str]], sigma_o: List[str], template_name: str = 'Observer', is_strict: bool = True, all_patterns: bool = False) → None[source]

Add an observer template, which will also be embedded in system declarations. If exists a template with the same name, it will raise error.

An observer is a monitor that observes the sequence of actions, and it will reach the pass state if the observed sequence of actions is a subsequence of the trace.

Parameters:

  • observations (List[str] | List[tuple[str, str, str]]) – observed actions. If List[str], then it is a list of actions. If List[tuple[str,str,str]], then it is a list of (action, lower_bound, upper_bound).

  • sigma_o (List[str]) – the set of observable actions.

  • template_name (str, optional) – the name of the template. Defaults to ‘observer’.

  • is_strict (bool, optional) – if strict, any other observations will be illegal. For example, assume you set observations a1, gclk=1, a2, gclk=3, and there exists trace T: a1, gclk=1, a2, gclk=2, a2, gclk=3. If is_strict_observer is True, then T is invalid. Defaults to True.

  • all_patterns (bool, optional) – whether the monitor is used for find_all_patterns. Defaults to False.

Raises:

ValueError – if template_name already exists, raise ValueError.

Returns:

None

add_input_monitor(inputs: Union[List[str], List[tuple[str, str, str]]], template_name: str = 'Input') → None[source]

Add a linear input template that captures specified inputs, which will also be embedded in system declarations. Template that has the same name will be over written.

Parameters:

  • observations (List[str] | List[tuple[str, str, str]]) – input actions. If List[str], then it is a list of actions. If List[tuple[str,str,str]], then it is a list of (action, lower_bound, upper_bound).

  • template_name (str, optional) – the name of the template. Defaults to ‘input’.

Returns:

None

add_template(template: Template) → None[source]

Add template to self.template. However, if you also want to embed the template to system, you should also call self.add_template_to_system(template_name: str).

Parameters:

template (Template) – the template to be added to self.template.

Raises:

ValueError – raise ValueError if template with the same name already exists.

add_template_to_system(template_name: str)[source]

Add a template to system declarations. For example, a system declaration is “system Process1, Process2;”. After add Process3 by add_template_to_system(‘Process3’), we get “system Process1, Process2, Process3;”.

Note that before add_template_to_system, you should first call self.add_template(template: Template).

Parameters:

template_name (str) – the name of the template.

Raises:

ValueError – if template_name already exists, raise ValueError.

find_a_pattern(focused_actions: Optional[List[str]] = None, keep_tmp_file: bool = True, options: Optional[str] = None) → pyuppaal.tracer.SimTrace | None[source]

Find a pattern in the current model.

Parameters:

  • focused_actions (List[str], optional) – the set of actions you are focused on. Only events in focused_actions will be analyzed when find_all_patterns. Defaults to None, taking all the events of the current model.

  • keep_tmp_file (bool, optional) – whether to keep the temp file such as xtr or in-process xml. Defaults to True.

  • options (str, optional) – options for verifyta, such as ` -t 0 -o 0`. Defaults to None.

Returns:

SimTrace | None – pattern will be returend as SimTrace. Return None if no pattern is found.

find_all_patterns(focused_actions: Optional[List[str]] = None, verify_options: str = '-t 1', keep_tmp_file: bool = True) → List[SimTrace][source]

Find all patterns of the first query in the model, if the number of patterns is finite. If the number of patterns is infinite, it will loop forever. It will always search the shortest patterns first, i.e., verify_options: str = “-t 1”. If you want the fastest patterns first, you can let verify_options: str = “-t 2”.

Parameters:

  • focused_actions (List[str], optional) – the set of actions you are focused on. Only events in focused_actions will be analyzed when find_all_patterns. Defaults to None, it will automatically extract all events from current model.

  • verify_options – (str, optional): model checking options of verifyta. Get more details by verifyta -h. Defaults to -t 1, and it will search from shortest pattern. Other options, -t 2 from the fastest pattern.

  • keep_tmp_file (bool, optional) – whether to keep the temp file such as xtr or in-process xml. Defaults to True.

Returns:

List[SimTrace] – the list of found patterns.

find_all_patterns_iter(focused_actions: Optional[List[str]] = None, verify_options: str = '-t 1', keep_tmp_file: bool = True) → SimTrace[source]

Find all patterns that satisfy self.queries[0] using a generator.

Parameters:

  • focused_actions (List[str], optional) – the set of actions you are focused on. Only events in focused_actions will be analyzed when find_all_patterns. Defaults to None, it will automatically extract all events from current model.

  • verify_options – (str, optional): model checking options of verifyta. Get more details by verifyta -h. Defaults to -t 1, and it will search from shortest pattern. Other options, -t 2 from the fastest pattern.

  • keep_tmp_file (bool, optional) – whether to keep the temp file such as xtr or in-process xml. Defaults to True.

Yields:

SimTrace – a pattern that satisfies the query.

fault_diagnosability(fault: str, n: int, sigma_o: List[str], sigma_un: List[str], visual=False, keep_tmp_file=True)[source]

Determine whether the fault is n diagnosable.

This function will NOT modify the model. It will copy to ‘tmp_diagnosable_suffix.xml’ and ‘tmp_identify.xml’ Note: If not keep_tmp_file, it won’t be able to get the trace because the tmp model is removed.

Parameters:

  • fault (str) – fault name

  • n (int) – n-diagnosability

  • sigma_o (List[str]) – the set of observable events,

  • sigma_un (List[str]) – the set of unobservable events,

  • visual (bool, optional) – whether to visualize the analyzing process with a progress bar. Defaults to False.

  • keep_tmp_file (bool, optional) – whether to keep the temp file such as xtr or in-process xml. Defaults to True.

Returns:

(bool, SimTrace) – bool: whether the fault is n-diagnosable. SimTrace: if is not n-diagnosable, a SimTrace will be returend as a proof.

fault_diagnosability_optimized(fault: str, n: int, sigma_o: List[str], sigma_un: List[str], keep_tmp_file=True)[source]

Determine whether the fault is n diagnosable.

This function will NOT modify the model. It will copy to ‘tmp_diagnosable_suffix.xml’ and ‘tmp_identify.xml’ Note: If not keep_tmp_file, it won’t be able to get the trace because the tmp model is removed.

Parameters:

  • fault (str) – fault name

  • n (int) – n-diagnosability

  • sigma_o (List[str]) – the set of observable events,

  • sigma_un (List[str]) – the set of unobservable events,

  • keep_tmp_file (bool, optional) – whether to keep the temp file such as xtr or in-process xml. Defaults to True.

Returns:

(bool, SimTrace) – bool: whether the fault is n-diagnosable. SimTrace: if is not n-diagnosable, a SimTrace will be returend as a proof.

fault_identification(suffix_sequence: List[str], fault: str, sigma_o: List[str], sigma_un: List[str], keep_tmp_file=True)[source]

Do fault identification of fault with suffix_sequence.

Parameters:

  • suffix_sequence (List[str]) – latest observation sequence.

  • fault (str) – the fault to be identified.

  • sigma_o (List[str]) – the set of observable events.

  • sigma_un (List[str]) – the set of unobservable events.

  • keep_tmp_file (bool, optional) – whether to keep the temp file such as xtr or in-process xml. Defaults to True.

Returns:

bool – whether the fault can be identified with suffix_sequence. SimTrace: if the fault can not be identified, a counter-example will be returned.

fault_tolerance(target_state: str, identified_faults: List[str], safety_events: List[str], sigma_f: List[str], sigma_c: List[str], control_length: int, keep_tmp_file=True) → str[source]

Tolerate the identified_faults such that the system can reach the target_state.

Examples

>>> possible return results
"Fault can NOT be tolerated"
"Fault can be tolerated, control sequence tail: ['a1', 'a2'], trace: ['a1', 'a2', 'a3', 'a4']"
"Fault may be tolerated, control sequence tail: ['a1', 'a2'], trace: ['a1', 'a2', 'a3', 'a4']"
"Fault may be tolerated" means that the the provided control sequence is not confirmed to tolerate `identified_faults`,
but there exists such a trace that lead to `target_state`.
Parameters:

  • target_state (str) – the expression of the target state to be reached, which will be concatinated to the ending of TCTL. For example: f”E<> MInputAfterFault.pass and {target_state}”.

  • identified_faults (List[str]) – the set of identified faults.

  • safety_events (List[str]) – the sequence of safety events that should be applied just after the fault.

  • sigma_f (List[str]) – the set of fault events.

  • sigma_c (List[str]) – the set of control events.

  • control_length (int) – the maximum length of control sequence, i.e., the identified_faults should be tolerated within control_length of control events.

  • keep_tmp_file (bool) – whether to keep the temp file such as xtr or in-process xml. Defaults to True.

Returns:

str – the result of tolerance, the control sequence tail, and the trace.

load_xtr_trace(xtr_trace_path: str, keep_if=False) → pyuppaal.tracer.SimTrace | None[source]

Analyze the xtr_trace_path trace file generated by model and return the instance SimTrace.

The internal process is as following: 1. Convert the model_path model into a .if file. 2. Analyze .if file and the xtr_trace_path to get the instance SimTrace. 3. reference: https://github.com/UPPAALModelChecker/utap.

Parameters:

  • model_path (str) – the path of the .xml model file

  • xtr_trace_path (str) – the path of the .xtr trace file

  • keep_if (bool) – keep the .if file

Raises:

  • FileNotFoundError – if the xtr_trace_path file does not exist, raise FileNotFoundError in Verifyta().compile_to_if(self.model_path)

  • ValueError – if the xtr_trace_path file is not a .xtr file, raise ValueError in Verifyta().compile_to_if(self.model_path)

  • ValueError – if the xtr_trace does not fit the model, raise ValueError in utap_parser(if_name, xtr_trace_path)

Returns:

SimTrace | None – if you want to save the parsed raw trace, you can use SimTrace.save_raw(file_name)

pyuppaal.nta

NTA Module This module contains classes and functions for working with UPPAAL NTA models.

class pyuppaal.nta.Location(location_id: int, location_pos: Tuple(int, int), name: str = None, name_pos: Tuple(int, int) = None, invariant: str = None, invariant_pos: Tuple(int, int) = None, rate_of_exponential: float = None, rate_of_exp_pos: Tuple(int, int) = None, is_initial: bool = False, is_urgent: bool = False, is_committed: bool = False, is_branchpoint: bool = False, comments: str = None, comments_pos: Tuple(int, int) = None, test_code_on_enter: str = None, test_code_on_exit: str = None)[source]

Bases: object

Represents a location in a UPPAAL model.

A location in UPPAAL is a state in the state machine of a template. It can have various properties like being an initial, urgent, or committed state, along with invariants, names, and positions.

Examples

>>> # Creating a basic location with an ID and position.
>>> location = Location(location_id=1, location_pos=(100, 200))
>>> # Creating a location with additional properties.
>>> location = Location(
>>>    location_id=2,
>>>    location_pos=(150, 250),
>>>    name="Start",
>>>    invariant="x <= 5",
>>>    is_initial=True)
property Element: Element

xml element as xml.etree.ElementTree.Element

Returns:

ET.Element – xml.etree.ElementTree.Element

property xml: str

获取xml字符串

Returns:

str – xml字符串

static from_xml(location_xml: str | xml.etree.ElementTree.Element) → Location[source]

Parse xml element to a Location instance.

Examples

>>> # A committed location with many properties such as invariant, testcode, etc.
    <location id="id1" x="0" y="0">
        <name x="-10" y="-34">location_name</name>
        <label kind="invariant" x="-10" y="17">inv_inv</label>
        <label kind="exponentialrate" x="-10" y="34">roe_roe</label>
        <label kind="testcodeEnter">on_enter_on_enter</label>
        <label kind="testcodeExit">on_exit_on_exit</label>
        <label kind="comments" x="-10" y="59">comments_comments</label>
        <committed/>
    </location>
Parameters:

location_xml (str | ET.Element) – string that meets xml element format of location.

Returns:

Location – location instance

class pyuppaal.nta.Edge(source_location_id: int, target_location_id: int, source_location_pos: Tuple(int, int), target_location_pos: Tuple(int, int), select: str = None, select_pos: Tuple(int, int) = None, sync: str = None, sync_pos: Tuple(int, int) = None, update: str = None, update_pos: Tuple(int, int) = None, guard: str = None, guard_pos: Tuple(int, int) = None, probability_weight: float = None, prob_weight_pos: Tuple(int, int) = None, comments: str = None, comments_pos: Tuple(int, int) = None, test_code: str = None, nails: List[Tuple(int, int)] = [])[source]

Bases: object

In GUI, it names Edge, but in xml, it names transition. Represents a transition (edge) between two locations in a UPPAAL model.

In UPPAAL, an edge (referred to as ‘transition’ in XML) defines the behavior and conditions for moving from one state (location) to another. It can include synchronization labels, guards, updates, selections, and more.

Examples

>>> # Creating an edge with basic properties.
>>> edge = Edge(
>>>     source_location_id=1,
>>>     target_location_id=2,
>>>     source_location_pos=(100, 200),
>>>     target_location_pos=(300, 400),
>>>     guard="x < 5")

>>> # Creating an edge with additional properties like synchronization and update.
>>> edge = Edge(
>>>     source_location_id=1,
>>>     target_location_id=2,
>>>     source_location_pos=(100, 200),
>>>     target_location_pos=(300, 400),
>>>     sync="a!",
>>>     update="x=0")
property Element: Element

xml element as xml.etree.ElementTree.Element

Returns:

ET.Element – xml.etree.ElementTree.Element

property xml: str

__summary__

Examples

>>> # example of transition (in gui named Edge) xml
    <transition>
        <source ref="id1"/>
        <target ref="id2"/>
        <label kind="select" x="18" y="-51">nnn:id</label>
        <label kind="guard" x="18" y="-34">guard:=0</label>
        <label kind="synchronisation" x="18" y="-17">sync?</label>
        <label kind="assignment" x="18" y="0">update</label>
        <label kind="testcode">testcode_testcode</label>
        <label kind="comments" x="18" y="25">comments_comments</label>
        <nail x="51" y="42"/>
        <nail x="76" y="34"/>
        <nail x="68" y="0"/>
        <nail x="102" y="42"/>
    </transition>
static from_xml(edge_xml: str | xml.etree.ElementTree.Element) → Edge[source]

__summary__

Examples

>>> # normal transition
    <transition>
        <source ref="id1"/>
        <target ref="id2"/>
        <label kind="select" x="18" y="-51">nnn:id</label>
        <label kind="guard" x="18" y="-34">guard:=0</label>
        <label kind="synchronisation" x="18" y="-17">sync?</label>
        <label kind="assignment" x="18" y="0">update</label>
        <label kind="testcode">testcode_testcode</label>
        <label kind="comments" x="18" y="25">comments_comments</label>
        <nail x="51" y="42"/>
        <nail x="76" y="34"/>
    </transition>
Parameters:

et (str | ET.Element) – string that meets xml element format of branch point.

Returns:

Edge – edge instance

class pyuppaal.nta.Template(name: str, locations: List[Location], init_ref: int, edges: Optional[List[Edge]] = None, params: Optional[str] = None, declaration: Optional[str] = None)[source]

Bases: object

Represents a template in a UPPAAL model, defining a set of locations (states), edges (transitions), and other properties.

A template in UPPAAL is a reusable structure that can be instantiated multiple times within a model. It contains locations, edges, declarations, and other components necessary for modeling a component or a system.

property Element: Element

xml element as xml.etree.ElementTree.Element

Returns:

ET.Element – xml.etree.ElementTree.Element

property xml: str

Convert self to ET.Element(part of .xml file) as string, which is not epected to be used by users.

Returns:

str – A string representing the Template instance in UPPAAL .xml format.

static from_xml(template_xml: str | xml.etree.ElementTree.Element) → Template[source]

parse template from .xml file by the following steps: 1. template的name 2. parameter 3. declaration 4. location(s) 5. branchpoint(s) 6. init ref (id of initial location) 7. transitions

Parameters:

template_xml (str | ET.Element) – The XML string or ElementTree Element representing the UPPAAL template.

Returns:

Template – A Template object constructed from the parsed XML data.

pyuppaal.tracer

使用方法 ./trace_custom.exe xxx.if xxx.xtr your_output.txt 注意输入要是LF行尾, 不能是CRLF, 否则会报错unknown section

class pyuppaal.tracer.SimTrace(trace_string: str)[source]

Bases: object

SimTrace is a class that represents a trace.

property raw: str

Original raw string of the trace.

Examples

>>> trace = SimTrace(trace_from_pedestrian)
>>> trace.raw
State: Cars.Idle TrafficLights.cRed_pGreen LV1Pedestrian2.Idle Cars.tCCrssMax=4 Cars.tCCrssMin=1 LV1Pedestrian2.tPCrssMin=0 LV1Pedestrian2.tPCrssMax=10 t(0)-tTL<=0 t(0)-Cars.tc<=0 t(0)-TrafficLights.tTL<=0 t(0)-LV1Pedestrian2.tp<=0 t(0)-LV1Pedestrian2.tTL<=0 tTL-t(0)<=55 tTL-Cars.tc<=0 Cars.tc-TrafficLights.tTL<=0 TrafficLights.tTL-LV1Pedestrian2.tp<=0 LV1Pedestrian2.tp-LV1Pedestrian2.tTL<=0 LV1Pedestrian2.tTL-tTL<=0
Transition: LV1Pedestrian2.Idle -> LV1Pedestrian2.CheckTL {1; pWantCrss!; 1;} TrafficLights.cRed_pGreen -> TrafficLights._id8 {1; pWantCrss?; 1;}
State: Cars.Idle TrafficLights._id8 LV1Pedestrian2.CheckTL Cars.tCCrssMax=4 Cars.tCCrssMin=1 LV1Pedestrian2.tPCrssMin=0 LV1Pedestrian2.tPCrssMax=10 t(0)-tTL<=0 t(0)-Cars.tc<=0 t(0)-TrafficLights.tTL<=0 t(0)-LV1Pedestrian2.tp<=0 t(0)-LV1Pedestrian2.tTL<=0 tTL-t(0)<=55 tTL-Cars.tc<=0 Cars.tc-TrafficLights.tTL<=0 TrafficLights.tTL-LV1Pedestrian2.tp<=0 LV1Pedestrian2.tp-LV1Pedestrian2.tTL<=0 LV1Pedestrian2.tTL-tTL<=0
Transition: TrafficLights._id8 -> TrafficLights.cRed_pGreen {1; pGreen!; 1;} LV1Pedestrian2.CheckTL -> LV1Pedestrian2._id27 {1; pGreen?; 1;}
State: Cars.Idle TrafficLights.cRed_pGreen LV1Pedestrian2._id27 Cars.tCCrssMax=4 Cars.tCCrssMin=1 LV1Pedestrian2.tPCrssMin=0 LV1Pedestrian2.tPCrssMax=10 t(0)-tTL<=0 t(0)-Cars.tc<=0 t(0)-TrafficLights.tTL<=0 t(0)-LV1Pedestrian2.tp<=0 t(0)-LV1Pedestrian2.tTL<=0 tTL-t(0)<=55 tTL-Cars.tc<=0 Cars.tc-TrafficLights.tTL<=0 TrafficLights.tTL-LV1Pedestrian2.tp<=0 LV1Pedestrian2.tp-LV1Pedestrian2.tTL<=0 LV1Pedestrian2.tTL-tTL<=0
Transition: LV1Pedestrian2._id27 -> LV1Pedestrian2.Crossing {1; pCrss!; tp = 0;} Cars.Idle -> Cars.Idle {1; pCrss?; 1;}
Returns:

str – Original raw string of the trace.

property states: List[List[str]]
property clock_constraints: List[ClockZone]
property transitions: List[Transition]
property actions: List[str]
property untime_pattern: List[str]
property global_variables: List[GlobalVar]
filter_by_actions(focused_actions: List[str]) → SimTrace[source]

Filter the transitions by actions.

Parameters:

focused_actions (List[str], optional) – actions that you take cares of.

Returns:

SimTrace – The filtered SimTrace.

save_raw(file_name: str) → None[source]

Save raw data to file.

Parameters:

file_name (str) – file name.

save(file_name: str) → None[source]

Save self.__str__() to file.

Parameters:

file_name (str) – file name.

trim_transitions(model_path: str) → None[source]

It reads the .xml file and gets the mapping from formal parameters to real parameters, then it replaces the formal parameters in the transitions with the real parameters.

Parameters:

model_path (str) – The path of the .xml file.

Raises:

ValueError – When the .xml file is invalid.

class pyuppaal.tracer.OneClockZone(clock1: str, clock2: str, is_equal: bool, bound_value: int)[source]

Bases: object

Represents a single clock zone constraint in a timed automaton.

This class encapsulates a constraint between two clock variables, typically used in the context of timed automata. It specifies a relationship between two clocks and a bound on their difference.

property clock1: str

clock1 - clock2 < or ≤ bound_value

Returns:

str – Name of the first clock variable.

property clock2: str

clock1 - clock2 < or ≤ bound_value

Returns:

str – Name of the second clock variable.

property is_equal: bool

clock1 - clock2 < or ≤ bound_value

Returns:

bool – is_equal

property bound_value: int

clock1 - clock2 < or ≤ bound_value

Returns:

int – bound_value

class pyuppaal.tracer.ClockZone(clockzones: List[OneClockZone])[source]

Bases: object

Composed by List of OneClockZone.

property clockzones: List[OneClockZone]

List of OneClockZone.

Returns:

List[OneClockZone] – The list of OneClockZone objects.

class pyuppaal.tracer.Edges(start_location: str, end_location: str, guard: str, sync: str, update: str)[source]

Bases: object

Edges are components of Transition. One Transition contains at least one Edge. If more than 1 Edges are contained, it means that there is sync occurred. On this condition, Edges[0] is the sender(!) and others are reveivers(?).

An Edge looks like this: process.start_location -> process.end_location: {guard, sync, update}. A Transition looks like this: Transition: LV1Pedestrian2.Idle -> LV1Pedestrian2.CheckTL {1; pWantCrss!; 1;} TrafficLights.cRed_pGreen -> TrafficLights._id8 {1; pWantCrss?; 1;}

property start_location: str

Gets the start location (state) of the edge.

Returns:

str – The start location of the edge.

property end_location: str

Gets the end location (state) of the edge.

Returns:

str – The end location of the edge.

property guard: str

Gets the guard condition of the edge.

The guard condition must be true for the transition to occur. If the guard is ‘1’, it implies the absence of a specific guard condition.

Returns:

str – The guard condition of the edge.

property has_guard: bool

Determines if the edge has a guard condition.

Returns:

bool – True if the edge has a guard condition, False otherwise.

property sync: str

Gets the synchronization action of the edge.

The synchronization action is used for coordinating transitions between different processes.

Returns:

str – The synchronization action of the edge.

property update: str

Gets the update action of the edge.

The update action is executed when the transition occurs.

Returns:

str – The update action of the edge.

property process: str

Gets the process to which the edge belongs.

Returns:

str – The name of the process.

property is_sync: bool

Determines if the edge involves synchronization.

Returns:

bool – True if the edge involves synchronization, False otherwise.

property sync_type: str

Gets the type of synchronization of the edge.

The synchronization type can be ‘send’ (denoted by ‘!’) or ‘receive’ (denoted by ‘?’).

Returns:

str – The synchronization type (‘send’, ‘receive’, or None if not applicable).

property sync_symbol: str

Gets the symbol used for synchronization in the edge.

The symbol represents the event or message involved in the synchronization.

Returns:

str – The synchronization symbol, or None if synchronization is not applicable.

class pyuppaal.tracer.Transition(sync: str, start_process: str, end_process: List[str], edges: Optional[List[Edges]] = None)[source]

Bases: object

One Transition contains at least one Edge. If more than 1 Edges are contained, it means that there is sync occurred. On this condition, Edges[0] is the sender(!) and others are reveivers(?).

An Edge looks like this: process.start_location -> process.end_location: {guard, sync, update}. A Transition looks like this: Transition: LV1Pedestrian2.Idle -> LV1Pedestrian2.CheckTL {1; pWantCrss!; 1;} TrafficLights.cRed_pGreen -> TrafficLights._id8 {1; pWantCrss?; 1;}

property sync: str

Gets the synchronization symbol of the transition.

Returns:

str – The synchronization symbol.

property start_process: str

Gets the start process of the transition.

Returns:

str – The name of the start process.

property end_process: List[str]

Gets the end processes of the transition.

Returns:

List[str] – The names of the end processes.

property edges: List[Edges]

Gets the edges that make up the transition.

Returns:

List[Edges] – The list of edges.

property action: str

Gets the action associated with the transition, typically the sync symbol.

Returns:

str – The action of the transition.

class pyuppaal.tracer.GlobalVar(variables_name: List[str], variables_value: List[float])[source]

Bases: object

Represents global variables in a process model.

Global variables are shared across different components of the model and can be used to store and manipulate data that is globally accessible.