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.