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 Subjection
| 'E<>' Expression Subjection
| 'E[]' Expression Subjection
| 'A<>' Expression Subjection
| Expression --> Expression Subjection
| 'sup' ':' List Subjection
| 'sup' '{' Expression '}' ':' List Subjection
| 'inf' ':' List Subjection
| 'inf' '{' Expression '}' ':' List Subjection
List ::= Expression | Expression ',' List
Subjection ::=
// empty for no subjection
| under StrategyName
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 ::=
ControlSpecifier Goal Subjection
| CollaborativeControlSpecifier Goal Subjection
| PartialControlSpecifier Goal Subjection
| TimeEfficientGameSpecifier Goal
ControlSpecifier ::=
'control:'
CollaborativeControlSpecifier ::=
'E<>' 'control:'
PartialControlSpecifier ::=
'{' List '}' 'control:'
TimeEfficientGameQuery ::=
'control_t*' '(' GameTimeLimitExpression ',' LocalGameTimeLimitExpression '):'
| 'control_t*' '(' u '):'
| 'control_t*:'
Goal ::=
'A<>' WinExpression
| 'A[' NotLooseExpression 'U' WinExpression ']'
| 'A[' NotLooseExpression 'W' WinExpression ']'
| 'A[]' NotLooseExpression
WinExpression ::= Expression
NotLooseExpression ::= Expression
GameTimeLimitExpression ::= Expression
LocalGameTimeLimitExpression ::= Expression
Subjection ::=
// empty for no subjection
| under StrategyName
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 Subjection
| Probability Subjection
| ProbUntil Subjection
| Probability ( '<=' | '>=' ) PROB Subjection
| Probability Subjection '>=' Probability Subjection
| Estimate Subjection
Simulate ::= 'simulate' '[' SMCBounds ']' '{' List '}' [ ':' [ SATRUNS ':' ] Expression ]
Probability ::=
'Pr' MITLExpression
| 'Pr[' SMCBounds ']' '(' PathType Expression ')'
ProbUntil ::= 'Pr[' SMCBounds ']' '(' Expression 'U' Expression ')'
Estimate ::= 'E[' SMCBounds ']' '(' ('min:' | 'max:') Expression ')'
SMCBounds ::= BoundType [ ; RUNS ]
BoundType ::= ( | Clock | '#' ) '<=' BOUND
PathType ::= ( '<>' | '[]' )
Subjection ::=
// empty for no subjection
| under StrategyName
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 Subjection
| ExpQuantifier '[' BoundType ']' Features ':' PathType Expression Subjection
| ExpPrQuantifier '[' BoundType ']' Features ':' PathType Expression Subjection
ExpQuantifier ::= ( minE | maxE )
ExpPrQuantifier ::= ( minPr | maxPr )
Features ::= '{' List '}' '->' '{' List '}'
Subjection ::=
// empty for no subjection
| under StrategyName
Strategy queries allow store, load, reuse and refine the strategies by assigning names to them.
AssignQuery ::=
'strategy' StrategyName '=' AssignableQuery
AssignableQuery ::=
TIGAQuery
| LearningQuery
| 'loadStrategy' Features '(' Path ')'
NonAssignableQuery ::=
SymbQuery
| SMCQuery
| 'saveStrategy' '(' Path ',' StrategyName ')'