This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 62

Summary: Time is allowed to pass when system is in urgent and / or committed locations
Product: UPPAAL Reporter: Juhan Ernits <juhan>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: CLOSED FIXED    
Severity: critical    
Priority: P2    
Version: 3.4.1   
Hardware: All   
OS: All   
URL: http://www.cc.ioc.ee/~juhan/bridge.zip
Architecture:
Attachments: relevant modified bridge examples

Description Juhan Ernits 2003-09-29 15:44:53 CEST
(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).
Comment 1 Juhan Ernits 2003-09-29 15:57:01 CEST
Created attachment 9 [details]
relevant modified bridge examples
Comment 2 Gerd Behrmann 2003-10-02 10:31:42 CEST
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.
Comment 3 Gerd Behrmann 2003-10-10 11:48:44 CEST
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.