Location time-locked when A[] not deadlock

[deliarico]

Hello, I have a model that verifies "A[] not deadlock" but shows a "time-locked" error when trying to validate UPPAAL-SMC. I am not sure why this happens. I have some feeling that it is related to the fact that a location is trying to exit due to the SMC and it is blocking. But the thing is that it shouldn't happen because if the location waits for the other automata, it can progress without deadlock and complying with the invariant.

The model is pretty easy, it is a Origin that sends a signal to a MiddleMan and a MiddleMan that waits X time until sending the signal to the Destination. The Destination resets the clock each X time marked by a limit if the MiddleMan does not have anything to send. I am not sure how to properly share the code here, so I am going to share a link with the code.

The error obtained is the following: when trying to validate UPPAAL-SMC with a dummy query like Pr[<=100] (<> end==1)
I get:

Location m.Empty [ clocktime=1 #time=1.2740762476356566335056186289876 ] empty=1 LIMIT=4 end=0 d.rc=0 is time-locked.

As I understand it, it shouldn't be an error because the invariant that the middleman has is "clocktime<=LIMIT" and it is true if clocktime=1, time=1.27 and limit=4. It should wait until the origin sends the signal or until the origin decides to end (we see that end=0, so the origin has not ended).

I have not been able to find much documentation on time-locked locations and I cannot get a counter-example trace so I would appreciate if someone could guide me in what is happening or why or how can it be avoided.

[RasmusRendal]

That does seem to be a bug. Trying the query with the latest version of UPPAAL, Stratego 9, which is available from our website, I could not reproduce it.

What version of UPPAAL are you using?

[mikucionisaau]

I can replicate the issue in Uppaal-4.1.26, where it says that the timelock is in MiddleMan.Empty:

The issue is that such automaton violates independent progress assumption when clocktime gets over the LIMIT and thus the process cannot escape the Empty location.
Independent progress is an important assumption in SMC because the processes are racing each other and thus need to be able to progress independendently. In symbolic analysis that process is simply lucky due to the fact that input always arrives earlier than the invariant expires.

A simple fix is to add an extra transition signifying what should happen if the input does not arrive before the LIMIT:

Destination.Receiving also has a similar problem.

Stratego is more forgiving in that respect (it'll wait until the invariant actually expires), but the issue is still with such processes.