Deadlock and no deadlock in the same state

[Leandro Ribeiro]

Hi,

I am a bit confused with a deadlock scenario UPPAAL is reporting.

I have 3 enabled edges:

The system is clearly in different states when it takes the first or second transition.

(TaskTimingV2(2).c and .t are different)

However, I see no difference at all between the state in the second and third (deadlock) cases:

Isn't it contradictory to have a deadlock and a possible transition in the same state?

Am I missing something?

Can that be a mistake on my model, or most likely a bug?

Thanks in advance!

LBR

[Marius Mikučionis]

There is indeed a bug in the simulator displaying false deadlocks, but the common symptom of such false deadlocks are the constraints beyound the state space (i.e. beyond invariant, thus easy to dismiss), the solution is to use verifier.

But in this case it looks like the deadlock is within invariant and indeed contradicting the previous transition.

Based on your uprevious questions, could it be a result of priorities?

maybe some higher priority process is preventing the lower priority process leaving a committed location?

Best regards,
Marius

[Leandro Ribeiro]

At this point,  none of the process is in a committed state.

I do use channel priorities in this model.

_kernelEntry has higher priority than all other channels.

The transition with _kernelEntry is enabled on TaskTimingV2(2).c = 20.

In the first transition, _kernelEntry is taken because of its higher priority.

getResource is only taken in case TaskTimingV2(2).c < 20 (second transition).

No idea why the third transition exists, hehe.

If I remove the priorities, the behavior is modified.

I will try to obtain the same behavior without priorities.

If it works, then the problem is in the use of priorities.

Thanks for the hint, Marius!

[Leandro Ribeiro]

Thread Update.

I have attached a simple model where the behavior occurs.

This behavior happens only when channel/process priorities are used in conjunction with urgent channels/locations.

In my example, the deadlock entries appear when the possible transitions are:

C1- a higher priority channel (_kernelEntry!) ; and

C2.1- a lower priority urgent channel (getResource!) ; or

C2.2- a lower priority channel from an urgent location (I tested this variant as well, when getResource is not urgent).

In short: IF ( C1 and (C2.1 or C2.2) ) deadlock appears.

 

Question:

It seems to really be a bug.

What's the most appropriate way to report it to UPPAAL development team?

__________________________________

Furthermore, I tried the same example with UPPAAL Stratego, which shows one extra deadlock entry.

We can see the #time is the only difference among the enabled transitions.

But #time is like a meta variable, correct? (it is not part of the state)

So it is the very same situation as my previous tests with UPPAAL 4.1.

[Mohammed Foughali]

@leandro "This behavior happens only when channel/process priorities are used in conjunction with urgent channels/locations." 

In my case it happens also with non urgent channels/locations as soon as you have an invariant on the location from which the lower-priority channel is triggered, and the intervals in which the lower-priority transition and the higher priority one are enabled intersect.

Hope it will help fixing the bug. I can provide my model if necessary.

[Mohammed Foughali]

Hi Leandro, Marius, 

I'm having exactly the same problem with a model I developed recently. I have spent a couple of days digging, and I am quite sure these deadlocks are false. And I can confirm this problem only appears when you have priorities over channels. 

However, it seems to me that it is not a simulator-only issue. The verifier also detects these false deadlocks and treats them as actual ones. In my model, when I try to verify a leadsto property (which should hold) the verifier replies with a negative answer and a counterexample that ends with a false deadlock...

On Friday, April 2, 2021 at 9:50:32 AM UTC+2 leandro...@gmail.com wrote: