<\/p>\n
Models are uploaded to PyECDAR via an XML files. This file can be edited with the graphical user interface of Uppaal<\/a> or Ecdar<\/a>. 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.<\/p>\n System declarations and queries from the Uppaal or Ecdar verifier are ignored by PyECDAR.<\/p>\n Identifiers<\/em> follow the same regular expression as in Uppaal: As in ECDAR, only broadcast channels are supported. They are declared by: Constants are either integers or Boolean values. They are declared in the following manner: expr<\/em> is an expression with constants, integer values or Boolean values, that can be evaluated to either an integer or a Boolean.<\/p>\n As in Ecdar, the model cannot have global clocks or global variables.<\/p>\n Template parameters are not supported.<\/p>\n Template constants can be used. As previously they are either integers or Boolean values. They are declared in the following manner: Clocks are declared in the following manner: 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:<\/p>\n Features variables are declared as Boolean variables at the end of the template’s declarations. They must be introduce by specific comments lines:<\/p>\n Locations can be urgent. Committed<\/em> locations are not supported.<\/p>\n Locations invariants are conjunctions of expressions separated by Transitions must all be synchronized.<\/p>\n The select<\/em> field <\/em> is not supported.<\/p>\n As for invariants, transitions guards are conjunctions of expressions separated by or Where Transitions update are list of updates separated by a comma. Each update is either:<\/p>\n where identifier<\/em> is a new feature variable and expr<\/em> is an Boolean expression with feature variables.<\/p>\n where identifier <\/em>is a variable and expr<\/em> is a variable expression with local variables, constants, integer or Boolean values.<\/p>\n <\/p>","protected":false},"excerpt":{"rendered":" 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 … <\/p>\n[a-zA-Z_]([a-zA-Z0-9_])*<\/code><\/p>\nProject declarations<\/h3>\n
\nbroadcast chan identifier<\/em>;<\/code> or
\nbroadcast chan list_identifier<\/em>;<\/code><\/p>\n
\nconst int identifier<\/em> = expr<\/em>;<\/code> or
\nconst bool\u00a0identifier<\/em> = expr<\/em>;<\/code><\/p>\nTemplates declarations<\/h3>\n
\nconst int identifier<\/em> = expr<\/em>;<\/code> or
\nconst bool\u00a0identifier<\/em> = expr<\/em>;<\/code><\/p>\n
\nclock identifier;<\/em><\/code> or
\nclock list_identifier<\/em><\/code>;<\/code><\/p>\n\n
int[min_expr<\/em>,max_expr<\/em>]\u00a0identifier<\/em> = init_expr<\/em>;<\/code> or
\nint[min_expr<\/em>,max_expr<\/em>]\u00a0identifier<\/em>;<\/code>
\nmin_expr,<\/em> max_expr <\/em>and init_expr<\/em> are expressions with constants, integer values or Boolean values, that can be evaluated to an integer value. min_expr<\/em> and max_expr<\/em> describe the range of the integer. If init_expr<\/em> is not defined the initial value is set to the value of min_expr<\/em>.<\/p>\n\n
bool identifier<\/em> = init_expr<\/em>;<\/code> or
\nbool identifier<\/em>;<\/code>
\nThen, init_expr<\/em> is an expression with constants, integer values or Boolean values, that can be evaluated to a Boolean value. If init_expr<\/em> is not defined the initial value is set to false<\/em>.<\/p>\n\/\/ system features<\/code><\/p>\n\n
bool identifier<\/em>;<\/code><\/p>\n\/\/ adaptive features<\/code><\/p>\n\n
bool identifier<\/em>,new_identifier<\/em>;<\/code><\/p>\n\/\/ environment features<\/code><\/p>\n\n
Templates locations<\/h3>\n
&&<\/code> or and<\/code>. Each expression is either:<\/p>\n\n
identifier<\/em> [<= | <] expr<\/em><\/code> or expr<\/em> [>= | >] identifier<\/em><\/code><\/p>\n\n
Templates transitions<\/h3>\n
&&<\/code> or and<\/code>. Each expression is either:<\/p>\n\n
identifier sign e<\/em>xpr<\/em><\/code> or expr sign<\/em> identifier<\/em><\/code><\/p>\nidentifier-identifier sign<\/em><\/code><\/em> expr<\/em><\/code> or expr sign\u00a0<\/em>identifier-identifier<\/em><\/code><\/p>\nsign<\/em> := [<= | < | == | > | >=]<\/code><\/p>\n\n
\n
\n
identifier = 0<\/em><\/code><\/p>\n\n
identifier = expr
\n<\/em><\/code><\/p>\n\n
identifier += expr<\/em><\/code> or identifier++<\/em><\/code> or<\/p>\nidentifier -= expr<\/em><\/code><\/em><\/code> or\u00a0identifier--<\/em><\/code><\/em><\/code><\/p>\n