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
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
A p.x<=0 is not satisfied.
Created attachment 26 [details]
Created attachment 27 [details]
UPPAAL Query file
In fact, the GUI crahes when trying to verify the second property, whereas
verifyta provides the wrong result.
This is not limitted to clocks. Any kind of reference parameters used in a property is not handled correctly.
A fix has been checked into CVS.