UPPAAL SMC - How to provide a time distribution data as an input for invariant at a location and/or a guard in a transition?

[Raghav G]

I currently have information of time in the form of a distribution as shown in the image below.

I want to provide this time information(which is in the form of a distribution) as invariant in a location and/or a guard in a transition in UPPAAL SMC(Statistical Model Checking). However, I see that in an invariant you can only provide two possible data: 1) Time data by using clock variables in Invariant and 2) By using Rate of Exponential (Attached an image of possible options in invariant).

In both these cases, we cannot provide a time distribution data (as shown in the above image) since invariant doesn't provide any other means to provide this data as a condition. It is also not possible to provide this time distribution data in Guard condition in a transition as far as I am aware.

I understand that UPPAAL SMC provides results(Output) in the form of distribution when you right click on the query in the Verifier. However, I am not able to understand how I can provide the same as an input to Locations in UPPAAL. So, could someone please let me know if this is possible to do in UPPAAL SMC? If so, could you please let me know on how we can do this?

[Marius Mikučionis]

Hi,

Uppaal SMC Tutorial has a brief section 7.2 on how to use custom distributions:

https://doi.org/10.1007/s10009-014-0361-y

https://uppaal.org/texts/uppaal-smc-tutorial.pdf

If you describe your distribution as an array of bars, then you could use the following code to sample from them:

typedef struct {
    double offset;
    double width; // remove if distribution is discrete
    double height;
} bar_t;

const int BARS = 7;
typedef int[0,BARS-1] barid_t;

/// models continuous distribution
const bar_t bars[barid_t] = {
    {2000.0, 1.0,  15.0},
    {3000.0, 1.0, 155.0},
    {4000.0, 1.0, 305.0},
    {5000.0, 1.0, 220.0},
    {6000.0, 1.0,  40.0},
    {7000.0, 1.0,   5.0},
    {9000.0, 1.0,   2.0}
};

/// generates random values from bars
double generate() {
    double total = sum (i:barid_t) bars[i].width * bars[i].height;
    double pick = random(total);
    int i = 0;
    double weight = bars[i].width * bars[i].height;
    while (i < BARS and weight < pick) {
        pick = pick - weight;
        ++i;
        weight = bars[i].width * bars[i].height;
    }
    return bars[i].offset + pick / bars[i].height;
}

You can test it with the following query:

E[#<=0;10000](max:generate())

or construct an automaton like this:

and then use the following query:

Pr[<=10000;10000](<> P.Done)

Best regards,
Marius

[Raghav G]

Hi Marius,

Apologies for the delay in getting back to you since I had been ill for the past two weeks.
Thank you so much for your response. This is super helpful!

However, I noticed a couple of things which I would like to mention here and also, I am now getting an error which I am not able to resolve even after following all the steps in the manual, which requires your assistance.
1) In the above code, I am not able to use double offset since double is currently not allowed in typedef struct in UPPAAL currently it seems. I used int instead of double and it seems to be working fine.
2) Whenever I try to declare delay as a clock in the above model you have shared, I am getting an error -  Reached state with invalid invariant on line 1 of Project/Template/Delay/invariant. However, when I declare delay as double it seems to be working fine. In the manual, it has been recommended to use delay as a clock than a double, but I am not sure why I am getting this error only when I use it as a clock and not as a double.

3) I have a network of timed automata. There are synchronizations which have been converted into broadcast synchronizations for SMC. However, it looks like I cannot have locations which do not have delay specified in there. Every time I do not declare a location as urgent, committed or without a delay, I am getting this error -  Unspecified delay due to missing invariant and exponential rate on Project. This is also the case when I tried the model that you have shared above in your reply message, where it says there is no invariant in Start location. I have fixed this in my model by making the locations as committed for now. I also checked this document - https://people.cs.kuleuven.be/~danny.weyns/software/ActivFORMS/Current-restrictions-Uppaal.pdf where the final bullet point on Page 2 mentions that this is a current limitation in UPPAAL. Could you please confirm on this whether while performing SMC in UPPAAL, can we not have locations without delay(Invariants or Exponential rates)?  How do I model such locations where delay doesn't matter at all or where I do not want to specify any delay? 

Error that I am not able to resolve: Time Lock Error

1) I have been trying to run the probabilistic query you had shared above, in my model. However, I get a time lock error everytime when I try to run this query. I know for a fact that all my  invariants have values from time distribution data as per your direction and so I am not really sure if there is any time related error that I have made in my model. Please find the screenshot attached below showing this error. It would be really great if you could take a look into this and let me know what is happening here since it is not clear for me at all. Please do let me know if it would be helpful to take a look into my model and I can share it with you.

Thanks in advance for your assistance!

[Raghav G]

Hi,

Did anyone also face this time lock error in their model? If so, could you please let me know how you managed to resolve it? I have tried resolving this issue for the past few days but I couldn't find a solution for fixing this error. Any assistance on this would be much appreciated!

[Marius Mikučionis]

Hi ,

Sorry for late reply, we are in exam season...

On Thursday 13 June 2024 at 05:37:45 UTC+2 Raghav G wrote:

Hi Marius,

Apologies for the delay in getting back to you since I had been ill for the past two weeks.
Thank you so much for your response. This is super helpful!

