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

Bug 139

Summary: Crash when referring to reference parameters from property
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: RESOLVED FIXED    
Severity: major CC: furang
Priority: P2    
Version: 3.5.4   
Hardware: All   
OS: All   
Architecture:
Attachments: Uppaal model
UPPAAL Query file

Description Gerd Behrmann 2005-03-21 21:28:33 CET 
Submitted by Angelo Furfaro:

As you can see in the attached model (clockref.xml + clockref.q), I used a clock
reference as  parameter for the template named P, i.e. P(clock& x). In the
process assignment section I specified 

 p=P(c);

where c is a global clock. P has only one location with the invariant x<=10 and
one loop transtion which reset the clock x. The query

 A[] c<=10 is satisfied

but 

 A[] p.x<=0 is not satisfied.
Comment 1 Gerd Behrmann 2005-03-21 21:31:01 CET 
Created attachment 26 [details]
Uppaal model
Comment 2 Gerd Behrmann 2005-03-21 21:31:36 CET 
Created attachment 27 [details]
UPPAAL Query file
Comment 3 Gerd Behrmann 2005-03-21 21:32:19 CET 
Confirmed.

In fact, the GUI crahes when trying to verify the second property, whereas
verifyta provides the wrong result.
Comment 4 Gerd Behrmann 2005-07-12 15:50:00 CEST 
This is not limitted to clocks. Any kind of reference parameters used in a property is not handled correctly.
Comment 5 Gerd Behrmann 2005-08-21 15:50:05 CEST 
A fix has been checked into CVS.