8 March 2010

Part 3. Appendices

Table of Contents

3.1. Syntax of GNA model
3.1.1. Syntactic conventions
3.1.2. BNF of a model
3.1.3. Additional constraints
3.2. Syntax of GNA initial conditions
3.2.1. Syntactic conventions
3.2.2. BNF of an initial conditions file
3.2.3. Additional constraints
3.3. Syntax of CTRL property
3.3.1. Syntactic conventions
3.3.2. BNF of a property
3.3.3. Additional constraints
3.3.4. BNF of a property formula
3.4. CUP Parser Generator license
3.5. JGraph license
3.6. SAT4J license
3.7. NuSMV license

3.1. Syntax of GNA model

Model files have the extension .gna and can be edited using any text editor.

3.1.1. Syntactic conventions

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.

3.1.2. BNF of a model

The BNF syntax of the GNA models is given below. The axiom is model.

Comments can be inserted into GNA models. 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 //.

3.1.3. Additional constraints

In addition to the above syntax, a number of constraints must be respected:

  • Some keywords are reserved and cannot be used as identifiers: true and false. In addition to this, it is recommended not to use the following identifiers if you intend to use GNA's model checking tools: equ, implies, or, and, not, ef, af, eg, ag, ex, ax, nil, e, a, u and r.

  • If the variable is an input variable, only the threshold-parameters, box-parameter, zero-parameter, and threshold-inequalities blocks can appear in a variable block.

  • The synthesis-parameters block must appear exactly once in a variable block. Each synthesis parameter used in the right-hand side of the state equation in some variable block must be declared in the synthesis-parameters block. In previous versions of GNA, the terminal production-parameters: was used instead of synthesis-parameters:. This alternative terminal is still accepted by the current version.

  • The degradation-parameters block must appear exactly once in a variable block.

  • The threshold-parameters block must appear at most once in a variable block. (It can be omitted if the state or input variable has no associated threshold parameters.) The threshold parameters in the thresholds-parameters block of a variable x are the thresholds at which x regulates other variables. That is, the threshold parameters may appear in step functions in other variable blocks.

  • The zero-parameter and box-parameter blocks must appear exactly once in a variable block.

  • The state-equation block must appear exactly once in a variable block. The idf in the left-hand side of the state equation must be the variable being described.

  • The synthesis-parameters, degradation-parameters, threshold-parameters, zero-parameter and maximum-parameter blocks must have been defined before the state equation and parameter-inequalities blocks.

  • In the synthesis term of the state equation, each idf corresponds to a synthesis parameter of the variable being described.

  • In the degradation term of the state equation, the rightmost idf in each alternative corresponds to the variable being described, while the others correspond to degradation parameters of that variable.

  • In step-function expressions, the first idf is the regulator variable and the second idf a threshold parameter of this variable.

  • The parameter-inequalities block must appear exactly once in a variable block. In order to make simulation possible, these inequalities must induce a total order on the threshold, focal, zero, and maximum parameters of the variable. The focal parameters occurring in the parameter inequality are determined from the state equation by taking all possible quotients of synthesis and degradation parameters, except 0. For instance, consider the following state equation: d/dt x_a = k_a1 + k_a2 * s+(x_b,t_b) - g_a * x_a.The possible focal parameters are in this case k_a1/ g_a and (k_a1+ k_a2)/ g_a.The user has to assure that the set of inequality constraints specified is consistent. Notice that the terminals threshold-inequalities: and equilibrium-inequalities: (nullcline-inequalities:) are no longer used in GNA 6.0.

  • The first inequality term in a parameter equality must be the zero parameter, while the last inequality term must be the maximum parameter.

Examples of model files can be consulted in the samples directory of the GNA distribution.