About select statement and queries in UPPAAL SMC

[Mingzhuo Zhang]

Hi,

    We had some confusion during modeling in UPPAAL.

    1. Is the select statement uniform in selecting values in the bounded range? For example, if we use a select statement i:int[1,99], we wonder the probability of choosing 1 is definitely 1/100?

        If so, what is the difference between select statement and the probability branch (using branch point) ?

    2. When our model has probabilistic characteristics, which means it is a SMC version model, can we still use standard queries like A[], E<>, etc. ?

Thank you!

[Marius Mikučionis]

On Sunday, May 17, 2020 at 4:03:22 AM UTC+2, Mingzhuo Zhang wrote:

Hi,

    We had some confusion during modeling in UPPAAL.

    1. Is the select statement uniform in selecting values in the bounded range?

Select statement is a succinct way of creating many independent edges and for independent edges Uppaal assigns a uniform distribution, provided that the guards are the same.

So yes, the choice is uniform.

 

 For example, if we use a select statement i:int[1,99], we wonder the probability of choosing 1 is definitely 1/100?

int[1,99] has 99 values, so each edge is going to be assigned a probablity of 1/99 (provided that the guards are the same).

 

        If so, what is the difference between select statement and the probability branch (using branch point) ?

The edges with branchpoints have probabilistic weights so one can customize the distribution based on weights.

You can also combine them with the select statement and provide weights in an array (there is demo/smc/lmac6.xml example which uses this feature).

See also Uppaal SMC Tutorial.

 

    2. When our model has probabilistic characteristics, which means it is a SMC version model, can we still use standard queries like A[], E<>, etc. ?

Yes, but with two caveats:

1) the probabilities are abstracted away. For example, the branched probabilistic edges become non-deterministic edges, also the exponential rates are ignored etc..

Thus symbolic analysis considers a broader abstraction of the concrete (stochastic) behavior. 

For example, locations without invariants but with an exponential rate 1 in SMC will generate delays of up to 22 time units (longer delays have virtually zero probability), but the symbolic queries will check potentially infinite delays which is much much longer than just 22 time units.

2) the foating point variables and operations are not supported and are silently disabled. 

For example, random(), fint() and other floating point functions will always return zero.

These features still make sense in Stratego where symbolic abstraction is used and then the stochastic behavior is reintroduced (hence no warning is issued).

We are working on adding some options that will allow the user to be notified when floating point operations are safely ignored and issue errors/warnings when used incorrectly.

Best regards,

Marius