Created attachment 322 [details]
A model with two templates: S and M

Observed: 
If we perform the following query "Refinement: M<=S" on the attached model with verifytga, we get "property not satisfied" and the following strategy:

Strategy for the attacker:

State: ( S.L1 M.L1 ) [spoiler]
While you are in        (S.x<=5 && S.x==M.x), wait.
When you are in (5<S.x && S.x==M.x), take transition S.L1->S.L2 { x >= 3, c?, 1 }

State: ( S.L2 M.L1 ) [spoiler]
While you are in        (S.x==M.x), wait.

State: ( S.L0 M.L0 ) [spoiler]
When you are in true, take transition M.L0->M.L1 { 1, b!, x := 0 } [SKIP]

The strategy for state S.L1 M.L1 suggest to take transition S.L1->S.L2 when 5<S.x, however there is an invariant x<=5 on S.L2 which is violated if we perform this transition. 

Expected: 
The engine should respond with the following strategy instead:

Strategy for the attacker:

State: ( S.L0 M.L0 ) [spoiler]
When you are in true, take transition M.L0->M.L1 { 1, b!, x := 0 } [SKIP]

State: ( S.L2 M.L1 ) [spoiler]
While you are in        (S.x==M.x), wait.

Steps:
1. Open commandopromt
2. Type following command: <verifytga> -t0 <model.xml> <queryfile> to recieve the faulty strategy

Build:
I tried with the following verifytga version:
(Academic) UPPAAL-TIGA 4.1.12-0.16 (rev. 5145), April 2013
Copyright (c) 1995 - 2013, Uppsala University and Aalborg University.
All rights reserved.
Compiled with i686-w64-mingw32-g++ -Wall -DLIBXML_STATIC -DNDEBUG -O2 -ffloat-store -msse2 -m32 -march=core2 -DENABLE_TIGA -DMULTI_TERMINAL -DENABLE_STORE_MINGRAPH -DTIGA_MERGE_STATES -DTIGA_GREEDY_MERGE -DTIGA_OTF_BUCHI    -DBOOST_DISABLE_THREADS -mwindows
Free for academic and non-commercial use only.

Frequency: 10/10