When I try to verify the property
     A<> (Generator.RSP and (Generator.latencyPush == 3))
on the model below, I am told that the property is not satisfied.
The diagnostics trace generated by all three techniques (some,
shortest, and fastest) is incorrect, since it is possible
to reach a state satisfying the property by simply continuing the
execution for 6 steps (each state has a single successor).


------------------------------------------------------------------

<?xml version='1.0' encoding='utf-8'?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>const int push_dl=3;
const int gen_dl=10;

//the time elapsing
clock time;

urgent chan PUSH_RQ, PUSH_RSP, PUSH_DL_START, GEN_DL_START;
chan PUSH_DL_STOP, GEN_DL_STOP;
</declaration><template><name>Queue</name><declaration>const int sMax=2;

//definition of the type status
const int idle=0;
const int pending=1;
const int started=2;
const int spent=3;
typedef int[0,3] status_value;
typedef struct{
	status_value value;
}status;

//instanciation and initialization of the status pushStatus
status pushStatus;

void init_status(){
	pushStatus.value=idle;
}
</declaration><location id="id0" x="-864" y="360"></location><location id="id1" x="-864" y="272"><urgent/></location><init ref="id1"/><transition><source ref="id0"/><target ref="id0"/><label kind="guard" x="-1216" y="288">pushStatus.value==spent</label><label kind="synchronisation" x="-1112" y="304">PUSH_RSP!</label><label kind="assignment" x="-1224" y="320">pushStatus.value=idle</label><nail x="-1024" y="336"/><nail x="-1024" y="296"/></transition><transition><source ref="id0"/><target ref="id0"/><label kind="guard" x="-1208" y="392">pushStatus.value==started</label><label kind="synchronisation" x="-1136" y="408">PUSH_DL_STOP?</label><label kind="assignment" x="-1192" y="424">pushStatus.value=spent</label><nail x="-1016" y="440"/><nail x="-1016" y="400"/></transition><transition><source ref="id0"/><target ref="id0"/><label kind="guard" x="-1216" y="488">pushStatus.value==pending</label><label kind="synchronisation" x="-1144" y="520">PUSH_DL_START!</label><label kind="assignment" x="-1208" y="536">pushStatus.value=started</label><nail x="-1016" y="552"/><nail x="-1016" y="496"/></transition><transition><source ref="id0"/><target ref="id0"/><label kind="guard" x="-1064" y="592">pushStatus.value==idle</label><label kind="synchronisation" x="-976" y="608">PUSH_RQ?</label><label kind="assignment" x="-1056" y="624">pushStatus.value=pending</label><nail x="-904" y="592"/><nail x="-944" y="592"/></transition><transition><source ref="id1"/><target ref="id0"/><label kind="assignment" x="-952" y="288">init_status()</label></transition></template><template><name>Generator</name><declaration>clock latencyPush;</declaration><location id="id2" x="-88" y="112"></location><location id="id3" x="-176" y="112"><name x="-216" y="104">RSP</name></location><location id="id4" x="-176" y="24"><name x="-216" y="8">RQ</name></location><location id="id5" x="-88" y="24"><name x="-98" y="-6">BRQ</name></location><init ref="id3"/><transition><source ref="id2"/><target ref="id5"/><label kind="synchronisation" x="-144" y="80">GEN_DL_STOP?</label></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-184" y="128">GEN_DL_START!</label></transition><transition><source ref="id4"/><target ref="id3"/><label kind="synchronisation" x="-216" y="40">PUSH_RSP?</label></transition><transition><source ref="id5"/><target ref="id4"/><label kind="synchronisation" x="-168" y="-40">PUSH_RQ!</label><label kind="assignment" x="-168" y="-24">latencyPush=0</label></transition></template><template><name>Delay</name><parameter>int delay, urgent chan &amp;START, chan &amp;STOP</parameter><declaration>clock clk;</declaration><location id="id6" x="-104" y="104"><label kind="invariant" x="-200" y="96">clk&lt;=delay</label></location><location id="id7" x="-64" y="104"></location><init ref="id7"/><transition><source ref="id6"/><target ref="id7"/><label kind="guard" x="-136" y="128">clk&gt;=delay</label><label kind="synchronisation" x="-120" y="144">STOP!</label><nail x="-80" y="128"/></transition><transition><source ref="id7"/><target ref="id6"/><label kind="synchronisation" x="-128" y="48">START?</label><label kind="assignment" x="-128" y="64">clk=0</label><nail x="-80" y="80"/></transition></template><system>Push_delay=Delay(push_dl,PUSH_DL_START,PUSH_DL_STOP);
Gen_delay =Delay(gen_dl ,GEN_DL_START ,GEN_DL_STOP );

system Queue, Generator, Push_delay, Gen_delay;
</system></nta>