First, start your python shell. Then inside the python shell run the following commands.
Loading the tool:
from pyecdar import loadModel
Loading the model into the workspace:
Choose a workspace name (for instance W), and load a UPPAAL model from an XML file:
W = loadModel("university.xml")
The loadModel function takes as parameter a string that is the path of the file.
Load specifications from TIOA templates:
A UPPAAL model file generated by ECDAR may contain several templates, each described by a Timed Input/Output Automata (TIOA). Each template defines a timed specification that can be loaded inside the shell and assign to a variable.
M = W.getSpecification("Machine")
loads the template named “Machine” from the workspace and assigns it to a variable also named “M”.
We can do the same for two other specifications:
R = W.getSpecification("Researcher")
MI = W.getSpecification("MachineImpl")
Refinement checking:
We can check the refinement between two specifications previously loaded. The easiest way is to use the operators <= or >=.
MI <= M or M >= MI
are two equivalent commands to check that the specification MI refines M. The result is true. As MI is the specification of an implementation this check also corresponds to the satisfaction check between an implementation and a specification.
Consistency checking:
Checking consistency is equivalent to determining if a specification admits an implementation. This is performed in PyECDAR by solving a timed game. To check the consistency of a specification run the command:
M.isConsistent()
Conjunction:
We can compute the conjunction of two specifications that have the same alphabet. To check it with PyECDAR run:
M.sameAlphabet(MI) or equivalently MI.sameAlphabet(M)
Then the conjunction of the two specifications can be built using the operator &. The result is a new specification that can be assigned to a variable:
S = M & MI
Parallel composition:
Two specifications are composable if their alphabets of output actions are disjoint. To check this in PyECDAR run:
M.composable(R) or equivalently R.composable(M)
Two composable specifications can be composed through parallel composition. The commutative operator | can be used in PyECDAR to build the parallel composition. This yields a new specification that can be assign to a new variable.
T = M | R
Compatibility checking:
Incompatibilities must be explicit in timed specifications. By default the tool assumes that a universal location name UNIV is used in the TIOA templates to model undesirable states. Then, two specifications are compatible if their exists at least one environment in which they can work together, such that no undesirable location is reached. Therefore checking compatibility is equivalent to finding a compatible environment for the parallel composition of the two specifications. We call this check usefulness checking, and it can be performed by solving a timed game. In PyECDAR run the command:
T.isUseful()
to check if T is useful, which means that M and R are compatible.
Robust satisfaction:
Robustness is achieved when a specification is tolerant with respect to small timings perturbations. We can add such perturbations in an implementation model. For instance the timings of the implementation MI can be perturbed by 0.5 time units:
MI_0_5 = MI.implemPerturbation(0.5)
This creates a new specification model that is assigned to the variable MI_0_5. Now we check if this perturbation is allowed by the specification using the refinement check:
MI_0_5
which proves that the implementation MI robustly satisfies the specification M for up to 0.5 time units perturbation.
Finally we can compute what is the maximum perturbation allowed, either using:
MI.maxRobSat(M,8,0.1)
which computes the maximum perturbation with a parametric CEGAR technique, assuming that 8 is a greater bound and 0.1 is the desired precision; or alternatively:
MI.maxRobSatBS(M,8,0.1)
which computes the same value with a binary search technique.
Robust consistency:
By extension a specification is robust consistent if it admits a robust implementation. This amounts to check a robust timed game.
M.isRobustConsistent(1.1)
checks that M admits at least an implementation that is robust for a 1.1 perturbation.
We can also computes the maximum perturbation such that a specification is robust consistent, using either:
Machine.maxRobustConsistent(8,0.1)
to use the parametric CEGAR technique, or:
Machine.maxRobustConsistentBS(8,0.1)
to use binary search.
Robust compatibility:
Similarly we consider that two specifications are robust compatible if there exists an environment that is compatible even when subject to some perturbation. We can check this is PyECDAR by playing a robust timed game with the command:
T.isRobustUseful(1.1)
As for robust consistency we can use either the parametric CEGAR technique or the binary search technique to compute the maximum perturbation allowed:
T.maxRobustUseful(8,0.1)
T.maxRobustUsefulBS(8,0.1)
