I am new to UPPAAL and i am trying to model an AEB system. I want the transition into the URGENT node FullBraking To happen immediately, without any single delay for the query to happen, however it does not happen and i do not know how make it choose the URGENT node first, any suggestions ? I attached the project to make it clearer.
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.6//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_6.dtd'>
<nta>
<declaration> // Place global declarations here.
int speed := -1 ;
int distance := -1;
int[0,2] reaction;
//The broadcasts
urgent broadcast chan car;
urgent broadcast chan noCar;
chan warning;
chan noWarning;
chan goodReaction;
chan badReaction;
chan partial;
urgent broadcast chan stop;
chan done;</declaration>
<template>
<name x="5" y="5">Dashboard</name>
<declaration>// Place local declarations here.
</declaration>
<location id="id0" x="0" y="-17">
<name x="-42" y="-51">NoWarning</name>
</location>
<location id="id1" x="0" y="93">
<name x="-26" y="110">Warning</name>
</location>
<init ref="id0"/>
<transition id="id2">
<source ref="id1"/>
<target ref="id0"/>
<label kind="synchronisation" x="-102" y="25">noCar?</label>
<nail x="-42" y="34"/>
</transition>
<transition id="id3">
<source ref="id0"/>
<target ref="id1"/>
<label kind="synchronisation" x="42" y="17">warning?</label>
<nail x="42" y="34"/>
</transition>
</template>
<template>
<name>Braking</name>
<location id="id4" x="0" y="0">
<name x="-42" y="-34">NoActivation</name>
<urgent/>
</location>
<location id="id5" x="110" y="127">
<name x="93" y="144">Full</name>
</location>
<location id="id6" x="-110" y="127">
<name x="-135" y="144">Partial</name>
</location>
<location id="id7" x="-170" y="-102">
<name x="-180" y="-136">start</name>
</location>
<init ref="id7"/>
<transition id="id8">
<source ref="id7"/>
<target ref="id4"/>
<label kind="synchronisation" x="-152" y="-68">car?</label>
</transition>
<transition id="id9">
<source ref="id6"/>
<target ref="id4"/>
<label kind="synchronisation" x="-92" y="110">noCar?</label>
<nail x="-25" y="127"/>
</transition>
<transition id="id10">
<source ref="id5"/>
<target ref="id4"/>
<label kind="synchronisation" x="43" y="110">noCar?</label>
<nail x="25" y="127"/>
</transition>
<transition id="id11">
<source ref="id4"/>
<target ref="id5"/>
<label kind="synchronisation" x="18" y="-17">stop?</label>
<nail x="110" y="0"/>
</transition>
<transition id="id12">
<source ref="id4"/>
<target ref="id6"/>
<label kind="synchronisation" x="-92" y="-17">partial?</label>
<nail x="-110" y="0"/>
</transition>
</template>
<template>
<name>Radar</name>
<location id="id13" x="0" y="-170">
<name x="-34" y="-204">Scanning</name>
</location>
<location id="id14" x="0" y="-34">
<name x="-34" y="-17">FoundObject</name>
</location>
<init ref="id13"/>
<transition id="id15">
<source ref="id14"/>
<target ref="id14"/>
<label kind="guard" x="34" y="-42">distance > 0</label>
<label kind="assignment" x="-51" y="17">distance = distance - 10</label>
<nail x="127" y="8"/>
<nail x="-85" y="8"/>
</transition>
<transition id="id16">
<source ref="id14"/>
<target ref="id13"/>
<label kind="guard" x="-136" y="-102">distance == 0</label>
<label kind="synchronisation" x="-85" y="-119">noCar!</label>
<nail x="-34" y="-102"/>
</transition>
<transition id="id17">
<source ref="id13"/>
<target ref="id14"/>
<label kind="synchronisation" x="42" y="-119">car!</label>
<label kind="assignment" x="34" y="-136">speed = 39, distance = 150</label>
<label kind="comments" x="51" y="-187">The distance is in meters so 150 m
The speed is in M/S so approx 140 KM/H</label>
<nail x="34" y="-102"/>
</transition>
</template>
<template>
<name>AEB</name>
<declaration>int recordedDist;
int TTC := 10000;
</declaration>
<location id="id18" x="-17" y="-144">
<name x="-51" y="-195">Normal</name>
</location>
<location id="id19" x="272" y="-42">
<name x="289" y="-51">FullBraking</name>
<urgent/>
</location>
<location id="id20" x="-17" y="68">
<name x="-76" y="85">PartialBraking</name>
</location>
<location id="id21" x="-450" y="-110">
<name x="-595" y="-119">PrimaryWarning</name>
</location>
<location id="id22" x="280" y="195">
<name x="272" y="212">halt</name>
<urgent/>
</location>
<location id="id23" x="-272" y="-221">
<name x="-282" y="-255">start</name>
</location>
<init ref="id23"/>
<transition id="id24">
<source ref="id20"/>
<target ref="id18"/>
<label kind="guard" x="-195" y="-34">reaction == 2</label>
<label kind="synchronisation" x="-127" y="-17">noCar!</label>
<nail x="-102" y="-42"/>
</transition>
<transition id="id25">
<source ref="id21"/>
<target ref="id18"/>
<label kind="guard" x="-331" y="-204">reaction == 2</label>
<label kind="synchronisation" x="-399" y="-178">noCar!</label>
<nail x="-272" y="-178"/>
</transition>
<transition id="id26">
<source ref="id22"/>
<target ref="id18"/>
<label kind="synchronisation" x="212" y="93">noCar!</label>
</transition>
<transition id="id27">
<source ref="id23"/>
<target ref="id18"/>
</transition>
<transition id="id28">
<source ref="id19"/>
<target ref="id22"/>
</transition>
<transition id="id29">
<source ref="id18"/>
<target ref="id18"/>
<label kind="assignment" x="-102" y="-272">TTC = (distance/speed)*1000</label>
<nail x="-93" y="-212"/>
<nail x="42" y="-212"/>
</transition>
<transition id="id30">
<source ref="id21"/>
<target ref="id18"/>
<label kind="guard" x="-297" y="-161">reaction != 2</label>
<nail x="-246" y="-144"/>
</transition>
<transition id="id31">
<source ref="id20"/>
<target ref="id18"/>
<label kind="guard" x="-25" y="-25">reaction != 2</label>
<nail x="0" y="-42"/>
</transition>
<transition id="id32">
<source ref="id18"/>
<target ref="id19"/>
<label kind="guard" x="178" y="-119">TTC <= 600 && (reaction == 0 || reaction == 1)</label>
<label kind="synchronisation" x="1" y="-148">stop!</label>
<nail x="136" y="-119"/>
<nail x="153" y="-170"/>
</transition>
<transition id="id33">
<source ref="id18"/>
<target ref="id20"/>
<label kind="guard" x="-340" y="34">TTC <= 1600 && TTC > 600 && distance < recordedDist && reaction == 0</label>
<label kind="synchronisation" x="-68" y="-59">partial!</label>
<nail x="-42" y="-42"/>
</transition>
<transition id="id34">
<source ref="id18"/>
<target ref="id21"/>
<label kind="guard" x="-374" y="-93">TTC <= 2600 && TTC > 1600</label>
<label kind="synchronisation" x="-331" y="-110">warning!</label>
<label kind="assignment" x="-382" y="-76">recordedDist := distance</label>
<nail x="-238" y="-119"/>
</transition>
</template>
<template>
<name>Dynamics</name>
<location id="id35" x="0" y="-34">
<name x="-10" y="-68">Normal</name>
</location>
<location id="id36" x="144" y="127">
<name x="93" y="144">actionEnough</name>
</location>
<location id="id37" x="0" y="127">
<name x="-51" y="144">actionNotEnough</name>
</location>
<location id="id38" x="-119" y="127">
<name x="-153" y="144">noAction</name>
</location>
<branchpoint id="id39" x="-59" y="365"/>
<branchpoint id="id40" x="0" y="34"/>
<init ref="id35"/>
<transition id="id41">
<source ref="id39"/>
<target ref="id36"/>
<label kind="assignment" x="68" y="357">reaction = 2</label>
<label kind="probability" x="153" y="348">0.33</label>
<nail x="161" y="348"/>
</transition>
<transition id="id42">
<source ref="id39"/>
<target ref="id37"/>
<label kind="assignment" x="-8" y="255">reaction = 1</label>
<label kind="probability" x="0" y="238">0.33</label>
<nail x="0" y="238"/>
</transition>
<transition id="id43">
<source ref="id39"/>
<target ref="id38"/>
<label kind="assignment" x="-127" y="212">reaction = 0</label>
<label kind="probability" x="-93" y="229">0.33</label>
<nail x="-68" y="246"/>
</transition>
<transition id="id44" controllable="false">
<source ref="id38"/>
<target ref="id39"/>
<label kind="synchronisation" x="-109" y="297">partial?</label>
<nail x="-127" y="263"/>
</transition>
<transition id="id45" controllable="false">
<source ref="id37"/>
<target ref="id39"/>
<label kind="synchronisation" x="-68" y="187">partial?</label>
<nail x="-42" y="229"/>
</transition>
<transition id="id46" controllable="false">
<source ref="id35"/>
<target ref="id40"/>
<label kind="synchronisation" x="-76" y="-17">warning?</label>
</transition>
<transition id="id47">
<source ref="id40"/>
<target ref="id36"/>
<label kind="assignment" x="17" y="42">reaction = 2</label>
<label kind="probability" x="76" y="76">0.33</label>
</transition>
<transition id="id48">
<source ref="id40"/>
<target ref="id37"/>
<label kind="assignment" x="-42" y="76">reaction = 1</label>
<label kind="probability" x="8" y="93">0.33</label>
</transition>
<transition id="id49">
<source ref="id40"/>
<target ref="id38"/>
<label kind="assignment" x="-136" y="51">reaction = 0</label>
<label kind="probability" x="-101" y="97">0.33</label>
</transition>
</template>
<system>
system Dashboard, Braking, Radar, AEB, Dynamics;
</system>
<queries>
<option key="--diagnostic" value="0"/>
<query>
<formula/>
<comment/>
</query>
<query>
<formula>A[] not deadlock
</formula>
<comment>The system is deadlock free</comment>
<result outcome="success" type="quality" timestamp="2023-12-18 17:14:12 +0100">
<option key="--diagnostic" value="0"/>
</result>
</query>
<query>
<formula>(reaction != 2 || reaction == 0 ||reaction == 1) && AEB.TTC <= 600 --> AEB.FullBraking
</formula>
<comment>If the driver fails to apply brake or less brake and TTC <= 600 ms then full braking will be activated.</comment>
<result outcome="failure" type="quality" timestamp="2023-12-18 17:10:25 +0100">
<option key="--diagnostic" value="0"/>
</result>
</query>
<query>
<formula>reaction == 2 --> !Braking.Full</formula>
<comment>If the driver steers or accelerates then automatic braking will not be activated.</comment>
<result outcome="success" type="quality" timestamp="2023-12-18 17:14:11 +0100">
<option key="--diagnostic" value="0"/>
</result>
</query>
</queries>
</nta>