We describe PyECDAR fonctions that are called inside the Python shell.<\/p>\n
The tool is imported with the python command: A XML model file is loaded inside a variable via the command: Each template in the model can be loaded in a separate variable:<\/p>\n 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.<\/p>\n If needed the newly generated templates (games or specification) can be added to the workspace:<\/p>\n This allows to save the model with the new templates in an XML file:<\/p>\n filename<\/em> 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).<\/p>\n Compatibility (or usefulness checking)<\/strong><\/p>\nfrom pyecdar import loadModel<\/code>
\nTo 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>.<\/p>\n
\nworkspace = loadModel(filename<\/em>)<\/code><\/p>\nspec = workspace.getSpecification(template_name<\/em>)<\/code> if the template is a timed specification, or<\/p>\ngame = workspace.getTimedGame(template_name,objective<\/em>)<\/code> if the template is a timed game associated to a T-AdaCTL formula (see the syntax below<\/a>).<\/p>\nspec1 | spec2<\/code>\u00a0\u00a0 computes the parallel composition<\/p>\nspec1<\/code>\u00a0&\u00a0<\/code>spec2<\/code>\u00a0\u00a0 computes the conjunction<\/p>\nspec1<\/code>\u00a0\/\u00a0<\/code>spec2<\/code>\u00a0\u00a0 computes the quotient<\/p>\nworkspace.addTemplate(template)<\/code><\/p>\nworkspace<\/code>.save(filename<\/em>)<\/code><\/p>\nTimed specification Checking<\/h3>\n
spec.isSpecification()<\/code> returns True or False, if the template syntax corresponds to a specification:<\/p>\n\n
spec<\/code>.isDeterministic()<\/code> returns True or False, if the template is action deterministic.<\/p>\nspec<\/code>.isInputEnabled()<\/code> returns True or False, if the template is input enabled.<\/p>\nnew_spec<\/code> = spec<\/code>.scale(self,factor)<\/code> computes a new model in which all the constants used in the DBMs are scaled by an integer factor.<\/p>\nspec.sameAlphabet(spec2)<\/code> Checks if the two specifications have the same alphabet of actions. This is a necessary condition to computes the conjunction.<\/p>\nspec.composable(spec2) <\/code> Checks if the two specifications have disjoint alphabet of output actions. This is a necessary condition to computes the parallel composition.<\/p>\nspec.quotientable(spec2)<\/code> Checks if the specification spec1 can be quotiented by spec2.<\/p>\nConsistency checking<\/h6>\n
spec<\/code>.isConsistent()<\/code> returns True or False, if the specification is consistent. This implies to solve a consistency game.<\/p>\nspec<\/code>.isRobustConsistent(delta<\/em>)<\/code> where delta<\/em> is a float value. Returns True or False, if the specification is robustly consistent for the value delta<\/em>. This implies to solve a robust consistency game.<\/p>\nspec<\/code>.maxRobustConsistent(delta_max<\/em>,confidence<\/em>)<\/code> where delta_max<\/em> 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<\/em> is a float value that defines the precision of the computation. Returns the value\u00a0delta<\/em> such that the specification is robustly consistent. This function uses the CEGAR algorithm for parametric robustness.<\/p>\nspec<\/code>.maxRobustConsistentBS(delta_max,confidence<\/em>)<\/code> same as previously, but using a binary search algorithm instead.<\/p>\nspec<\/code>.getConsistencyGame()<\/code> returns the timed game used to check the consistency of the specification.<\/p>\nspec<\/code>.getRobustConsistencyGame(delta<\/em>,param<\/em>)<\/code> returns the robust consistency game used to check robust consistency. delta<\/em> is either an integer value, or a parameter name. By default delta<\/em> is a parameter named “delta”. param<\/em> is only useful if delta<\/em> is a parameter, in which case param<\/em> is the initial value of delta<\/em>. By default param<\/em>=0.<\/p>\nspec<\/code>.isUseful(bad_locations<\/em>)<\/code> 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.<\/em><\/p>\nspec<\/code>.isRobustUseful(delta<\/em>,bad_locations<\/em><\/code>)<\/code> where delta<\/em> is a float value. Returns True or False, if the specification is robustly useful for the value delta<\/em>. This implies to solve a robust usefulness game.<\/p>\nspec<\/code>.maxRobustUseful(delta_max<\/em>,confidence,bad_locations<\/em><\/code><\/em>)<\/code> where delta_max<\/em> 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<\/em> is a float value that defines the precision of the computation. Returns the value\u00a0delta<\/em> such that the specification is robustly useful. This function uses the CEGAR algorithm for parametric robustness.<\/p>\nspec<\/code>.maxRobustUseful<\/code>BS(delta_max<\/em>,confidence<\/em>)<\/code> same as previously, but using a binary search algorithm instead.<\/p>\nspec<\/code>.getUsefulnessGame()<\/code> returns the timed game used to check the usefulness of the specification.<\/p>\nspec<\/code>.getRobustUsefulnessGame(delta<\/em>,param<\/em>)<\/code> returns the robust consistency game used to check robust usefulness. delta<\/em> is either an integer value, or a parameter name. By default delta<\/em> is a parameter named “delta”. param<\/em> is only useful if delta<\/em> is a parameter, in which case param<\/em> is the initial value of delta<\/em>. By default param<\/em>=0.<\/p>\nRefinement and satisfaction checking<\/h6>\n
spec.refine(big_spec)<\/code> 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:<\/p>\nspec <= big_spec<\/code> or big_spec >= spec<\/code> are equivalent to the function call above.<\/p>\nspec.robSat(big_spec,delta<\/em><\/em>)<\/code> checks if spec is a robust implementation of big_spec for a perturbation of delta<\/em><\/p>\nspec.maxRobSat(big_spec,delta_max<\/em>,confidence<\/em>)<\/code> computes the maximum perturbation allowed by the implementation spec in order to robustly satisfies the specification big_spec. delta_max<\/em> is an integer value, sufficiently big to know that the implementation is not robust, and confidence<\/em> is a float value that defines the precision of the computation.<\/p>\nspec.implemPerturbation(delta<\/em>,param<\/em>)<\/code> Applies a perturbation to the guards of the implementation. delta<\/em> is either an integer value, or a parameter name. By default delta<\/em> is a parameter named “delta”. param<\/em> is only useful if delta<\/em> is a parameter, in which case param<\/em> is the initial value of delta<\/em>. By default param<\/em>=0.<\/p>\nT-AdaCTL checking<\/h6>\n