API tools faq
paste
Guest User

pcs.xml

a guest
Aug 8th, 2015
175
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
XML 12.69 KB | None | 0 0
raw download clone embed print report
  1. <?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.
  2.  
  3. const int SENSORS   = 8;      // amount of sensors
  4. const int POSITIONS = 8;      // amount of distinguishable positions that a block can have
  5.  
  6. typedef int[1,SENSORS] id_s;  // sensor ID type
  7.  
  8. chan Go_event;
  9.  
  10. chan FB_blocked_event, FB_Wait_event, FB_Run_event;
  11. chan FE_mv_fwd_event,FE_ReeledOut_event;
  12. chan error_event;
  13. bool error;
  14. bool FB_Running, FB_Waiting;
  15.  
  16. bool FE_MovingFwd, FE_MovingBwd;
  17.  
  18. bool FE_DrawnIn, FE_EndStopIn;
  19. bool FE_ReeledOut, FE_EndStopOut;
  20.  
  21. bool sensor[SENSORS+1]={true,true,true,true,true,true,true,true,true};
  22. //bool sensor1=true;
  23. //bool sensor7=true;
  24.  
  25. // BLOCKS
  26.  
  27. bool BlockAtPos[POSITIONS+1];
  28.  
  29. chan BlockAtPos_event[POSITIONS+1];</declaration><template><name x="5" y="5">FB_FeederBelt</name><declaration>// Place local declarations here.
  30. </declaration><location id="id0" x="-512" y="-400"><name x="-496" y="-416">Run</name><label kind="invariant" x="-522" y="-385">FB_Running || sensor[1] || FE_DrawnIn</label></location><location id="id1" x="-944" y="-400"><name x="-1024" y="-416">WaitStop</name><label kind="invariant" x="-1024" y="-384">FB_Waiting</label><label kind="comments">FB has to wait since FE became stuck or
  31. is busy. This is represented by (OR)..........
  32. - moving FE ..............................................
  33. - Sensor1 == 0 (active)............................</label></location><location id="id2" x="-512" y="-640"><name x="-496" y="-664">ErrorStop</name><label kind="invariant" x="-496" y="-648">error</label></location><location id="id3" x="-944" y="-640"><name x="-954" y="-670">Start</name></location><init ref="id3"/><transition><source ref="id3"/><target ref="id0"/><label kind="guard" x="-856" y="-608">!sensor[7]</label><label kind="assignment" x="-832" y="-592">FB_Running = true</label></transition><transition><source ref="id1"/><target ref="id2"/><label kind="synchronisation" x="-680" y="-616">error_event?</label></transition><transition><source ref="id3"/><target ref="id1"/><label kind="guard" x="-1080" y="-600">sensor[7]</label><label kind="assignment" x="-1080" y="-584">FB_Waiting = true</label></transition><transition><source ref="id3"/><target ref="id2"/><label kind="synchronisation" x="-744" y="-664">error_event?</label></transition><transition><source ref="id0"/><target ref="id2"/><label kind="synchronisation" x="-608" y="-576">error_event?</label></transition><transition><source ref="id1"/><target ref="id0"/><label kind="guard" x="-784" y="-304">!sensor[7]</label><label kind="assignment" x="-784" y="-288">FB_Running = true</label><nail x="-816" y="-312"/><nail x="-632" y="-312"/></transition><transition><source ref="id0"/><target ref="id1"/><label kind="guard" x="-784" y="-392">!sensor[1] || !FE_EndStopIn</label><label kind="assignment" x="-784" y="-376">FB_Waiting = true</label><nail x="-616" y="-400"/><nail x="-800" y="-400"/></transition></template><template><name>FE_Feeder</name><location id="id4" x="-560" y="-432"><name x="-570" y="-462">Start</name></location><location id="id5" x="-416" y="-192"><name x="-400" y="-208">MovingBwd</name><label kind="invariant" x="-400" y="-192">FE_MovingBwd</label></location><location id="id6" x="-720" y="-184"><name x="-704" y="-200">MovingFwd</name><label kind="invariant" x="-704" y="-184">FE_MovingFwd</label></location><location id="id7" x="-560" y="-120"><name x="-584" y="-104">ReeledOut</name><label kind="invariant" x="-592" y="-88">FE_ReeledOut</label></location><location id="id8" x="-560" y="-256"><name x="-584" y="-240">DrawnIn</name><label kind="invariant" x="-600" y="-224">FE_DrawnIn</label></location><init ref="id4"/><transition><source ref="id4"/><target ref="id8"/><label kind="assignment" x="-552" y="-352">FE_DrawnIn=true,
  34. FE_EndStopIn=true</label><label kind="comments">Homing..</label></transition><transition><source ref="id5"/><target ref="id8"/><label kind="assignment" x="-416" y="-288">FE_EndStopIn=true,
  35. FE_DrawnIn=true,
  36. FE_MovingBwd=false</label><nail x="-416" y="-256"/></transition><transition><source ref="id7"/><target ref="id5"/><label kind="assignment" x="-416" y="-112">FE_EndStopOut=false,
  37. FE_ReeledOut=false,
  38. FE_MovingBwd=true</label><nail x="-416" y="-120"/></transition><transition><source ref="id6"/><target ref="id7"/><label kind="synchronisation" x="-872" y="-128">FE_ReeledOut_event!</label><label kind="assignment" x="-872" y="-112">FE_EndStopOut=true,
  39. FE_ReeledOut=true,
  40. FE_MovingFwd=false</label><nail x="-720" y="-120"/></transition><transition><source ref="id8"/><target ref="id6"/><label kind="guard" x="-880" y="-288">!sensor[1]</label><label kind="synchronisation" x="-880" y="-304">FE_mv_fwd_event!</label><label kind="assignment" x="-880" y="-272">FE_EndStopIn=false,
  41. FE_DrawnIn=false,
  42. FE_MovingFwd=true</label><nail x="-720" y="-256"/></transition></template><template><name>Molder</name><location id="id9" x="0" y="0"></location><init ref="id9"/></template><template><name>Extractor</name><location id="id10" x="0" y="0"></location><init ref="id10"/></template><template><name>ExtractionBelt</name><location id="id11" x="0" y="0"></location><init ref="id11"/></template><template><name>Rotator</name><location id="id12" x="0" y="0"></location><init ref="id12"/></template><template><name>Sensor</name><parameter>const id_s sid</parameter><location id="id13" x="-256" y="-320"><name x="-266" y="-350">Start</name></location><location id="id14" x="-256" y="64"><name x="-232" y="56">Active_0</name><label kind="invariant" x="-266" y="79">BlockAtPos[sid] || FE_MovingFwd || FE_ReeledOut</label><label kind="comments">Object detection.</label></location><location id="id15" x="-256" y="-224"><name x="-240" y="-248">Inactive_1</name><label kind="invariant" x="-232" y="-224">sensor[sid]</label><label kind="comments">No object detected.</label></location><init ref="id13"/><transition><source ref="id13"/><target ref="id15"/><label kind="assignment" x="-224" y="-272">sensor[sid]=true</label></transition><transition><source ref="id14"/><target ref="id14"/><nail x="-320" y="128"/><nail x="-192" y="128"/></transition><transition><source ref="id14"/><target ref="id15"/><label kind="guard" x="-168" y="-104">!BlockAtPos[sid] &amp;&amp; !FE_MovingFwd &amp;&amp; FE_ReeledOut</label><label kind="assignment" x="-168" y="-88">sensor[sid] = false</label><nail x="-192" y="-32"/><nail x="-192" y="-128"/></transition><transition><source ref="id15"/><target ref="id14"/><label kind="guard" x="-480" y="-104">BlockAtPos[sid]</label><label kind="assignment" x="-480" y="-88">sensor[sid] = true</label><nail x="-320" y="-128"/><nail x="-320" y="-32"/></transition></template><template><name>BlockCycle</name><location id="id16" x="-768" y="-256"><name x="-778" y="-286">Start</name></location><location id="id17" x="-96" y="64"><name x="-80" y="40">Pos4_5</name></location><location id="id18" x="-432" y="-256"><name x="-442" y="-286">Pos6_7</name></location><location id="id19" x="-424" y="160"><name x="-408" y="136">Pos2</name></location><location id="id20" x="-96" y="-128"><name x="-80" y="-152">Pos6</name></location><location id="id21" x="-96" y="-40"><name x="-80" y="-64">Pos5</name></location><location id="id22" x="-96" y="160"><name x="-88" y="136">Pos4</name></location><location id="id23" x="-256" y="160"><name x="-248" y="136">Pos2_4</name></location><location id="id24" x="-592" y="160"><name x="-584" y="136">Pos1_2</name></location><location id="id25" x="-768" y="160"><name x="-760" y="136">Pos1</name></location><location id="id26" x="-768" y="64"><name x="-760" y="40">Pos8</name></location><location id="id27" x="-768" y="-64"><name x="-760" y="-88">Pos7</name></location><init ref="id16"/><transition><source ref="id16"/><target ref="id27"/><label kind="assignment" x="-760" y="-240">BlockAtPos[7] = true</label></transition><transition><source ref="id18"/><target ref="id27"/><label kind="assignment" x="-624" y="-216">BlockAtPos[7] = true</label><nail x="-480" y="-256"/><nail x="-552" y="-248"/><nail x="-600" y="-232"/><nail x="-664" y="-192"/><nail x="-720" y="-144"/></transition><transition><source ref="id20"/><target ref="id18"/><label kind="assignment" x="-384" y="-216">BlockAtPos[6] = false</label><nail x="-136" y="-168"/><nail x="-192" y="-208"/><nail x="-256" y="-232"/><nail x="-328" y="-248"/><nail x="-400" y="-256"/></transition><transition><source ref="id22"/><target ref="id17"/><label kind="assignment" x="-256" y="88">BlockAtPos[4] = false</label></transition><transition><source ref="id17"/><target ref="id21"/><label kind="assignment" x="-256" y="-8">BlockAtPos[5] = true</label></transition><transition><source ref="id19"/><target ref="id23"/><label kind="assignment" x="-416" y="184">BlockAtPos[2] = false</label></transition><transition><source ref="id24"/><target ref="id19"/><label kind="synchronisation" x="-584" y="208">FE_ReeledOut_event?</label><label kind="assignment" x="-584" y="184">BlockAtPos[2] = true</label></transition><transition><source ref="id21"/><target ref="id20"/><label kind="assignment" x="-256" y="-96">BlockAtPos[6] = true,
  43. BlockAtPos[5] = false</label></transition><transition><source ref="id23"/><target ref="id22"/><label kind="assignment" x="-240" y="184">BlockAtPos[4] = true</label></transition><transition><source ref="id25"/><target ref="id24"/><label kind="synchronisation" x="-752" y="208">FE_mv_fwd_event?</label><label kind="assignment" x="-752" y="184">BlockAtPos[1] = false</label></transition><transition><source ref="id26"/><target ref="id25"/><label kind="guard" x="-752" y="80">FB_Running</label><label kind="assignment" x="-752" y="96">BlockAtPos[1] = true,
  44. BlockAtPos[8] = false</label></transition><transition><source ref="id27"/><target ref="id26"/><label kind="guard" x="-752" y="-32">FB_Running</label><label kind="assignment" x="-752" y="-16">BlockAtPos[8] = true,
  45. BlockAtPos[7] = false</label></transition></template><template><name>Sensor1</name><location id="id28" x="-512" y="-352"><name x="-496" y="-376">InActive_1</name><label kind="invariant" x="-488" y="-352">sensor[1]</label></location><location id="id29" x="-512" y="-64"><name x="-522" y="-94">Active_0</name><label kind="invariant" x="-522" y="-49">BlockAtPos[1] ||
  46. FE_MovingFwd ||
  47. FE_ReeledOut</label></location><location id="id30" x="-512" y="-448"><name x="-522" y="-478">Start</name></location><init ref="id30"/><transition><source ref="id30"/><target ref="id28"/><label kind="assignment" x="-480" y="-400">sensor[1]=true</label></transition><transition><source ref="id28"/><target ref="id29"/><label kind="guard" x="-416" y="-232">!BlockAtPos[1] &amp;&amp;
  48. !FE_MovingFwd &amp;&amp;
  49.  FE_ReeledOut &amp;&amp;
  50. !FE_MovingBwd</label><label kind="assignment" x="-416" y="-176">sensor[1]=true</label><nail x="-448" y="-256"/><nail x="-448" y="-160"/></transition><transition><source ref="id28"/><target ref="id29"/><label kind="guard" x="-704" y="-232">BlockAtPos[1]</label><label kind="assignment" x="-704" y="-217">sensor[1] = false</label><nail x="-576" y="-256"/><nail x="-576" y="-160"/></transition><transition><source ref="id29"/><target ref="id29"/><nail x="-576" y="0"/><nail x="-440" y="0"/></transition></template><template><name>Sensor7</name><location id="id31" x="-448" y="-96"><name x="-458" y="-126">Active_0</name><label kind="invariant" x="-458" y="-81">BlockAtPos[7]</label></location><location id="id32" x="-448" y="-384"><name x="-432" y="-408">InActive_1</name><label kind="invariant" x="-424" y="-384">sensor[7]</label></location><location id="id33" x="-448" y="-480"><name x="-458" y="-510">Start</name></location><init ref="id33"/><transition><source ref="id31"/><target ref="id31"/><nail x="-512" y="-32"/><nail x="-384" y="-32"/></transition><transition><source ref="id31"/><target ref="id32"/><label kind="guard" x="-352" y="-264">!BlockAtPos[7]</label><label kind="assignment" x="-352" y="-248">sensor[7]=true</label><nail x="-384" y="-192"/><nail x="-384" y="-288"/></transition><transition><source ref="id32"/><target ref="id31"/><label kind="guard" x="-672" y="-264">BlockAtPos[7]</label><label kind="assignment" x="-672" y="-248">sensor[7] = false</label><nail x="-512" y="-288"/><nail x="-512" y="-192"/></transition><transition><source ref="id33"/><target ref="id32"/><label kind="assignment" x="-416" y="-432">sensor[7]=true</label></transition></template><template><name>Main</name><location id="id34" x="-448" y="-128"><name x="-432" y="-152">On</name></location><location id="id35" x="-448" y="-256"><name x="-432" y="-280">Off</name></location><init ref="id35"/><transition><source ref="id35"/><target ref="id34"/><label kind="synchronisation" x="-432" y="-208">Go_event!</label></transition></template><system>
  51. // List one or more processes to be composed into a system.
  52. system FB_FeederBelt, Sensor, BlockCycle, FE_Feeder;</system></nta>
Advertisement
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!