Bug 62

(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).