How to simulate a random real-time variable in a model at execution time, and use Symbolic Simulator to manually execute transitions of another model, both at the same time?

[denizcaygoz]

Hi,

I'm using UPPAAL to modell and verify my real-time smart home heating system.
First I wanted to simulate the outside weather temperature as an integer variable. To simulate this variable I used weather_temp = fint(round(random_normal(weather_temp, 1.0))) . But because I implemented this, I cannot use the symbolic simulator. This was not a problem at the time because I didn't need to use symbolic simulator.
But now I came to the point where I implement a feature in my system which is Occupancy-Based Adaptive Heating. That is, the system adjusts the heating power based on whether someone is in the room or not. To implement this model I have implemented two models, MotionSensor and OccupancyController which they both use a chan variable to communicate to check if someone is in the room.
The problem is I cannot use symbolic simulator and because of that I cannot test these two models in Symbolic simulator which both are really suitable to use symbolic simulator.

My question is:
I want to randomly simulate a real-time variable like temperature at runtime and simultaneously manually execute various scenarios for the MotionSensor model in Symbolic Simulator. Is it possible to implement both simultaneously in UPPAAL at the same time?

[mikucionisaau]

Hi,

The root issue is that the symbolic engine (symbolic simulator and symbolic queries like E<> p, A[] p) need to explore all behavior exhaustively, but random_normal generates floating point numbers representing continuous range of values, and that is not possible to exhaust.

Instead of random_normal you can use select statement on an edge to generate non-deterministic edges with finite amount of distinct values.

For example, the following generates values from 6*Sigma range:

Declarations:

const int MEAN = 20;
const int SD = 5;
const double sqrt_2_pi = sqrt(2 * M_PI);
int value = INT16_MIN;
hybrid clock normal = INT16_MIN; /// continuous "cost", abstracted away in symbolic engine

/// Probability of observing v given Normal(mean,standard_deviation) distribution
double normal_prob(double x, double mean, double standard_deviation) {
    // https://en.wikipedia.org/wiki/Normal_distribution
    const double norm = (x - mean) / standard_deviation;
    return exp(-norm*norm/2.0) / sqrt_2_pi / standard_deviation;
}

The query E[<=1;1000000](max:value) yields the following distribution:

which is very close to Normal(20,5) generated by random_normal(20,5):

Here is a comparison composed using Tools > Plot Composer:

In this example the number of values is coupled with the standard deviation, but it can be easily customized.

Model: normal-distribution-discrete-generator.zip

[mikucionisaau]

@denizcaygoz I have added my model so you can inspect it how it works.

[denizcaygoz]

Hi @mikucionisaau,

thank you for your reply. It helped me a lot. I have still something in my mind:

As I understood, the statement in select generates a random value between 5 to 35 for example in this select statement: int[5, 35]. So the probability of each number that comes up are the same.

the another reason why I used weather_temp = random_normal(weather_temp, 1.0) is that every time this statement is executed I get really closed values respectively in concrete simulator. So let's say 25, 25, 24 and 26 and it goes on. I actually wanted to get something like this because this sequence of outputs represent realistic outside weather temperature, in which in each iteration weather temperature changes slightly.

In your suggestion, in which when I use int[5, 35] in select-part on the edge, I can get very random values respectively which does not simulate the weather temperature realistically in concrete simulator. Because I get the sequence of output something like: 20, 8, 30, 6. Which does not represent a proper weather temperature changes in a certain period of time.

So is there any other option in which I use select and at the same time I get outputs like I get in random_normal(weather_temp, 1.0). And also be able to use Symbolic Simulator?

[denizcaygoz]

I actually found a solution for this by using Select. I can do something like this:

diff:int[-2,2]
weather_temp = weather_temp + diff

with this approach I can get each time weather_temp which all are slightly different.
So with this approach I can use symbolic simulator and also simulate a weather temperature realistically. Thanks for the help.

[mikucionisaau]

As I understood, the statement in select generates a random value between 5 to 35 for example in this select statement: int[5, 35]. So the probability of each number that comes up are the same.

This is correct on simple edges, but in my example the edge comes from a branch-point which has an additional field: probabilistic weight (typeset in brown color), that's where I used normal_prob to compute a weight based on normal distribution.

The probabilistic branching lets you specify discrete probabilities over edges, while they are treated as non-deterministic edges in the symbolic engine.

The range diff:int[-2,2] has very few choices (only 5), so maybe the actual distribution is not that important?

If there are only a handful of options, then one can enumerate them with weights:

Which is equivalent to: