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>

I checked this and 4.0.6 indeed gives false negative,
while the version on trunk says that property is satisfied.

Revision 3932 fixes it.