ALL API

pyuppaal.pyuppaal

PYUPPAAL

pyuppaal.pyuppaal.set_verifyta_path(verifyta_path: str)

Set verifyta path, and you will get tips if verifyta_path is invalid. This function will check whether verifyta_path is valid by following steps: 1. run ‘{verifyta_path} -h’ with cmd 2. check whether ‘-h [ –help ]’ is in the result

Parameters:

verifyta_path (str) – absolute path to verifyta

class pyuppaal.pyuppaal.DeveloperTools

Bases: object

给开发者用的开发工具, 用于内部测试, 可以在多平台进行测试。 普通用户无法使用。

static get_verifyta_path_dev(uppaal_version: int = 5)

static set_verifyta_path_dev(uppaal_version: int = 4)

给开发者测试用的，用户别用这个

Returns:

None

pyuppaal.umodel

umodel

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

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

创建一个新的uppaal xml文件

Parameters:

file_name (str) – file name

Returns:

UModel – a new UModel instance.

write_xml_tree(path: str, indent: int) → None

Write the xml tree to disk

Parameters:

• path (str) – target xml file storing the model

• indent (int) – indentation of the xml, must >= 0

Returns:

None.

save_as(new_path: str, indent=4) → UModel

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

Parameters:

• new_path (str) – target model path

• indent (int) – indentation of the created xml

Returns:

UModel – self.

save() → UModel

Save the current model.

Returns:

UModel – self.

copy_as(new_path: str) → UModel

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, timeout: Optional[float] = None) → str

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.

• timeout (float, optional) – timeout in seconds for the verification command execution.

Returns:

str – terminal verify results for self.

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

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.

• timeout (float, optional) – timeout in seconds for the verification command execution.

Returns:

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

get_communication_graph(save_path=None, is_beautify=True) → Mermaid

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

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

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

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

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)

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

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]

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

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)

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)

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)

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

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

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.monitors

class pyuppaal.monitors.Monitors

Bases: object

static fault_monitor(name: str, fault_name: str, init_ref: int) → Template

_summary_

Parameters:

• name (str) – the name of the returned Template.

• fault_name (str) – the name of the fault.

• init_ref (int) – the initial location id of the returned Template. You can set init_ref by UModel.max_location_id + 1.

Returns:

Template – _description_

static observer_suffix_monitor(name: str, suffix_sequence: List[str], sigma_o: List[str], sigma_un: List[str], init_ref: int) → Template

observer suffix monitor Creates an observer suffix monitor template.

Parameters:

• name (str) – The name of the returned Template.

• suffix_sequence (List[str]) – The sequence of suffix events to be observed. These events will be monitored in sequence.

• sigma_o (List[str]) – The set of observable events. This includes all events that the monitor could potentially observe.

• init_ref (int) – the initial location id of the returned Template. You can set init_ref by UModel.max_location_id + 1.

Returns:

Template –

The constructed monitor template.

This template contains a series of locations and transitions that describe how to transition states based on the given suffix sequence and the set of observable events.

static obs_after_fault_monitor(name: str, suffix_sequence: List[str], sigma_o: List[str], sigma_un: List[str], fault: str, init_ref: int) → Template

Parameters:

• name (str) – the name of returend Template.

• suffix_sequence (List[str]) – suffix sequence.

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

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

• fault (str) – fault name.

• init_ref (int) – the initial location id of the returned Template. You can set init_ref by UModel.max_location_id + 1.

Returns:

Template – monitor template

static input_after_fault_monitor(name: str, identified_faults: List[str], protecting_events: List[str], sigma_fault: List[str], sigma_control: List[str], control_length: int, init_ref: int) → Template

Parameters:

• name (str) – the name of returend Template.

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

• protecting_events (List[str]) – sequence of evnets that should be immediately applied after the faults are identified.

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

• control_length (int) – the longest control limits.

• init_ref (int) – the initial location id of the returned Template. You can set init_ref by UModel.max_location_id + 1.

Returns:

Template – monitor template

static tolerance_checker_monitor(name: str, identified_faults: List[str], protecting_events: List[str], sigma_fault: List[str], sigma_control: List[str], control_sequence: List[str], init_ref: int) → Template

Parameters:

• name (str) – the name of returned Template.

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

• protecting_events (List[str]) – sequence of evnets that should be immediately applied after the faults are identified.

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

• control_length (int) – the longest control limits.

• init_ref (int) – the initial location id of the returned Template. You can set init_ref by UModel.max_location_id + 1.

Returns:

Template – monitor template

static input_template(name: str, signals: List[Tuple[str, str, str]], init_ref: int) → Template

>>> monitor = Template.construct_input_template(xxx)
>>> umodel = UModel(xxx)
>>> umodel.add_template(monitor: Tempalte)
>>> umodel.add_template_to_system(str: template_name)

Parameters:

• name (str) –

• signals (Union[List[str], List[Tuple[str, str, str]]]) –

  input signals, can accept discrete event sequence (List[str]), or timed event sequence (List[Tuple[str, str, str]]) List[str] xxxx discrete event sequence, example: [‘a’, ‘b’, ‘c’] List[Tuple[str, str, str]] xxxx timed event sequence, stands for List[(action_name, guard, invariant)]

  example: [(‘a’, ‘t>=10’, ‘t<=10’), (‘b’, ‘t>=20’, ‘t<=20’), (‘c’, ‘t>=30’, ‘t<=30’)] [(‘a’, ‘t1>=10’, ‘t1<=10’), (‘b’, ‘t2>=20’, ‘t2<=20’), (‘c’, ‘t3>=30’, ‘t3<=30’)] you can use any guard and invariant expression

• init_ref (int) – the initial location id of the returned Template. You can set init_ref by UModel.max_location_id + 1.

Returns:

Template – monitor template

static observer_template(name: str, signals: List[Tuple[str, str, str]], sigma_o: List[str], init_ref: int, strict: bool = False, allpattern: bool = False) → Template

sigma_o: the set of observable events

>>> monitor = Template.construct_observer_template(xxx)
>>> umodel = UModel(xxx)
>>> umodel.add_template(monitor: Tempalte)
>>> umodel.add_template_to_system(str: template_name)
<template>
    <name>Monitor</name>
    <location> </location>
    <location>init ref="id47"/>
    <transition> </transition>
</template>

pyuppaal.verifyta

verifyta

class pyuppaal.verifyta.Verifyta

Bases: object

This is a singleton class that help to use verifyta command.

property verifyta_path: str

Get current verifyta path.

Returns:

str – current verifyta path.

static get_env() → str

get_uppaal_version() → int

set_verifyta_path(verifyta_path: str) → None

Set the verifyta path before using pyuppaal. This function will check the validation of the verifyta_path automatically by the following steps:

1. run cmd with verifyta_path -v;

2. check whether ‘UPPAAL’ in res.

Example paths:

1. Windows: path_to_uppaalbin-Windowsverifyta.exe

2. Linux : path_to_uppaal/bin-Linux/verifyta

3. macOS : path_to_uppaal/bin-Darwin/verifyta

Parameters:

verifyta_path (str) – (absolute) path to verifyta

Raises:

ValueError – if verifyta_path is invalid.

Returns:

None

cmd(cmd: str, timeout: Optional[float] = None) → str

Run common command with cmd, you can easily ignore the verifyta path.

Parameters:

• cmd (str) – command to run.

• timeout (float, optional) – timeout in seconds for the command execution.

Raises:

• ValueError – if verifyta_path is not set.

• ValueError – if cmd got stderr and not as expected.

• TimeoutError – if command execution times out.

Returns:

str – the output of the input command.

compile_to_if(model_path: str) → str

Compile the .xml model_path to a .if file and return the content of the .if file.

Parameters:

model_path (str) – .xml model file.

Raises:

• FileNotFoundError – model_path not found.

• ValueError – model_path is not a .xml.

Returns:

str – path to .if file.

verify(model_path: str, trace_path: Optional[str] = None, verify_options: str = '-t 1', keep_tmp_file=True, timeout: Optional[float] = None) → str

Verify model and return the verify result as list. This is designed for advanced UPPAAL user.

Verify models and return the verify results as list. For trace_path param, both .xtr and .xml`(DBM) files are supported. WARNING: Note that `-f xx.xtr or -X xx.xml should be used together with -t options, otherwise you may fail to save the path files. WARNING: -t option must be set for verify_options, which is set by default `verify_options = ‘-t 1’`(shortest), otherwise counter-example file may not be created.

Examples

>>> Verifyta().set_verifyta_path(VERIFYTA_PATH)
>>> model_path = os.path.join(ROOT_DIR, 'demo1.xml')
>>> trace_path = os.path.join(ROOT_DIR, 't1.xtr')
>>> Verifyta().verify(model_path, trace_path=trace_path, verify_options='-t 1 -o 0')

Parameters:

• model_path (str) – model path to be verified.

• trace_path (str, optional) – target trace path, both .xtr and .xml`(DBM) are supported. Defaults to None, which will create `.xtr path.

• verify_options (str, optional) – verify options that are proveded by verifyta, and you can get details by run verifyta -h in your terminal. Defaults to ‘-t 1’, returning the shortest trace.

• keep_tmp_file (bool, optional) – whether to keep temporary trace files. Defaults to True.

• timeout (float, optional) – timeout in seconds for the verification command execution.

Raises:

• ValueError – if tracer file is not xml or xtr.

• TimeoutError – if verification command times out.

Returns:

str – terminal verify results for .xml model.

pyuppaal.tracer

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

class pyuppaal.tracer.SimTrace(trace_string: str)

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

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

Save raw data to file.

Parameters:

file_name (str) – file name.

save(file_name: str) → None

Save self.__str__() to file.

Parameters:

file_name (str) – file name.

trim_transitions(model_path: str) → None

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)

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

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)

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)

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

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.

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)

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

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)] = [])

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

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

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

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.build_cg

author: Yining She

class pyuppaal.build_cg.Mermaid(mermaid_str: str)

Bases: object

class Mermaid

property mermaid_str: str

Raw mermaid string.

Returns:

str – raw mermaid string.

property mermaid_list: List[List[str]]

List of [source, edge_name, target]

Returns:

List[List[str]] – List of [source, edge_name, target].

beautify(join_str: str = ',') → str

Beautify Mermaid by merging edges with the same source and target.

FROM: `mermaid graph TD TrafficLights--cGreen-->Cars TrafficLights--cYellow-->Cars LV1Pedestrian2--pCrss-->Cars `

TO: `mermaid graph TD TrafficLights--cGreen,cYellow-->Cars LV1Pedestrian2--pCrss-->Cars `

Parameters:

join_str (str, optional) – join flag. Defaults to ‘,’.

Returns:

str – beautified mermaid string.

remove(components: Union[str, List[str]]) → str

Remove mermaid lines that contains components.

Parameters:

excluded_components (str | List[str]) – components to remove.

Returns:

str – mermaid string.

export(target_file: str) → str

Export mermaid to a <.md | .svg | .pdf | .png> file.

Parameters:

target_file (str) – <.md | .svg | .pdf | .png>.

Returns:

str – path to the target file.

pyuppaal.build_cg.get_str_before(string: str, label: str)

Returns:

the substring of ‘string’ before the first occurrence of ‘label’.

If ‘label’ doesn’t exist in ‘string’, raise error.

pyuppaal.build_cg.get_str_after(string, label)

Returns:

the substring of ‘string’ after the first occurence of ‘label’.

If ‘label’ doesn’t exist in ‘string’, raise error.

class pyuppaal.build_cg.Node(name, temp_name, sig_in, sig_out)

Bases: object

A instance of a Xml Template.

Parameters:

• strname – the name of the instance

• temp_name (str) – the name of the template

• sig_in (list) – a list of names of signals enter the node

• sig_out (list) – a list of names of signals sent by the node

class pyuppaal.build_cg.XmlTemplate(code)

Bases: object

Used to define a template in the xml. Input is the corresponding code in the xml. :param str name: name of the template :param list sig_in: a list of signals enter the template :param list sig_out: a list of signals sent by the template :param dict params: relate input signal variable with its index in the input arguments

init_name()

Get the name from self.code

get_all_sync()

Using label “synchronisation” to find all signal names used in the template.

get_param()

Find the signal variables that come in through input.

And store the name of them with their index in the input arguments, which can be used to find the actual signal variable when give input argument.

get_instance(name, para_string)

Return and initialize an instance of the template using the input argument.

Parameters:

• name (str) – name of the new instance

• para_string (str) – code of the input argument

class pyuppaal.build_cg.XmlReader(filename)

Bases: object

Used to read the xml file and take advantage of classes defined above.

init_template()

Find all templates in the code and init a ‘XmlTemplate’ for each of them.

get_notes()

By reading the ‘system’ part in the xml to init all time-automata instances. :return: a list fo ‘Node’.

pyuppaal.build_cg.add_edge(a, b, label='')

pyuppaal.build_cg.build_cg_code(nodes)

Given a list of ‘Node’, build the CG graph and print the markdown code.

pyuppaal.build_cg.build_cg(filename)