We describe PyECDAR fonctions that are called inside the Python shell.

### Loading, system construction and saving

The tool is imported with the python command: `from pyecdar import loadModel`

To run it the shell must either be launched from pyecdar directory or the tool must have been installed in the system. See the section Installation.

A XML model file is loaded inside a variable via the command:

`workspace = loadModel(`

*filename*)

Each template in the model can be loaded in a separate variable:

`spec = workspace.getSpecification(`

if the template is a timed specification, or*template_name*)

`game = workspace.getTimedGame(`

if the template is a timed game associated to a T-AdaCTL formula (see the syntax below).*template_name,objective*)

Complex systems of timed specifcations are build by combining the specifications already loaded using Python standard operators. The results of each operation is a new specification, which allows to use the operators in an algebraic expression.

`spec1 | spec2`

computes the parallel composition

`spec1`

& `spec2`

computes the conjunction

`spec1`

/ `spec2`

computes the quotient

If needed the newly generated templates (games or specification) can be added to the workspace:

`workspace.addTemplate(template)`

This allows to save the model with the new templates in an XML file:

`workspace`

.save(*filename*)

*filename* may be omitted if the user wants to overwrite the previous XML file. Note that the templates are saved without positions for graphical elements. Therefore if the model is open in Uppaal or Ecdar all the elements (locations and transitions will overlap).

### Timed specification Checking

`spec.isSpecification()`

returns True or False, if the template syntax corresponds to a specification:

- no features
- all transitions are synchronized
- inputs and outputs are disjoint
- the automata is deterministic and input enabled.

returns True or False, if the template is action deterministic.`spec`

.isDeterministic()

returns True or False, if the template is input enabled.`spec`

.isInputEnabled()

`new_`

computes a new model in which all the constants used in the DBMs are scaled by an integer factor.`spec`

= `spec`

.scale(self,factor)

`spec.sameAlphabet(spec2)`

Checks if the two specifications have the same alphabet of actions. This is a necessary condition to computes the conjunction.

`spec.composable(spec2) `

Checks if the two specifications have disjoint alphabet of output actions. This is a necessary condition to computes the parallel composition.

`spec.quotientable(spec2)`

Checks if the specification spec1 can be quotiented by spec2.

###### Consistency checking

returns True or False, if the specification is consistent. This implies to solve a consistency game.`spec`

.isConsistent()

where `spec`

.isRobustConsistent(*delta*)*delta* is a float value. Returns True or False, if the specification is robustly consistent for the value *delta*. This implies to solve a robust consistency game.

where `spec`

.maxRobustConsistent(*delta_max*,*confidence*)*delta_max* is an integer value, sufficiently big to know that the specification is not robustly consistent for this value (e.g. the maximum constant used in the model), and *confidence* is a float value that defines the precision of the computation. Returns the value *delta* such that the specification is robustly consistent. This function uses the CEGAR algorithm for parametric robustness.

same as previously, but using a binary search algorithm instead.`spec`

.maxRobustConsistentBS(*delta_max,confidence*)

returns the timed game used to check the consistency of the specification.`spec`

.getConsistencyGame()

returns the robust consistency game used to check robust consistency. `spec`

.getRobustConsistencyGame(*delta*,*param*)*delta* is either an integer value, or a parameter name. By default *delta* is a parameter named “delta”. *param* is only useful if *delta* is a parameter, in which case *param* is the initial value of *delta*. By default *param*=0.

**Compatibility (or usefulness checking)**

returns True or False, if the specification is useful, which means that its components are compatible. This solves a usefulness game whose objective is to avoid the set of `spec`

.isUseful(*bad_locations*)*bad_locations.*

where `spec`

.isRobustUseful(*delta*,

)*bad_locations**delta* is a float value. Returns True or False, if the specification is robustly useful for the value *delta*. This implies to solve a robust usefulness game.

where `spec`

.maxRobustUseful(*delta_max*,*confidence,*)

*bad_locations*

*delta_max*is an integer value, sufficiently big to know that the specification is not robustly useful for this value (e.g. the maximum constant used in the model), and

*confidence*is a float value that defines the precision of the computation. Returns the value

*delta*such that the specification is robustly useful. This function uses the CEGAR algorithm for parametric robustness.

same as previously, but using a binary search algorithm instead.`spec`

.`maxRobustUseful`

BS(*delta_max*,*confidence*)

returns the timed game used to check the usefulness of the specification.`spec`

.getUsefulnessGame()

returns the robust consistency game used to check robust usefulness. `spec`

.getRobustUsefulnessGame(*delta*,*param*)*delta* is either an integer value, or a parameter name. By default *delta* is a parameter named “delta”. *param* is only useful if *delta* is a parameter, in which case *param* is the initial value of *delta*. By default *param*=0.

###### Refinement and satisfaction checking

`spec.refine(big_spec)`

return True or False, if the specification spec refines the specification big_spec. The refinement check is also used to check if an implementation satisfies a specification. The python operators <= and >= can also be used to check the refinement:

`spec <= big_spec`

or `big_spec >= spec`

are equivalent to the function call above.

`spec.robSat(big_spec,`

checks if spec is a robust implementation of big_spec for a perturbation of *delta*)*delta*

`spec.maxRobSat(big_spec,`

computes the maximum perturbation allowed by the implementation spec in order to robustly satisfies the specification big_spec. *delta_max*,*confidence*)*delta_max* is an integer value, sufficiently big to know that the implementation is not robust, and *confidence* is a float value that defines the precision of the computation.

`spec.implemPerturbation(`

Applies a perturbation to the guards of the implementation. *delta*,*param*)*delta* is either an integer value, or a parameter name. By default *delta* is a parameter named “delta”. *param* is only useful if *delta* is a parameter, in which case *param* is the initial value of *delta*. By default *param*=0.

###### T-AdaCTL checking

The logic T-AdaCTL is introduced in [CLST13]. The grammar of the logic used by PyECDAR is the following:

`tadactlformula := ( "[" `

*featureExpression* "]" )? stateFormula

stateFormula := "A" pathFormula | "E" pathFormula) | orFormula

pathFormula := ("("featureFormula ")" ["U"|"W"] interval? "(" featureFormula ")") |

("<>" interval? "(" featureFormula ")") |

("[]" "(" featureFormula ")")

orFormula := andFormula ("or" orFormula)*

andFormula := notFormula ("and" andFormula)*

notFormula := ("not")? atomicFormula

atomicFormula := "true" | "false" | *guard* | *location* | "(" tadactlformula ")"

*featureExpression* is an expression over feature variables, *guard* is an expression that defines a DBM and *location* is the name of a location in the template.

To solve a timed game launch the command:

`game.solve() `

This solves the game and prints the results.

`game.print_results(all_states)`

Prints the result of the game. If the parameter all_states is true (by default it’s false) all the winning states are printed. Otherwise only the winning features for the initial state are printed.

Returns the BDD with the winning features for the initial state.

game.get_winning_features()