Random numbers in UPPAAL

[Sailesh Sai Teja]

Hello,

Is there a way to assign a random value to a global variable in UPPAAL. I see an old stackoverflow (https://stackoverflow.com/questions/19522823/random-number-in-uppaal) to make use of the select but it's not exactly suiting my use case.

My use case is as-follows (path_value is global variable initial assigned to -1) :-

1) Generate a random number (between 0 and n(2 in my case) inclusive)

2) I now enter a loop where based on the random number generated previously, the new path to be taken and the value that needs to be assigned to 'new_value' is determined.

I tried the solution discussed in the above referenced stackoverflow link but it doesn't suit the requirement.

Thank you.

[Marius Mikučionis]

It depends on what you are trying to do:

1) if you are using symbolic simulator and/or symbolic queries like A[], E<> etc, then the `select` statement as cited in stackoverflow post is the only valid solution (the next options won't work). The reason is that such "randomness" is actually non-determinism in disguise, and hence must be models as such.

I know it is inconvenient with many values, but such behavior quickly results in a state space explosion and hence discouraged. With many values it is better to try harder and find a better abstraction.

2) if you are using concrete simulator and/or SMC query, then you can use variables of `double` type and functions like `random()` and `fint()`, see https://docs.uppaal.org/language-reference/expressions/#floating-point-type-support.

3) if you want to combine controller synthesis (timed games) with SMC or learning (optimization), then the only way is through `hybrid clock` variables, which can be used to store information about cost. Such cost variables cannot be read (used in guards etc) and they are abstracted away (i.e. ignored) in symbolic queries, thus does not seem to fit your scenario.

Best regards,
Marius