# Contents

# 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' ':' List | 'sup' '{' Expression '}' ':' List

| 'inf' ':' List | 'inf' '{' Expression '}' ':' List

| Probability | ProbUntil | Probability ( '<=' | '>=' ) PROB | Probability ( '<=' | '>=' ) Probability | Estimate

List ::= Expression | Expression ',' List

Probability ::= 'Pr[' ( Clock | '#' ) '<=' CONST ']' '(' ('<>'|'[]') Expression ')'

ProbUntil ::= 'Pr[' ( Clock | '#' ) '<=' CONST ']' '(' Expression 'U' Expression ')'

Estimate ::= 'E[' ( Clock | '#' ) '<=' CONST ';' CONST ']' '(' ('min:' | 'max:') 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

`A[] 1<2`

invariantly 1<2.`E<> p1.cs and p2.cs`

true if the system can reach a state where both process`p1`and p2 are in their locations`cs`.`A[] p1.cs imply not p2.cs`

invariantly process`p1`in location`cs`implies that process`p2`is**not**in location`cs`.`A[] not deadlock`

invariantly the process is not deadlocked.`sup: list`

the property is always true and returns the suprema of the expressions (maximal values in case of integers, upper bounds, strict or not, for clocks).`sup{expression}: list`

The expressions in the list are evaluated only on the states that satisfy the the expression (a state predicate) that acts like an observation.- The
`inf`formula are similar to`sup`but for infima. A state predicate should be used when a clock infimum is asked otherwise the trivial result is >= 0.