Models are uploaded to PyECDAR via an XML files. This file can be edited with the graphical user interface of Uppaal or Ecdar. The models used by PyECDAR must be valid in Uppaal or Ecdar (these tools provide syntactic checks). PyECDAR supports the main syntactic elements proposed by these tools. We explain below which restrictions to apply.
System declarations and queries from the Uppaal or Ecdar verifier are ignored by PyECDAR.
Identifiers follow the same regular expression as in Uppaal: [a-zA-Z_]([a-zA-Z0-9_])*
Project declarations
As in ECDAR, only broadcast channels are supported. They are declared by:
broadcast chan identifier; or
broadcast chan list_identifier;
Constants are either integers or Boolean values. They are declared in the following manner:
const int identifier = expr; or
const bool identifier = expr;
expr is an expression with constants, integer values or Boolean values, that can be evaluated to either an integer or a Boolean.
As in Ecdar, the model cannot have global clocks or global variables.
Templates declarations
Template parameters are not supported.
Template constants can be used. As previously they are either integers or Boolean values. They are declared in the following manner:
const int identifier = expr; or
const bool identifier = expr;
Clocks are declared in the following manner:
clock identifier; or
clock list_identifier;
Local variables may be used. The only types allowed are fixed range integers and Boolean. They may or may not be initialized. If not a default value is assume:
- Fixed range integers are declared by:
int[min_expr,max_expr] identifier = init_expr; or
int[min_expr,max_expr] identifier;
min_expr, max_expr and init_expr are expressions with constants, integer values or Boolean values, that can be evaluated to an integer value. min_expr and max_expr describe the range of the integer. If init_expr is not defined the initial value is set to the value of min_expr.
- Boolean variable are declared by:
bool identifier = init_expr; or
bool identifier;
Then, init_expr is an expression with constants, integer values or Boolean values, that can be evaluated to a Boolean value. If init_expr is not defined the initial value is set to false.
Features variables are declared as Boolean variables at the end of the template’s declarations. They must be introduce by specific comments lines:
// system features
- Starts the declaration of non-adaptive system features. Each feature is declared in the following manner:
bool identifier;
// adaptive features
- Starts the declaration of adaptive system features. Each feature must be declared with two identifiers: the first is the feature variable, the second is the new value of the feature after firing a transition:
bool identifier,new_identifier;
// environment features
- Starts the declaration of environment features. All these features are adaptive, which means that they are declared, as previously, with two identifiers.
Templates locations
Locations can be urgent. Committed locations are not supported.
Locations invariants are conjunctions of expressions separated by && or and. Each expression is either:
- A clock guard with only upper bound constraint. The coefficient expr is an expression with constants and integers that can be evaluated to an integer value:
identifier [<= | <] expr or expr [>= | >] identifier
- A feature expression with only feature variables and Boolean operators.
- A variable expression with local variables, constants, integer or Boolean values.
Templates transitions
Transitions must all be synchronized.
The select field is not supported.
As for invariants, transitions guards are conjunctions of expressions separated by && or and. Each expression is either:
- A clock guard, that can be a lower bound, an upper bound or a clock difference. The coefficient expr is an expression with constants and integers that can be evaluated to an integer value:
identifier sign expr or expr sign identifier
or identifier- or identifier sign exprexpr sign identifier-identifier
Where sign := [<= | < | == | > | >=]
- A feature expression with only feature variables and Boolean operators.
- A variable expression with local variables, constants, integer or Boolean values.
Transitions update are list of updates separated by a comma. Each update is either:
- A clock reset:
identifier = 0
- A feature update:
identifier = expr
where identifier is a new feature variable and expr is an Boolean expression with feature variables.
- A variable increment or decrement:
identifier += expr or identifier++ or
identifier -= expridentifier--
where identifier is a variable and expr is a variable expression with local variables, constants, integer or Boolean values.
