Generate a Random number in Uppaal

Question

My question is Can I generate a random number in Uppaal?

I would like to generate a number from a range of values. Even more, I would like to generate not just integers I would like to generate double values as well.

for example: double [7.25,18.3]

I found this question that were talking about the same. I tried it. However, I got this error: syntax error unexpected T_SELECT.

It doesn't work. I'm pretty new in Uppaal world, I would appreciate any help that you can provide me.

Regards,

Answer 1

This is a common and misunderstood question in Uppaal.

Simple answer:

    double val; // declaration
    val = random(18.3-7.25)+7.25; // use in update, works in SMC (Uppaal v4.1)

Verbose answer:

1. Uppaal supports symbolic analysis as well as statistical and the treatment and possibilities are radically different. So one has to decide first what kind of analysis is needed. Usually one starts with simple symbolic analysis and then augment with stochastic features, sometimes stochastic behavior needs also to be checked symbolically.

2. In symbolic analysis (queries A[], A<>, E<>, E[] etc), random is synonymous with non-deterministic, i.e. if the model contains some "random" behavior, then verification should check all of them any way. Therefore such behavior is modelled as non-deterministic choices between edges. It is easy to setup a set of edges over an integer range by using select statement on the edge where a temporary variable is declared and its value can be used in guards, synchronization and update. Symbolic analysis supports only integer data types (no floating point types like double) and continuous ranges over clocks (specified by constraints in guards and invariants).

3. Statistical analysis (via Monte-Carlo simulations, queries like Pr[...](<> p), E[...](max: var), simulate, etc) supports double types and floating point functions like sin, cos, sqrt, random(MAX) (uniform distribution over [0, MAX)), random_normal(mean, dev) etc. in addition to int data types. Clock variables can also be treated as floating point type, except that their derivative is set to 1 by default (can be changed in the invariants which allow ODEs -- ordinary differential equations).

4. It is possible to create models with floating point operations (including random) and still apply symbolic analysis provided that the floating point variables do not influence/constrain the model behavior, and act merely as a cost function over the state space. Here are systematic rules to achieve this:

   a) the clocks used in ODEs must be declared of hybrid clock type.

   b) hybrid clock and double type variables cannot appear in guard and invariant constraints. Only ODEs are allowed over the hybrid clocks in the invariant.