Queries

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(template_name) if the template is a timed specification, or

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

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.

spec.isDeterministic() returns True or False, if the template is action deterministic.

spec.isInputEnabled() returns True or False, if the template is input enabled.

new_spec = spec.scale(self,factor) computes a new model in which all the constants used in the DBMs are scaled by an integer 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

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

spec.isRobustConsistent(delta) where 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.

spec.maxRobustConsistent(delta_max,confidence) where 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.

spec.maxRobustConsistentBS(delta_max,confidence) same as previously, but using a binary search algorithm instead.

spec.getConsistencyGame() returns the timed game used to check the consistency of the specification.

spec.getRobustConsistencyGame(delta,param) returns the robust consistency game used to check robust consistency. 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)

spec.isUseful(bad_locations) 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 bad_locations.

spec.isRobustUseful(delta,bad_locations) where 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.

spec.maxRobustUseful(delta_max,confidence,bad_locations) where 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.

spec.maxRobustUsefulBS(delta_max,confidence) same as previously, but using a binary search algorithm instead.

spec.getUsefulnessGame() returns the timed game used to check the usefulness of the specification.

spec.getRobustUsefulnessGame(delta,param) returns the robust consistency game used to check robust usefulness. 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,delta) checks if spec is a robust implementation of big_spec for a perturbation of delta

spec.maxRobSat(big_spec,delta_max,confidence) computes the maximum perturbation allowed by the implementation spec in order to robustly satisfies the specification big_spec. 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(delta,param) Applies a perturbation to the guards of the implementation. 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.

game.get_winning_features() Returns the BDD with the winning features for the initial state.