# Syntax of Statistical Queries

## Statistical Queries

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 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
``````
BOUND
is a non-negative integer constant denoting an upper bound over the absolute global time (when a variable is not specified), specific Clock (cost) variable or a number of action-transitions (#).
RUNS
is an optional positive integer constant denoting the maximum number of runs. If the number of runs is not specified, then it is decided based on Statistical parameters and the particular estimation algorithm.
SATRUNS
is an optional positive integer constant denoting the maximum number of runs that satisfy the state expression.
PROB
is a floating point number from interval [0; 1] denoting a probability bound.
’#’
means a number of simulation steps – discrete edge-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.

### Examples

`simulate [<=10] { x }`
creates one stochastic simulation run of up to `10` time units in length and plot the values of `x` expression over time (after checking, right-click the query and choose a plot).
`simulate [c<=10] { x, y+z }`
creates one simulation run of up to `10` cost units in terms of clock variable `c` and plot the values of `x` and `y+z` expressions over the cost `c`.
`simulate [#<=10] { x, y+z }`
creates one simulation run of up to `10` edge-transitions and plot the values of `x` and `y+z` expressions over the discrete simulation steps (edge-transitions).
`simulate [<=10; 100] { x, y+z } : 2 : goal`
selects up to `2` simulation runs from `100` simulations of up to `10` time units in length, which satisfy `goal` state predicate, and then plot the values of expressions `x` and `y+z` over time. The query will also estimate a probability confidense interval of the expression `goal` being true just like in `Pr` query. The confidence level is controlled by α-level of significance in the Statistical parameters.
`Pr[<=10](<> good)`
runs a number of stochastic simulations and estimates the probability of `good` eventually becoming true within `10` time units. The number of runs is decided based on the probability interval precision (±ε) and confidence level (level of significance α in Statistical parameters), see Confidence Intervals for details. The query also computes a probability distribution over time when the predicate `good` is satisfied (right-click the property and choose a plot).
`Pr[c<=10; 100]([] safe)`
runs `100` stochastic simulations and estimates the probability of `safe` remaining true within `10` cost units in terms of clock `c`.
`Pr[<=10](<> good) >= 0.5`
checks if the probability of reaching `good` within `10` time units is greater than `50%`. Such query uses Wald’s algorithm to decide the probability inequality and requires fewer runs than probability estimation and explicit comparison. Uses -δ, +δ, α and β Statistical parameters.
`Pr[<=10](<> best) >= Pr[<=10](<> good)`
checks if the probability of reaching `best` is greater than reaching `good` within `10` time units. Such query uses a sequential algorithm to decide the probability inequality and requires fewer runs than probability estimation and explicit comparison. Uses -δ, +δ, u0, u1, α and β Statistical parameters. The query also provides a probability comparison plot over time/cost (right-click the query and choose plot).
`E[<=10; 100](max: cost)`
estimates the maximal value of `cost` expression over `10` time units of stochastic simulation. Uses `100` stochastic simulations and assumes that the value follows Student’s t-distribution with 1-α confidence level.

The plots can be super-imposed using the Plot Composer from the Tools menu.