Symbolic queries are performed using symbolic operations based on symbolic semantics of timed automata and correspond to a mathematically rigorous proof.
SymbolicQuery ::=
'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 rail road diagram for the entire SymbolicQuery syntax.
See also: Semantics of the Symbolic Queries
A[] 1<2
1<2
.E<> p1.cs and p2.cs
p1
and p2
are in their locations cs
.A[] p1.cs imply not p2.cs
p1
in location cs
implies that process p2
is not in location cs
.A[] not deadlock
sup: Train(1).x, Train(2).x
sup{Train(1).Crossing}: Train(1).x
inf{Gate.Occ}: Gate.len
sup
, inf
query computes infimum of the given expression Gate.len while process Gate is in Occ location. When a clock infimum is needed, the state predicate should be used, otherwise the result is trivially >=0
.