Re: the problem of stop in UPPAAL.

[Marius Mikučionis]

Hi,

On Monday, December 30, 2019 at 7:29:40 AM UTC+1, 李帅 wrote:

Dear sir or madam:

I have a question about UPPAAL, the details are as follows:

I have set two execution interval of activities with label states with invariant "t<=2","t<=4" and arcs with guard "t>=5", "t>=8" after the states in Independent time automatons, where 2, 4 and 5, 8 are the upper and lower bounds of execution intervals, respectively, i.e., the execution intervals are [2, 4] and [5, 8] of activities. However, when I begin to simulate in simulator of UPPAAL, it will stop at certain state, but when I delete the execution interval [5, 8], it can continue to execute and no stop. So I want to know why it stops, is it version of UPPAAL has potential bugs, or the setting of this is bad.

What you mean by "when I delete the execution interval"?

The way you describe it, it seems that the invariant and guard conditions are incompatible: the lower bounds on guards are greater than the upper bounds in the invariants.

Which means that the outgoing transitions are not enabled yet, but the invariant has already expired -- a deadlock and thus the simulator stops.

I would expect the simulator to show a deadlock transition with constraints t ∈ (2;5) and another deadlock with t ∈ (4;8).

It would be easier to comment if you include a screenshot.

Best regards,

Marius