diff --git a/cobot1.xml b/cobot1.xml index 48ec2e85a6764ebb49ba200694764bb8492be63e..94002a9b30dcc0d9ba8edb44bd6672efad0a293a 100644 --- a/cobot1.xml +++ b/cobot1.xml @@ -193,6 +193,7 @@ int glass_in_target_pos = 0;</declaration> </location> <location id="id15" x="595" y="42"> <name x="578" y="25">move_to_glass</name> + <label kind="invariant" x="501" y="59">bottle_in_start_pos == false</label> </location> <location id="id16" x="1020" y="59"> <name x="926" y="68">start_pour</name> diff --git a/cobot1_v1.xml b/cobot1_v1.xml new file mode 100644 index 0000000000000000000000000000000000000000..2ecf333e5e22e658248cb33d64cbf3f63d7e22fa --- /dev/null +++ b/cobot1_v1.xml @@ -0,0 +1,379 @@ +<?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_2.dtd'> +<nta> + <declaration>// Place global declarations here. +int init_retry, retry; +int glass_retry; +bool successful; +bool orient_constraint_set; +chan pressure_signal; +chan move_to_bottle_pos; +chan move_to_glass_start, move_to_glass_end; +chan start_pour, stop_pour; +chan bottle_pickup, bottle_place; +chan glass_pickup, glass_place_start, glass_place_target; +chan move_to_start_pos;</declaration> + <template> + <name x="5" y="5">Cobot</name> + <declaration>// Place local declarations here.</declaration> + <location id="id0" x="-510" y="-365"> + </location> + <location id="id1" x="-340" y="-187"> + </location> + <location id="id2" x="-119" y="-187"> + </location> + <location id="id3" x="221" y="-187"> + </location> + <location id="id4" x="221" y="-17"> + <name x="238" y="-42">pouring</name> + </location> + <location id="id5" x="-8" y="-17"> + </location> + <location id="id6" x="-331" y="-17"> + </location> + <location id="id7" x="-510" y="-17"> + </location> + <location id="id8" x="-161" y="-17"> + </location> + <location id="id9" x="-510" y="-187"> + </location> + <location id="id10" x="-510" y="119"> + </location> + <location id="id11" x="-272" y="119"> + </location> + <location id="id12" x="17" y="119"> + </location> + <location id="id13" x="255" y="119"> + <name x="272" y="127">finished_success</name> + </location> + <location id="id14" x="-340" y="-365"> + <committed/> + </location> + <location id="id15" x="306" y="-365"> + <name x="331" y="-365">shut_down</name> + </location> + <location id="id16" x="-161" y="-119"> + <committed/> + </location> + <location id="id17" x="-731" y="-17"> + <committed/> + </location> + <location id="id18" x="-272" y="212"> + <committed/> + </location> + <location id="id19" x="-42" y="212"> + </location> + <location id="id20" x="-42" y="297"> + <committed/> + </location> + <location id="id21" x="272" y="212"> + <committed/> + </location> + <init ref="id0"/> + <transition> + <source ref="id7"/> + <target ref="id15"/> + <label kind="guard" x="221" y="42">glass_retry == 0</label> + <label kind="synchronisation" x="229" y="8">glass_pickup?</label> + <label kind="assignment" x="221" y="25">successful = true</label> + <nail x="-272" y="59"/> + <nail x="357" y="59"/> + <nail x="357" y="-246"/> + </transition> + <transition> + <source ref="id21"/> + <target ref="id15"/> + <label kind="guard" x="306" y="195">retry == 1</label> + <nail x="416" y="212"/> + <nail x="416" y="-212"/> + </transition> + <transition> + <source ref="id21"/> + <target ref="id19"/> + <label kind="guard" x="153" y="255">retry > 1</label> + <label kind="assignment" x="161" y="272">retry--</label> + <nail x="161" y="255"/> + </transition> + <transition> + <source ref="id19"/> + <target ref="id21"/> + <label kind="synchronisation" x="102" y="170">glass_place_start?</label> + <label kind="assignment" x="93" y="187">successful = false</label> + </transition> + <transition> + <source ref="id20"/> + <target ref="id7"/> + <label kind="assignment" x="-578" y="280">glass_retry--</label> + <nail x="-629" y="297"/> + </transition> + <transition> + <source ref="id19"/> + <target ref="id20"/> + <label kind="synchronisation" x="-34" y="255">glass_place_start?</label> + <label kind="assignment" x="-34" y="272">successful = true</label> + </transition> + <transition> + <source ref="id18"/> + <target ref="id19"/> + <label kind="guard" x="-195" y="195">retry == 1</label> + <label kind="assignment" x="-221" y="212">retry = init_retry</label> + </transition> + <transition> + <source ref="id18"/> + <target ref="id11"/> + <label kind="guard" x="-391" y="153">retry > 1</label> + <label kind="assignment" x="-374" y="170">retry--</label> + <nail x="-331" y="170"/> + </transition> + <transition> + <source ref="id11"/> + <target ref="id18"/> + <label kind="synchronisation" x="-263" y="144">glass_place_target?</label> + <label kind="assignment" x="-263" y="161">successful = false</label> + </transition> + <transition> + <source ref="id17"/> + <target ref="id15"/> + <label kind="guard" x="-731" y="-518">retry == 1</label> + <nail x="-731" y="-501"/> + <nail x="297" y="-501"/> + </transition> + <transition> + <source ref="id17"/> + <target ref="id7"/> + <label kind="guard" x="-714" y="51">retry > 1</label> + <label kind="assignment" x="-714" y="68">retry--</label> + <nail x="-620" y="59"/> + </transition> + <transition> + <source ref="id7"/> + <target ref="id17"/> + <label kind="synchronisation" x="-663" y="-59">glass_pickup?</label> + <label kind="assignment" x="-688" y="-34">successful = false</label> + </transition> + <transition> + <source ref="id16"/> + <target ref="id15"/> + <label kind="guard" x="-68" y="-136">retry == 1</label> + <nail x="306" y="-119"/> + </transition> + <transition> + <source ref="id16"/> + <target ref="id8"/> + <label kind="guard" x="-85" y="-93">retry > 1</label> + <label kind="assignment" x="-85" y="-68">retry--</label> + <nail x="-85" y="-68"/> + </transition> + <transition> + <source ref="id8"/> + <target ref="id16"/> + <label kind="synchronisation" x="-297" y="-119">bottle_place?</label> + <label kind="assignment" x="-340" y="-102">successful = false</label> + <nail x="-229" y="-68"/> + </transition> + <transition> + <source ref="id14"/> + <target ref="id15"/> + <label kind="guard" x="-322" y="-399">retry == 1</label> + </transition> + <transition> + <source ref="id14"/> + <target ref="id1"/> + <label kind="guard" x="-280" y="-331">retry > 1</label> + <label kind="assignment" x="-272" y="-314">retry--</label> + <nail x="-255" y="-280"/> + </transition> + <transition> + <source ref="id1"/> + <target ref="id14"/> + <label kind="synchronisation" x="-450" y="-314">bottle_pickup?</label> + <label kind="assignment" x="-459" y="-297">successful = false</label> + </transition> + <transition> + <source ref="id12"/> + <target ref="id13"/> + <label kind="synchronisation" x="51" y="93">move_to_start_pos?</label> + </transition> + <transition> + <source ref="id11"/> + <target ref="id12"/> + <label kind="synchronisation" x="-204" y="85">glass_place_target?</label> + <label kind="assignment" x="-204" y="102">successful = true</label> + </transition> + <transition> + <source ref="id10"/> + <target ref="id11"/> + <label kind="synchronisation" x="-467" y="102">move_to_glass_end?</label> + <label kind="assignment" x="-467" y="119">retry = init_retry</label> + </transition> + <transition> + <source ref="id7"/> + <target ref="id10"/> + <label kind="guard" x="-510" y="76">glass_retry > 1</label> + <label kind="synchronisation" x="-510" y="42">glass_pickup?</label> + <label kind="assignment" x="-510" y="59">successful = true, orient_constraint_set = true</label> + </transition> + <transition> + <source ref="id8"/> + <target ref="id6"/> + <label kind="synchronisation" x="-280" y="-17">bottle_place?</label> + <label kind="assignment" x="-408" y="0">successful = true, retry = init_retry, orient_constraint_set = false</label> + </transition> + <transition> + <source ref="id9"/> + <target ref="id1"/> + <label kind="synchronisation" x="-501" y="-204">move_to_bottle_pos?</label> + </transition> + <transition> + <source ref="id6"/> + <target ref="id7"/> + <label kind="synchronisation" x="-501" y="-68">move_to_glass_start?</label> + <label kind="assignment" x="-510" y="-51">glass_retry = init_retry</label> + </transition> + <transition> + <source ref="id5"/> + <target ref="id8"/> + <label kind="synchronisation" x="-136" y="-34">move_to_bottle_pos?</label> + </transition> + <transition> + <source ref="id4"/> + <target ref="id5"/> + <label kind="synchronisation" x="51" y="-34">stop_pour?</label> + <label kind="assignment" x="17" y="-17">orient_constraint_set = true</label> + </transition> + <transition> + <source ref="id3"/> + <target ref="id4"/> + <label kind="synchronisation" x="153" y="-170">start_pour?</label> + <label kind="assignment" x="68" y="-153">orient_constraint_set = false</label> + </transition> + <transition> + <source ref="id2"/> + <target ref="id3"/> + <label kind="synchronisation" x="-68" y="-212">move_to_glass_start?</label> + </transition> + <transition> + <source ref="id1"/> + <target ref="id2"/> + <label kind="synchronisation" x="-280" y="-187">bottle_pickup?</label> + <label kind="assignment" x="-433" y="-170">successful = true, retry = init_retry, orient_constraint_set = true</label> + </transition> + <transition> + <source ref="id0"/> + <target ref="id9"/> + <label kind="select" x="-629" y="-340">i : int[5,10]</label> + <label kind="synchronisation" x="-637" y="-323">pressure_signal?</label> + <label kind="assignment" x="-731" y="-306">init_retry = i, retry = init_retry</label> + </transition> + </template> + <template> + <name>channels</name> + <location id="id22" x="-561" y="-144"> + <committed/> + </location> + <init ref="id22"/> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-697" y="-408">move_to_start_pos!</label> + <nail x="-680" y="-391"/> + <nail x="-595" y="-391"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-892" y="-382">glass_place_target!</label> + <nail x="-561" y="-153"/> + <nail x="-807" y="-340"/> + <nail x="-748" y="-365"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-977" y="-297">glass_place_start!</label> + <nail x="-867" y="-255"/> + <nail x="-841" y="-297"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-960" y="-204">glass_pickup!</label> + <nail x="-867" y="-187"/> + <nail x="-858" y="-221"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-943" y="-102">bottle_place!</label> + <nail x="-850" y="-93"/> + <nail x="-850" y="-119"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-884" y="0">bottle_pickup!</label> + <nail x="-782" y="-8"/> + <nail x="-807" y="-34"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-739" y="85">stop_pour!</label> + <nail x="-671" y="59"/> + <nail x="-722" y="25"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-578" y="76">start_pour!</label> + <nail x="-535" y="59"/> + <nail x="-595" y="68"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-425" y="-17">move_to_glass_end!</label> + <nail x="-433" y="0"/> + <nail x="-493" y="42"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-340" y="-93">move_to_glass_start!</label> + <nail x="-340" y="-110"/> + <nail x="-340" y="-51"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-340" y="-221">move_to_bottle_pos!</label> + <nail x="-340" y="-246"/> + <nail x="-331" y="-187"/> + </transition> + <transition> + <source ref="id22"/> + <target ref="id22"/> + <label kind="synchronisation" x="-425" y="-374">pressure_signal!</label> + <nail x="-459" y="-382"/> + <nail x="-391" y="-306"/> + </transition> + </template> + <system>// Place template instantiations here. +// List one or more processes to be composed into a system. +system Cobot, channels; + </system> + <queries> + <query> + <formula>A[] (deadlock imply (Cobot.finished_success or Cobot.shut_down))</formula> + <comment></comment> + </query> + <query> + <formula>A[] ((Cobot.finished_success or Cobot.shut_down) imply deadlock)</formula> + <comment></comment> + </query> + <query> + <formula>A<> (Cobot.finished_success or Cobot.shut_down)</formula> + <comment></comment> + </query> + </queries> +</nta>