(Sorry for the lengthy intro) The problem can be extracted from the bridge example that comes with the Uppaal distribution. In the original example it is possible (and perfectly legal from the point of view of the model) that when the 5 minute viking and 10 minute viking cross the bridge then the 5 minute viking can release the torch after 5 minutes have elapsed although his partner has not yet made it over the bridge. This does not have any falsifing effect on the properties to be verified. The system shows this behaviour in the trace when "breadth first" search is enabled. I tried to modify the model to make passing the torch procedures more realistic. And this is where I came across behaviour I did not expect regarding urgent and committed locations. I modified the Torch process (pls check the URL) and added names "onBridgeEscaping" and "onBridgeReturning" to appropriate locations of the Soldier template. The semantics of the committed location according to my understanding is something atomic, so no time can pass while staying in this location and no interleaving is allowed. The semantics of the urgent location should be that no time can pass when staying in the location but interleavings are allowed. It should be also equivalent to introducing a new clock that is reset to zero on all incoming edges and adding an invariant of <=0 for the clock to the location. In the model bridge_case1.xml the two properties E<> (Viking1.safe and Viking2.onBridgeEscaping and time <=5 and Torch.one) and A[] not deadlock should not be valid at the same time, because as Torch.one is urgent (or even committed) then if this location is arrived at in 5 time units, then there should be no way out from there without letting time pass. Currently it seems to be ok for Uppaal 3.4.1 (and previous versions) when Torch.one is either urgent or committed. (Viking1 is the 5 minute guy and Viking2 is the 10 minute one.) The behaviour is different for the case when an additional clock is introduced for modelling urgency in location Torch.one. This is shown in model bridge_case2.xml. In that case the system can deadlock, but time still seems to progress in location Torch.one (NB! please have breadth first search on when checking for e.g. E<> Viking1.safe and Viking2.safe and Viking3.safe and Viking4.safe and then following the trace. The new clock Torch.t stays equal to 0 while the difference time-Torch.t changes from [5,inf] to [10,inf]) (this is when passing through the location Torch.one).
Created attachment 9 [details] relevant modified bridge examples
I can confirm the problem with the urgent location. It turns out to be a problem in the deadlock checker (which btw also affects the liveness checker). I have checked in a fix to CVS. I cannot see what the problem with model bridge_case2.xml is. It is correct that in the symbolic state where Torch is in location one, the difference time-Torch.t is in [5,inf], but this does not mean that time can progress. It simply means that before entering the state time >= 5. Since Torch.t == 0, we have that time-Torch.t >= 5.
I talked to Juhan about the second problem, and it seems to a documentation issue, see bug 64. The other problem has been fixed. Juhan confirmed that the fix solved the problem.