Clock guards and deadlocks

Question

I'm using UPPAAL for an academic project and I have some questions. I have to design a timed automata so my model has invariants on locations and clock guards on the edges. The problem is I must also verify my model. When I have cheked for deadlock states, before including guards, UPPAAL told me the property was satified. Now that I have add guards (with <=) it tells me the property is not satified so there are states that are not deadlock free. Using diagnostic trace I discovered the problem are the guards with the <= but I can't understand why. Can someone please help me figure it out? ps Sorry for my bad english

Answer 1

With x <= C guard where x is a clock and C is a constant, the system runs into situation where the time has progressed beyond and x is now above C, but the guard is disabling the edge, thus the system does not have any edge to execute -- deadlock. To see this, inspect the clock constraints when "deadlock" transition is selected in the symbolic simulator.

Here is an example:

This means that the process has no enabled edge and thus deadlock when x>5 (which makes the guard false and disable that edge).

The edge transition is still available when x<=5 and the simulator shows that constraint when that transition is selected: