about time-locked states in uppaal SMC

[harvest...@gmail.com]

Hi,

I am a fresh user of uppaal. I wanted to try the SMC-based verification using the uppaal 4.1.24 version.

So, I took the SchedulingFramework.xml example provided in the "demo" directory of uppaal. I first transformed all channels into broadcast channels (this is a requirement) and I tried the following verification formulas:

1) Pr[<=20] (<> Task(0).Error or Task(1).Error or Task(2).Error or Task(3).Error or Task(4).Error)

The output shows a "time-locked" state that I cannot understand given the indicated task state values and the clock values in that state. I will be happy to have any opinion on this reproducible situation. Note that for X <= 19, the property:

Pr[<=X] (<> Task(0).Error or Task(1).Error or Task(2).Error or Task(3).Error or Task(4).Error)

surprisingly seems to work fine.

Now, to make it easy, I tried the next simplified formula:

2) Pr[<=20] (<> Task(2).Error)

The output gave:

"Server exception: Location Task(2).Ready has unbounded delay but no positive rate"

I may be wrong but the state "Ready" in the Task automaton already has an associated clock invariant with a bound. Nevertheless, I added another clock invariant on "time[id]" with a deadline value as the bound. But, it still does not work.


Could you please explain to me what I am doing wrong regarding these issues? It seems that such a topic is not covered enough in the uppaal documentation. Thank you so much.

Best regards

[Marius Mikučionis]

On Wednesday, May 13, 2020 at 5:58:47 PM UTC+2, harvestonjames wrote:

Hi,

I am a fresh user of uppaal. I wanted to try the SMC-based verification using the uppaal 4.1.24 version.

So, I took the SchedulingFramework.xml example provided in the "demo" directory of uppaal. I first transformed all channels into broadcast channels (this is a requirement)

Interesting exercise, but you have to be careful when changing to broadcast, it is not merely syntactic change: broadcast synchronizations are non-blocking, thus senders may progress without receivers and there is risk for "lost updates" if the receivers are not always listening.

 

and I tried the following verification formulas:

1) Pr[<=20] (<> Task(0).Error or Task(1).Error or Task(2).Error or Task(3).Error or Task(4).Error)

The output shows a "time-locked" state that I cannot understand given the indicated task state values and the clock values in that state. I will be happy to have any opinion on this reproducible situation.

I think the issue is that the "time-lock" happens in one of the committed locations of the Resource which expects a synchronization "inserted?" and thus cannot progress independently.

In this particular model the resource is tightly synchronized with a Policy, thus this location does not have to be committed.

 

Note that for X <= 19, the property:

Pr[<=X] (<> Task(0).Error or Task(1).Error or Task(2).Error or Task(3).Error or Task(4).Error)

surprisingly seems to work fine.

Now, to make it easy, I tried the next simplified formula:

2) Pr[<=20] (<> Task(2).Error)

The output gave:

"Server exception: Location Task(2).Ready has unbounded delay but no positive rate"

I may be wrong but the state "Ready" in the Task automaton already has an associated clock invariant with a bound. Nevertheless, I added another clock invariant on "time[id]" with a deadline value as the bound. But, it still does not work.

The Ready invariant uses a stopwatch, ie. the progress of that clock can be stopped and thus the invariant is preserved with any delay, therefore any delay is possible and concrete simulator needs a probability distribution.

By default the simulator uses uniform distribution when there is an upper limit, but Ready does not have an upper limit, thus Uppaal is trying to fallback to exponential rate and is asking for an exponential rate.

Thus please supply an exponential rate.

The rate is inversely proportional to an average delay.

E.g. rate 2 means average delay 0.5 time units and rate 1:2 means average delay of 2 time units.

 

Could you please explain to me what I am doing wrong regarding these issues? It seems that such a topic is not covered enough in the uppaal documentation. Thank you so much.

There is Uppaal SMC tutorial in case you have not seen:

https://www.it.uu.se/research/group/darts/papers/texts/uppaal-smc-tutorial.pdf

 

Best regards