Time Lock Error in UPPAAL Model (Learning query)

[Szpilman2]

Dear UPPAAL team, hi
recently I have been working on your tool for verifying my model. but I encountered to time lock error in uppaal. i attached my model in here and uppaal verifier says that Time-lock error: State: ( m.L0 n.second ) #t(0)=0#time=3 x=3 energy=9 how can I fix this error?

also my query is : strategy Opt = minE(energy) [<=30] : <> m.L3

I also used this technique but it still gives me timeLock Error.

in other terms i have a formula which is time dependent (in this case energy changes over time). and each state consumes fixed amount of energy. and i want to model it. but in combination with time constraints (time invariant) or channel synchronization it has error. do you know how can i fix this problem? or how can I model this in proper ways?

best regards.

[mikucionisaau]

Enable the diagnostic trace to inspect the situation in the simulator:
Options -> Diagnostic trace -> Some

Time-lock error: State: ( m.L0 n.second ) #t(0)=0#time=3 x=3 energy=9 means that the system cannot leave the state m.L0 n.second when x reaches 3, because m.L0 has an invariant x<=3 and the output transition is guarded with input synchronization use?, i.e. the process cannot make progress independently (cannot leave L0) and the invariant blocks the time -- time-lock (special case of a deadlock).

Similarly the timelock happens in the k.l0 because the process k cannot leave L0 when clock x gets to 5 because the outgoing transition is guarded with input synchronization use?.

You need to either remove the input synchronization use? or add an extra edge to be executed when use? does not arrive before the invariant lapses.

[Szpilman2]

Thank you for your reply. Your explanation was excellent and easy to understand. I implemented the solution you suggested in this link and added a controllable edge to be executed when the invariant is violated. However, this led to another time lock error. Subsequently, I changed the controllable edge to uncontrollable, and it resolved the issue. Am I on the right track?

model with time lock error:

model without time lock error:

best regards

[mikucionisaau]

This one is probably specific to strategy synthesis.
The issue is that in order for the controller to make a controllable transition from sofLoc1 to sofLoc2 it needs to delay. The trouble is that strategy learning cannot pick a specific delay and if it needs to pick a delay, then it treats it as infinite delay (or until an opponent makes an edge-transition) and thus the controllable transition is never available as a decision. Then there is an invariant which causes the timelock. It stems from one of the strategy assumptions that controller may choose from either taking a controllable edge-transition immediately, or take a delay (without edge-transition).

The solution is to split the location sofLoc1 into two locations: one where the automaton can delay and then make uncontrollable edge-transition to a new urgent location, then model the decisions from that new urgent location: one to move to sofLoc2 location, and another decision (potentially) to go back to the original location to delay some more.

We are working on the documentation of all these assumptions.