However, I noticed a couple of things which I would like to mention here and also, I am now getting an error which I am not able to resolve even after following all the steps in the manual, which requires your assistance.
1) In the above code, I am not able to use double offset since double is currently not allowed in typedef struct in UPPAAL currently it seems. I used int instead of double and it seems to be working fine.

The double in struct support has been added recently in Uppaal 5.1.

 

2) Whenever I try to declare delay as a clock in the above model you have shared, I am getting an error -  Reached state with invalid invariant on line 1 of Project/Template/Delay/invariant. However, when I declare delay as double it seems to be working fine. In the manual, it has been recommended to use delay as a clock than a double, but I am not sure why I am getting this error only when I use it as a clock and not as a double.

Can you paste your automaton?

SMC tutorial uses delay clock for a bound, but it also stops the bound progress with `delay' == 0` -- this is equivalent to a plain double.

If you start modeling with double and then change the bound to a clock, then you need to add `delay'==0`.

 

3) I have a network of timed automata. There are synchronizations which have been converted into broadcast synchronizations for SMC. However, it looks like I cannot have locations which do not have delay specified in there. Every time I do not declare a location as urgent, committed or without a delay, I am getting this error -  Unspecified delay due to missing invariant and exponential rate on Project. This is also the case when I tried the model that you have shared above in your reply message, where it says there is no invariant in Start location.

That's right. The reason is that stochastic semantics requires not just delay bounds, but also a probability distribution to be able to determine a concrete successor state.

When an invariant limits the delay, then a uniform distribution is assumed, which does not require any more specifications.

But if there is no invariant, then the delay is unbounded, and in such cases an exponential distribution is used.

Exponential distribution requires a rate parameter, and that's what Uppaal is asking to specify.

The intuition behind the exponential rate is that the larger the rate, the more eager/faster the process is executing edges (smaller delays).

For example, an exponential distribution with a rate of 1:M  (or 1.0/M) has an average delay M.

The exponential distribution has a lot of nice properties, it is also the basis of Continuous Time Markov Chains, which makes it trivial to model those.

 

I have fixed this in my model by making the locations as committed for now.

That's a significant change of the behavior, not good. 

Basically committed/urgent location introduces an upper bound and switches to urgent behavior, except it is even more constrained: committed will prevent other non-committed processes, so you will not observe full behavior.

 

I also checked this document - https://people.cs.kuleuven.be/~danny.weyns/software/ActivFORMS/Current-restrictions-Uppaal.pdf where the final bullet point on Page 2 mentions that this is a current limitation in UPPAAL. Could you please confirm on this whether while performing SMC in UPPAAL, can we not have locations without delay(Invariants or Exponential rates)?  

I see this document is from 2018, many limitations have been fixed since then.

In particular, at that time we did not have concrete simulator, which actually deals with floating point numbers and can even make a plot (right click on a variable and choose Add plot).

The symbolic simulator still uses symbolic operations and does not support floating point states.

See UPPAAL 5 feature page for more:

https://uppaal.org/uppaal5/

 

How do I model such locations where delay doesn't matter at all or where I do not want to specify any delay? 

If you don't want any delay at all, then a better choice is an urgent location. If you want an uninterruptable/atomic behavior, then committed is the proper choice.

If the delay can be arbitrary large, then pick a small exponential rate, which will try to delay as much as possible.

For example, 1:1000 produces delays with 1000 time units on average.

 

Error that I am not able to resolve: Time Lock Error

1) I have been trying to run the probabilistic query you had shared above, in my model. However, I get a time lock error everytime when I try to run this query. I know for a fact that all my  invariants have values from time distribution data as per your direction and so I am not really sure if there is any time related error that I have made in my model. Please find the screenshot attached below showing this error. It would be really great if you could take a look into this and let me know what is happening here since it is not clear for me at all. Please do let me know if it would be helpful to take a look into my model and I can share it with you.

I need to examine that state, i.e. all the locations with their invariants and outgoing edges. Maybe edges are not enabled.

If you enable a diagnostic trace in Options menu, then you should get a trace and it should be easier to examine the situation.

It could also be a floating point precision issue, we tried to address this in the past, but it's not completely solved, especially when clocks differ in several magnitudes.

Best regards,
Marius

[Raghav G]

Hi Marius,

Thanks a ton for your response. I totally understand.

1) Yes, I will then eventually upgrade from 5.0 to 5.1.

2) I have included the automaton below(Will send it to you privately). Please do take a look into this and let me know what I am missing.

3) Thank you so much for the detailed explanation on the delay and the rationale behind using exponential delays, what to do in cases for arbitrary delays and no delays. It is much clearer now. I will keep this in mind while changing the delay in my model.

4) Thank you so much for agreeing to take a look into the model. I will send it to you privately.
I believe the edges are enabled in this situation, but I am not sure why it is still showing this error. I was wondering if this could be a deadlock because of time. However, once you take a look into this model, I think you will be able to provide better clarity on this.

Thanks again in advance for your assistance on this!

[Marius Mikučionis]

Hi,

It turns that the race of several components with different clocks still results in a floating point precision issues (the generated delay overshoots the invariant by a tiny margin).

So the solution is to replace the strict equality guard with non-strict and expand the invariant a bit, like so:

Where eps is defined as:

const double eps = 0.001;

The eps value needs to be adjusted based on precision requirements and the magnitude of the delay (precision bits are lost due to absolute value).

Best regards,
Marius