Requirements

In this help section we give a BNF-grammar for the requirement specification language used in the verifier of UPPAAL.

Prop ::=
        'A[]' Expression
      | 'E<>' Expression
      | 'E[]' Expression
      | 'A<>' Expression
      | Expression --> Expression
| 'sup' ':' ExpressionList | 'sup' '{' Expression '}' ':' List | 'inf' ':' ExpressionList | 'inf' '{' Expression '}' ':' List
| Simulation | Probability | ProbUntil | Probability ( '<=' | '>=' ) PROB | Probability ( '<=' | '>=' ) Probability | Estimate
ExpressionList ::= Expression (',' Expression)* Simulation ::= 'simulate' SMCBounds '{' ExpressionList '}' ((':' CONST)? ':' Predicate)? Probability ::= 'Pr' SMCBounds '(' ('<>'|'[]') Expression ')' ProbUntil ::= 'Pr' SMCBounds '(' Expression 'U' Expression ')' Estimate ::= 'E' SMCBounds '(' ('min:' | 'max:') Expression ')' SMCBounds ::= '[' ( Clock | '#' ) '<=' CONST (';' CONST)? ']'

Predicate
is a Boolean expression.
CONST
is a non-negative integer constant.
PROB
is a floating point number from an interval [0;1] denoting probability.
'#'
means a number of simulation steps -- discrete transitions -- in the run.
'min:'
means the minimum value over a run of the proceeding expression.
'max:'
means the maximum value over a run of the proceeding expression.

All expressions are state predicates and must be side effect free. It is possible to test whether a certain process is in a given location using expressions on the form process.location. For sup properties, expression may not contain clock constraints and must evaluate to either an integer or a clock.

See also: Semantics of the Requirement Specification Language

Examples