Bug 472

Created attachment 216 [details]
wrong file

Comment on attachment 216 [details]
wrong file

><?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>// Place global declarations here.
>
>urgent chan go;
>
>// Controller of one feed belt (DB_Entry automaton) notifies other that new bag was put on the distribution belt, and that stop time has to be recalculated
>broadcast chan bagReschedule;
>
>
>// Sensor value constants
>typedef int[0,3] sensor_value;
>const sensor_value Sens_None = 0,
>	Sens_Black = 1,
>	Sens_Yellow = 2,
>	Sens_Unknown = 3;
>
>// TODO: Consider using some starvation free controller to put some bounds on stops variable
>typedef int stopPeriod;
>
>
>// Motor state variables
>bool	FeedMov[2] = { true, true };	// feedbelt1 is moving, feedbelt2 is moving
>
>// Sensor state variables
>sensor_value Sensor[2];
>
>
>// Distribution belt reservation time
>int DB_Reservation;
>// The clock since the last bag entered DB:
>clock DB_BagClk;
>
>// Stop Delta: smallest allowed stop period
>const int SD = 1;
></declaration><template><name x="5" y="5">Bag </name><declaration>// Place local declarations here.
>
>clock clk;
></declaration><location id="id0" x="-1008" y="-2160"><name x="-1040" y="-2192">B</name></location><location id="id1" x="-1008" y="-2432"><name x="-1120" y="-2464">readyToEnter</name><label kind="invariant" x="-1112" y="-2448">clk &lt;= 10</label></location><location id="id2" x="-1056" y="-2552"><name x="-1080" y="-2584">decide
></name></location><location id="id3" x="-1008" y="-2288"><name x="-1040" y="-2328">A</name><label kind="invariant" x="-1096" y="-2312">clk &lt;= 16</label></location><init ref="id2"/><transition><source ref="id3"/><target ref="id0"/><label kind="guard" x="-992" y="-2256">clk &gt;= 16</label><label kind="assignment" x="-992" y="-2224">Sensor[0] := Sens_None</label></transition><transition><source ref="id2"/><target ref="id1"/><label kind="synchronisation" x="-1016" y="-2552">go?</label><label kind="assignment" x="-1008" y="-2536">clk := 0</label><nail x="-1008" y="-2496"/></transition><transition><source ref="id1"/><target ref="id3"/><label kind="assignment" x="-1000" y="-2384">clk := 0,
>Sensor[0] := Sens_Unknown</label></transition></template><template><name>DB_Entry </name><declaration>stopPeriod stopsNeeded;
>clock y;</declaration><location id="id4" x="-192" y="-144"><name x="-256" y="-160">Moving</name><label kind="invariant" x="-264" y="-136">y &lt;= 40</label></location><location id="id5" x="320" y="32"><name x="320" y="-8">calculateStopTime</name><label kind="comments">Calculate amount of stops still needed before the last bag reaches its destination:
>y + stopsNeeded &gt;= DB_Reservation - DB_BagClk.
>
>// DB_Reservation-DB_BagClk: time still needed to wait
>// y : time now</label><committed/></location><location id="id6" x="48" y="-320"><name x="24" y="-360">ReleaseBag</name><committed/></location><location id="id7" x="-192" y="32"><name x="-224" y="56">decide
></name><committed/></location><location id="id8" x="248" y="-320"><name x="224" y="-360">wait</name><label kind="invariant" x="264" y="-352">y &lt;= stopsNeeded*SD</label></location><location id="id9" x="-192" y="-320"><name x="-208" y="-360">none
></name></location><init ref="id9"/><transition><source ref="id4"/><target ref="id7"/><label kind="guard" x="-256" y="-80">y &gt;= 40</label></transition><transition><source ref="id8"/><target ref="id5"/><label kind="synchronisation" x="312" y="-192">bagReschedule?</label><label kind="comments">When new bag is realeased onto the Distribution Belt we might need to wait longer.</label></transition><transition><source ref="id5"/><target ref="id8"/><label kind="guard" x="352" y="40">stopsNeeded - DB_Reservation &lt;= DB_BagClk-y</label><nail x="544" y="32"/><nail x="544" y="-320"/></transition><transition><source ref="id5"/><target ref="id5"/><label kind="guard" x="80" y="112">stopsNeeded - DB_Reservation &gt; DB_BagClk-y</label><label kind="assignment" x="216" y="136">stopsNeeded++</label><label kind="comments">Calculate amount of stops still needed before the last bag reaches its destination:
>y + stopsNeeded &gt;= DB_Reservation - DB_BagClk.
>
>// DB_Reservation-DB_BagClk: time still needed to wait
>// y : time now</label><nail x="248" y="112"/><nail x="320" y="112"/></transition><transition><source ref="id7"/><target ref="id6"/><label kind="guard" x="-96" y="-104">DB_BagClk &gt;= DB_Reservation</label></transition><transition><source ref="id8"/><target ref="id6"/><label kind="guard" x="80" y="-312">y &gt;= stopsNeeded*SD</label></transition><transition><source ref="id9"/><target ref="id4"/><label kind="guard" x="-280" y="-264">Sensor[0] == Sens_Unknown</label><label kind="synchronisation" x="-248" y="-288">go?</label><label kind="assignment" x="-248" y="-240">y := 0</label></transition><transition><source ref="id6"/><target ref="id9"/><label kind="synchronisation" x="-144" y="-400">bagReschedule!</label><label kind="assignment" x="-144" y="-376">DB_BagClk := 0,
>DB_Reservation := 10,
>FeedMov[0]:= true</label></transition><transition><source ref="id7"/><target ref="id5"/><label kind="guard" x="-96" y="8">DB_BagClk &lt; DB_Reservation</label><label kind="assignment" x="-96" y="40">y := 0,
>FeedMov[0] := false,
>stopsNeeded := 0</label><label kind="comments">Stop because destination of the new bag is different than the distribution belt.</label></transition></template><template><name>Urgent </name><location id="id10" x="-160" y="-16"></location><init ref="id10"/><transition><source ref="id10"/><target ref="id10"/><label kind="synchronisation" x="-152" y="-104">go!</label><nail x="-152" y="-24"/><nail x="-88" y="-72"/><nail x="-200" y="-88"/></transition></template><system>// Place template instantiations here.
>
>system Bag, DB_Entry, Urgent;
>
></system></nta>

Created attachment 217 [details]
query

Created attachment 218 [details]
model

This is correct attachment of the model

Fixed in rev. 4369.