The simulation is deterministic (at each step only one transition is allowed).
But Uppall server is unable to finish verification.

The are two queries, which just test if it is possible to reach locations of
Bag automaton. Uppall can verify the first one, but hangs on the second.


The model works correctly with dev version of Uppaal [4.1.1 (rev. 4276)].

Created an attachment (id=216) [details]
model

(From update of attachment 216 [details])
><?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 an attachment (id=217) [details]
query

Created an attachment (id=218) [details]
model

This is correct attachment of the model

Fixed in rev. 4369.