# 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.

## 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.