The property file specifies a biological property enconded with a CTRL temporal logic formula, and the corresponding Atomic Propositions (describing restrictions on a given state) that are referenced inside this formula. Property files have the extension.prop and can be edited using any text editor.
Terminals are written in bold, whereas non-terminals are written in italics. Furthermore,
| separates alternatives;
(...) delimitates a block composed of several alternatives;
[...] delimitates an optional block;
[...]* denotes a block repeated any (possibly 0) number of times;
[...]+ denotes a block repeated at least once.
The BNF syntax of a property is given below. The axiom is property.
Comments can be inserted into the files. The syntax of comments follows the rules for comments in languages like C: multi-line comments are placed between /* and */, while single-line comments are placed after characters //.
In addition to the above syntax, a number of constraints must be respected:
The property formula is not checked when loading the property and the corresponding atomic propositions. For the grammar, the formula is everything until the semi colon. The syntax should be verified when trying to check the validity of the property.
The identifier of each atomic-proposition must be the one used inside the property formula, and it will be the identifier appearing on the navigation tree.
For the subatomic propositions domain and focal-set, the identifier idf represents a variable name that must be declared in the model. For each variable, the lower and upper bounds should be defined. If absent the lower bound will be zero_var and the upper bound max_var.
For the subatomic proposition derivative, the identifier idf represents a variable name that must be declared in the model.
The property block must appear exactly once in a variable block.
The BNF syntax of a property formula is given below. The axiom is specification.
Some of these operators are boolean operators (nil, not, true, false, and, or, equ, implies), CTL and CTRL operators (EF, AF, EX, AX, EG, AG, A, E, U, R, EF@, AF@, EG-|, AG-|) and regular operators (., |, *,+). The CTRL grammar describing how these operators are articulated is shown below.