UPPAAL chooses to loop on instead of a transition of a higher priority

35 Views Asked by At

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 &gt; 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 &lt;= 600 &amp;&amp; (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 &lt;= 1600 &amp;&amp; TTC &gt; 600 &amp;&amp; distance &lt; recordedDist &amp;&amp; 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 &lt;= 2600 &amp;&amp; TTC &gt; 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) &amp;&amp; AEB.TTC &lt;= 600 --&gt; AEB.FullBraking
</formula>
         <comment>If the driver fails to apply brake or less brake and TTC &lt;= 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 --&gt; !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>

0

There are 0 best solutions below