Bug 472 - Verification hangs, even though model is deterministic and small.
Summary: Verification hangs, even though model is deterministic and small.
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.8
Hardware: PC Linux
: P1 major
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2009-06-17 17:42 CEST by edgar
Modified: 2009-08-04 12:08 CEST (History)
0 users

See Also:
Architecture:


Attachments
wrong file (2.92 KB, text/plain)
2009-06-17 17:43 CEST, edgar
Details
query (223 bytes, application/octet-stream)
2009-06-17 17:49 CEST, edgar
Details
model (5.67 KB, application/xml)
2009-06-17 17:55 CEST, edgar
Details

Note You need to log in before you can comment on or make changes to this bug.
Description edgar 2009-06-17 17:42:18 CEST
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)].
Comment 1 edgar 2009-06-17 17:43:52 CEST
Created attachment 216 [details]
wrong file
Comment 2 edgar 2009-06-17 17:49:13 CEST
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>
Comment 3 edgar 2009-06-17 17:49:41 CEST
Created attachment 217 [details]
query
Comment 4 edgar 2009-06-17 17:55:37 CEST
Created attachment 218 [details]
model

This is correct attachment of the model
Comment 5 Alexandre David 2009-08-04 12:08:06 CEST
Fixed in rev. 4369.