We have design a new version of PyECDAR for the analysis of adaptive featured real-time systems. This version is currently separated from the main version of pyecdar. It includes a new parser for UPPAAL models with features that replaces PyUPPAAL. Features are added as boolean arrays. 3 types of arrays may be used and declare in a template has follow:
- bool Fa[n], Fb[n];
It declares an array Fa of n adaptive system features, and the corresponding array Fb to update these features.
These features can be changed by output transitions. - bool Fe[n], Ff[n];
It declares an array Fe of n adaptive environment features, and the corresponding array Ff to update these features. These features can be changed by input transitions. - bool Fs[n];
It declares an array Fs of n non adaptive system features. These features cannot be changed at runtime initialisation.
Features variable Fa[i], Fe[i] or Fs[i] can used in guards and invariants. The updates Fb[i] or Ff[i] can be used in guards only. These features expressions may only be used at then end of a guard (or an invariant) inside parentheses. For instance the following guard:
(Fs[1] and ((Fa[0] and Fb[0]) or (not Fa[0] and not Fb[0])))
specifies that the transition is enable if the system feature Fs[1] is enable and that the adaptive feature Fa[0] is not altered by the transition. The last part can be shorten by using an assignment:
(Fb[0]=Fa[0])
You can have a look at the demo included in the package to see how to use this new version of PyECDAR.
In the future we will merge this version with the main version of PyECDAR.
