This section describes a BNF-grammar for the requirement specification language used in the verifier of UPPAAL.
Symbolic queries are performed using symbolic operations based on symbolic semantics of timed automata and correspond to a mathematically rigorous proof.
SymbQuery ::=
'A[]' Expression
| 'E<>' Expression
| 'E[]' Expression
| 'A<>' Expression
| Expression --> Expression
| 'sup' ':' List
| 'sup' '{' Expression '}' ':' List
| 'inf' ':' List
| 'inf' '{' Expression '}' ':' List
List ::= Expression | Expression ',' List
For sup properties, expression may not contain clock constraints and must evaluate to either an integer or a clock.
See also: Semantics of the Symbolic Queries
Controller synthesis queries are decided using symbolic techniques over Timed Game (TIGA) automata, where the discrete actions are either controllable (controller’s actions, solid edges) or uncontrollable (environment actions, dashed edges). The result is either a strategy solving the game objective or that the strategy does not exist.
TIGAQuery ::=
'control:' 'A<>' WinExpression
| 'control:' 'A[' NotLooseExpression 'U' WinExpression ']'
| 'control:' 'A[' NotLooseExpression 'W' WinExpression ']'
| 'control:' 'A[' NotLooseExpression ']'
WinExpression ::= Expression
NotLooseExpression ::= Expression
Statistical queries are decided using concrete semantics of stochastic hybrid automata over a number of bounded concrete simulation runs and correspond to empirical measurements of the system performance. The results are of statistical estimate nature and may vary across different executions based on uncertainties specified in the statistical parameters.
SMCQuery ::=
| Simulate
| Probability
| ProbUntil
| Probability ( '<=' | '>=' ) PROB
| Probability ( '<=' | '>=' ) Probability
| Estimate
Simulate ::= 'simulate' '[' SMCBounds ']' '{' List '}' [ : Expression [ ':' SATRUNS ]]
Probability ::= 'Pr[' SMCBounds ']' '(' PathType Expression ')'
ProbUntil ::= 'Pr[' SMCBounds ']' '(' Expression 'U' Expression ')'
Estimate ::= 'E[' SMCBounds ']' '(' ('min:' | 'max:') Expression ')'
SMCBounds ::= BoundType [ ; RUNS ]
BoundType ::= ( | Clock | '#' ) '<=' BOUND
PathType ::= ( '<>' | '[]' )
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.
See also: Semantics of the SMC Queries
LearningQuery ::=
ExpQuantifier '(' Expression ')' '[' BoundType ']' Features ':' PathType Expression
ExpQuantifier ::= ( min | max )
Features ::= '{' List '}' '->' '{' List '}'
Strategy queries allow store, load, reuse and refine the strategies by assigning names to them.
StrategyQuery ::=
'strategy' Name '=' Query [ 'under' Name ]
| 'saveStrategy' '(' Path ',' Name ')'
| 'loadStrategy' Features '(' Path ')'
Query ::=
SymbQuery
| TIGAQuery
| SMCQuery
| LearningQuery