|Summary:||Crash when referring to reference parameters from property|
|Product:||UPPAAL||Reporter:||Gerd Behrmann <behrmann>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
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 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.