Skip to content
Snippets Groups Projects
Commit eafb74d7 authored by Christoph Schröter's avatar Christoph Schröter
Browse files

No commit message 

No commit message
parent 420ab135
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
cobot1.xml
+ 1
− 0
View file @ eafb74d7
...@@ -193,6 +193,7 @@ int glass_in_target_pos = 0;</declaration> ...@@ -193,6 +193,7 @@ int glass_in_target_pos = 0;</declaration>
</location> </location>
<location id="id15" x="595" y="42"> <location id="id15" x="595" y="42">
<name x="578" y="25">move_to_glass</name> <name x="578" y="25">move_to_glass</name>
<label kind="invariant" x="501" y="59">bottle_in_start_pos == false</label>
</location> </location>
<location id="id16" x="1020" y="59"> <location id="id16" x="1020" y="59">
<name x="926" y="68">start_pour</name> <name x="926" y="68">start_pour</name>
......
cobot1_v1.xml 0 → 100644
+ 379
− 0
View file @ eafb74d7
<?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 &gt; 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 &gt; 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 &gt; 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 &gt; 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 &gt; 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 &gt; 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&lt;&gt; (Cobot.finished_success or Cobot.shut_down)</formula>
<comment></comment>
</query>
</queries>
</nta>
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment