pyuppaal 0.1.13

A research tool that can simulate, verify or modify UPPAAL models with python. It can also help to analyze counter-examples in .xml format

Introduction

pyUPPAAL is a research tool that can simulate, verify and modify UPPAAL models with python. It can also help to analyze counter-examples in .xml format. Note that the implementations are based on verifyta and the built-in xml package. With this package, you can do

1. run any UPPAAL commands with multi-process that is valid with verifyta.

2. modify a .xml model, including templates, declarations, system declarations, and queries. It has a powerful method find_all_patterns that can get all different untimed traces that can explain current inputs-obs.

3. analyze a counter-example file, and return input-observation-based analysis.

4. analyze the SMC simulation results.

Quickstart

Something to prepare

Installation

To install pyuppaal, simply run this simple command:

python -m pip install pyuppaal

Get started

Begin by importing the pyuppaal module:

import pyuppaal as pyu

Set verifyta path first!

You MUST set the verifyta path firstly before verification!

pyu.set_verifyta_path(r'C:/Users/22215/OneDrive/Software/UPPAAL/bin-Windows/verifyta.exe')

Try some simple verification!

Choose the model file you want to verify, as well as the path you want to save the result, you can complete a simple verifivation:

# Two paths you choose
p1_model_path = 'verifyta_demo1.xml'
p1_trace_path = 'verifyta_demo1_trace.xml'
# The result will be written in the target file, and the procedure information is saved in res1
res1 = pyu.simple_verify(model_path=p1_model_path, trace_path=p1_trace_path)
print(res1)

## OUTPUT:
## [('set UPPAAL_COMPILE_ONLY=&&C:/Users/22215/OneDrive/Software/UPPAAL/bin-Windows/verifyta.exe -t 1 -X verifyta_demo1_trace verifyta_demo1.xml', 'Options for the verification:\n  Generating shortest trace\n  Search order is breadth first\n  Using conservative space optimisation\n  Seed is 1662285315\n  State space representation uses minimal constraint systems\n\x1b[2K\nVerifying formula 1 at /nta/queries/query[1]/formula\n\x1b[2K -- Formula is NOT satisfied.\nXMLTrace outputted to: verifyta_demo1_trace1.xml\n')]

Get timed trace easily

You can also get a timed trace with the same params:

simtracer = pyu.get_timed_trace(p1_model_path, p1_trace_path,hold=True)
print(simtracer)

## OUTPUT:
## State [0]: ['P2.A']
## global_variables [0]: []
## Clock_constraints [0]: [t(0) - P2.t ≤ 0; P2.t - t(0) ≤ 10; ]
## transitions [0]: None: P2.A -> P2.B
## -----------------------------------
## State [1]: ['P2.B']
## global_variables [1]: []
## Clock_constraints [1]: [t(0) - P2.t ≤ -10; P2.t - t(0) ≤ 10; ]
## transitions [1]: None: P2.B -> P2.C
## -----------------------------------
## State [2]: ['P2.C']
## global_variables [2]: []
## Clock_constraints [2]: [t(0) - P2.t ≤ -10; P2.t - t(0) ≤ 20; ]

Find a pattern

You can quickly find a pattern with plentiful params, e.g., inputs, observations, actions:

model_path = 'pyuppaal_demo_PipeNet.xml'
# input at 0 and 1000
inputs = pyu.TimedActions(actions=['input_ball', 'input_ball'], lb=[0, 1000], ub=[0,1000])
# observe at 500 and 1550
observations = pyu.TimedActions(actions=['exit1', 'exit2'], lb=[500, 1550], ub=[500, 1550])
# concerned actions
hidden_actions = ['hidden_path1', 'hidden_path2', 'hidden_path3', 'hidden_path4', 'hidden_path5', 'hidden_path6']
input_actions = ['input_ball']
observe_actions = ['exit1','exit2','exit3']
focused_actions = list(set(hidden_actions+input_actions+observe_actions))
# find a pattern
pyu.find_a_pattern(inputs, observations, observe_actions=observe_actions, focused_actions=None, hold=False)

## OUTPUT:
## ('E<> Monitor0.pass',
##  ['input_ball',
##   'input_ball',
##   'hidden_path1',
##   'hidden_path3',
##   'exit1',
##   'input_ball',
##   'input_ball',
##   'hidden_path1',
##   'hidden_path4',
##   'exit2'])

Find all patterns

You can also find all patterns:

pyu.find_all_patterns(inputs, observations, observe_actions=observe_actions, hold=False, max_patterns = 2)

## OUTPUT
## [('E<> Monitor0.pass',
##   ['input_ball',
##    'input_ball',
##    'hidden_path1',
##    'hidden_path3',
##    'exit1',
##    'input_ball',
##    'input_ball',
##    'hidden_path1',
##    'hidden_path4',
##    'exit2']),
##  ('E<> Monitor0.pass && !Monitor1.pass',
##   ['input_ball',
##    'input_ball',
##    'hidden_path1',
##    'hidden_path3',
##    'exit1',
##    'input_ball',
##    'input_ball',
##    'hidden_path2',
##    'hidden_path5',
##    'exit2'])]

Generate communication graph

You can easily generate your communication graph to plentiful type, e.g., .md, .png, .svg and .pdf:

model_path = r'C:\Users\22215\OneDrive\Coding\Github\pyuppaal\src\tests\Pedestrian.xml'
# just take .png as an example
save_path = r'C:\Users\22215\OneDrive\Coding\Github\pyuppaal\src\tests\Pedestrian.png'
pyu.get_communication_graph(model_path,save_path)