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.