diff --git a/cobot1.xml b/cobot1.xml
index 6dd709d9f333623bc4ef0a7a721238b01e6960c8..6eedb6d43a7e6ea010c7c0db85eb28fc1dc4a5cb 100644
--- a/cobot1.xml
+++ b/cobot1.xml
@@ -12,6 +12,7 @@ chan place_fail, place_success;
chan move_fail, move_success;
chan goal;
chan position_update;
+chan test_done;
int bottle_in_start_pos = 1;
int glass_in_start_pos = 1;
int glass_in_target_pos = 0;</declaration>
@@ -52,23 +53,29 @@ int glass_in_target_pos = 0;</declaration>
<location id="id5" x="-1079" y="-187">
<name x="-1173" y="-170">bottle_and_glass_end_pos</name>
</location>
- <location id="id6" x="-986" y="8">
+ <location id="id6" x="-850" y="17">
</location>
- <location id="id7" x="-986" y="-323">
- <name x="-969" y="-340">glass_back_to_start</name>
+ <location id="id7" x="-850" y="-323">
</location>
<init ref="id1"/>
+ <transition>
+ <source ref="id7"/>
+ <target ref="id5"/>
+ <label kind="synchronisation" x="-1062" y="-357">position_update?</label>
+ <label kind="assignment" x="-1062" y="-340">glass_in_target_pos = 1</label>
+ <nail x="-1079" y="-323"/>
+ </transition>
<transition>
<source ref="id4"/>
<target ref="id6"/>
- <label kind="synchronisation" x="-1283" y="-85">position_update?</label>
- <label kind="assignment" x="-1283" y="-68">glass_in_start_pos = 1</label>
+ <label kind="synchronisation" x="-1275" y="-102">position_update?</label>
+ <label kind="assignment" x="-1283" y="-85">glass_in_start_pos = 1</label>
</transition>
<transition>
<source ref="id5"/>
<target ref="id7"/>
- <label kind="synchronisation" x="-1147" y="-289">position_update?</label>
- <label kind="assignment" x="-1198" y="-272">glass_in_target_pos = 0</label>
+ <label kind="synchronisation" x="-1003" y="-238">position_update?</label>
+ <label kind="assignment" x="-1037" y="-221">glass_in_target_pos = 0</label>
</transition>
<transition>
<source ref="id3"/>
@@ -87,8 +94,8 @@ int glass_in_target_pos = 0;</declaration>
<transition>
<source ref="id7"/>
<target ref="id6"/>
- <label kind="synchronisation" x="-977" y="-272">position_update?</label>
- <label kind="assignment" x="-977" y="-255">glass_in_start_pos = 1</label>
+ <label kind="synchronisation" x="-841" y="-212">position_update?</label>
+ <label kind="assignment" x="-841" y="-195">glass_in_start_pos = 1</label>
</transition>
<transition>
<source ref="id4"/>
@@ -187,10 +194,10 @@ int glass_in_target_pos = 0;</declaration>
<location id="id13" x="-221" y="-119">
</location>
<location id="id14" x="127" y="-119">
- <name x="34" y="-153">pick_bottle</name>
+ <name x="17" y="-144">picking_bottle</name>
</location>
<location id="id15" x="578" y="-119">
- <name x="535" y="-110">move_to_glass</name>
+ <name x="535" y="-110">moving_to_glass</name>
<label kind="invariant" x="467" y="-93">bottle_in_start_pos == false</label>
</location>
<location id="id16" x="773" y="-8">
@@ -203,40 +210,45 @@ int glass_in_target_pos = 0;</declaration>
<name x="688" y="102">stop_pour</name>
</location>
<location id="id19" x="357" y="76">
- <name x="255" y="51">place_bottle</name>
+ <name x="246" y="51">placing_bottle</name>
</location>
<location id="id20" x="-246" y="76">
- <name x="-365" y="34">pick_glass</name>
+ <name x="-374" y="34">picking_glass</name>
<label kind="invariant" x="-459" y="51">bottle_in_start_pos == true</label>
</location>
<location id="id21" x="314" y="365">
- <name x="271" y="373">place_glass_target</name>
+ <name x="246" y="374">placing_glass_target</name>
</location>
<location id="id22" x="-246" y="612">
- <name x="-238" y="570">place_glass_orig</name>
+ <name x="-238" y="570">placing_glass_start</name>
</location>
<location id="id23" x="314" y="552">
<name x="314" y="569">goto_last_state</name>
</location>
<location id="id24" x="1113" y="612">
- <name x="952" y="620">goto_last_state_orig</name>
+ <name x="892" y="629">goto_last_state_before_shut_down</name>
</location>
<location id="id25" x="977" y="365">
<name x="918" y="331">move_to_start_pos</name>
</location>
- <location id="id26" x="977" y="501">
- <name x="833" y="493">finished_success</name>
+ <location id="id26" x="977" y="527">
+ <name x="841" y="518">finished_success</name>
</location>
<location id="id27" x="365" y="-119">
+ <name x="323" y="-102">bottle_picked</name>
</location>
<location id="id28" x="773" y="-119">
+ <name x="773" y="-153">moved_to_glass</name>
</location>
<location id="id29" x="-59" y="365">
+ <name x="-127" y="374">glass_picked</name>
</location>
<location id="id30" x="671" y="365">
+ <name x="603" y="331">glass_placed_target</name>
<label kind="invariant" x="595" y="382">glass_in_target_pos == true</label>
</location>
<location id="id31" x="-246" y="408">
+ <name x="-391" y="399">glass_placed_start</name>
</location>
<location id="id32" x="314" y="467">
<name x="340" y="459">stepping_back</name>
@@ -249,20 +261,46 @@ int glass_in_target_pos = 0;</declaration>
<location id="id35" x="-127" y="-221">
</location>
<location id="id36" x="535" y="76">
+ <name x="535" y="85">pouring_done</name>
</location>
<location id="id37" x="-25" y="76">
+ <name x="-17" y="51">bottle_placed</name>
+ </location>
+ <location id="id38" x="977" y="459">
+ <name x="875" y="450">in_start_pos</name>
+ </location>
+ <location id="id39" x="663" y="612">
+ <name x="578" y="629">steping_back_start</name>
+ </location>
+ <location id="id40" x="1062" y="-187">
</location>
<init ref="id33"/>
+ <transition>
+ <source ref="id40"/>
+ <target ref="id17"/>
+ <label kind="synchronisation" x="1028" y="-246">test_done!</label>
+ <nail x="1062" y="-263"/>
+ </transition>
+ <transition>
+ <source ref="id39"/>
+ <target ref="id24"/>
+ <label kind="synchronisation" x="807" y="595">move_success?</label>
+ </transition>
+ <transition>
+ <source ref="id38"/>
+ <target ref="id26"/>
+ <label kind="synchronisation" x="892" y="484">test_done!</label>
+ </transition>
<transition>
<source ref="id37"/>
<target ref="id20"/>
<label kind="synchronisation" x="-153" y="34">goal?</label>
- <label kind="assignment" x="-221" y="51">orient_constraint_set = false</label>
+ <label kind="assignment" x="-229" y="51">orient_constraint_set = false</label>
</transition>
<transition>
<source ref="id36"/>
<target ref="id19"/>
- <label kind="synchronisation" x="416" y="34">goal?</label>
+ <label kind="synchronisation" x="433" y="34">goal?</label>
<label kind="assignment" x="382" y="51">orient_constraint_set = true</label>
</transition>
<transition>
@@ -287,7 +325,7 @@ int glass_in_target_pos = 0;</declaration>
<target ref="id35"/>
<label kind="select" x="-357" y="-280">i : int[1,15]</label>
<label kind="synchronisation" x="-357" y="-263">pressed?</label>
- <label kind="assignment" x="-459" y="-246">init_retry_count = i, retry_count = init_retry_count</label>
+ <label kind="assignment" x="-442" y="-246">init_retry_count = i, retry_count = init_retry_count</label>
<nail x="-374" y="-221"/>
</transition>
<transition>
@@ -303,8 +341,8 @@ int glass_in_target_pos = 0;</declaration>
<transition>
<source ref="id31"/>
<target ref="id20"/>
- <label kind="synchronisation" x="-357" y="298">goal?</label>
- <label kind="assignment" x="-450" y="315">orient_constraint_set = false</label>
+ <label kind="synchronisation" x="-357" y="289">goal?</label>
+ <label kind="assignment" x="-450" y="306">orient_constraint_set = false</label>
</transition>
<transition>
<source ref="id30"/>
@@ -332,8 +370,9 @@ int glass_in_target_pos = 0;</declaration>
</transition>
<transition>
<source ref="id25"/>
- <target ref="id26"/>
- <label kind="synchronisation" x="858" y="450">move_success?</label>
+ <target ref="id38"/>
+ <label kind="synchronisation" x="867" y="408">move_success?</label>
+ <nail x="977" y="416"/>
</transition>
<transition>
<source ref="id21"/>
@@ -342,24 +381,24 @@ int glass_in_target_pos = 0;</declaration>
</transition>
<transition>
<source ref="id24"/>
- <target ref="id17"/>
+ <target ref="id40"/>
<label kind="synchronisation" x="1003" y="561">move_success?</label>
- <nail x="1113" y="-297"/>
+ <nail x="1113" y="-187"/>
</transition>
<transition>
<source ref="id22"/>
- <target ref="id24"/>
- <label kind="guard" x="629" y="578">retry_count == 1</label>
- <label kind="synchronisation" x="629" y="595">place_fail?</label>
+ <target ref="id39"/>
+ <label kind="guard" x="493" y="569">retry_count == 1</label>
+ <label kind="synchronisation" x="493" y="586">place_fail?</label>
</transition>
<transition>
<source ref="id20"/>
- <target ref="id17"/>
+ <target ref="id40"/>
<label kind="guard" x="578" y="170">place_glass_retry == 0</label>
<label kind="synchronisation" x="578" y="187">pickup_success?</label>
<nail x="178" y="204"/>
<nail x="1079" y="212"/>
- <nail x="1079" y="-272"/>
+ <nail x="1079" y="-153"/>
</transition>
<transition>
<source ref="id22"/>
@@ -392,7 +431,7 @@ int glass_in_target_pos = 0;</declaration>
<transition>
<source ref="id22"/>
<target ref="id22"/>
- <label kind="synchronisation" x="-400" y="664">move_success?</label>
+ <label kind="synchronisation" x="-399" y="654">move_success?</label>
<nail x="-264" y="672"/>
<nail x="-297" y="655"/>
</transition>
@@ -434,21 +473,21 @@ int glass_in_target_pos = 0;</declaration>
</transition>
<transition>
<source ref="id20"/>
- <target ref="id17"/>
+ <target ref="id40"/>
<label kind="guard" x="221" y="212">retry_count == 1</label>
<label kind="synchronisation" x="221" y="229">pickup_fail?</label>
<nail x="178" y="246"/>
<nail x="1096" y="255"/>
- <nail x="1096" y="-280"/>
+ <nail x="1096" y="-170"/>
</transition>
<transition>
<source ref="id20"/>
<target ref="id20"/>
- <label kind="guard" x="-476" y="119">retry_count > 1</label>
- <label kind="synchronisation" x="-476" y="136">pickup_fail?</label>
- <label kind="assignment" x="-476" y="153">retry_count--</label>
- <nail x="-373" y="144"/>
- <nail x="-339" y="169"/>
+ <label kind="guard" x="-425" y="110">retry_count > 1</label>
+ <label kind="synchronisation" x="-399" y="127">pickup_fail?</label>
+ <label kind="assignment" x="-399" y="144">retry_count--</label>
+ <nail x="-314" y="119"/>
+ <nail x="-297" y="136"/>
</transition>
<transition>
<source ref="id20"/>
@@ -472,11 +511,10 @@ int glass_in_target_pos = 0;</declaration>
</transition>
<transition>
<source ref="id19"/>
- <target ref="id17"/>
+ <target ref="id40"/>
<label kind="guard" x="935" y="144">retry_count == 1</label>
<label kind="synchronisation" x="960" y="161">place_fail?</label>
<nail x="1062" y="195"/>
- <nail x="1062" y="-263"/>
</transition>
<transition>
<source ref="id19"/>
@@ -492,7 +530,7 @@ int glass_in_target_pos = 0;</declaration>
<target ref="id19"/>
<label kind="synchronisation" x="374" y="136">move_success?</label>
<nail x="383" y="136"/>
- <nail x="434" y="110"/>
+ <nail x="416" y="110"/>
</transition>
<transition>
<source ref="id19"/>
@@ -548,10 +586,11 @@ int glass_in_target_pos = 0;</declaration>
</transition>
<transition>
<source ref="id14"/>
- <target ref="id17"/>
- <label kind="guard" x="416" y="-255">retry_count == 1</label>
- <label kind="synchronisation" x="433" y="-238">pickup_fail?</label>
- <nail x="425" y="-263"/>
+ <target ref="id40"/>
+ <label kind="guard" x="450" y="-272">retry_count == 1</label>
+ <label kind="synchronisation" x="450" y="-255">pickup_fail?</label>
+ <nail x="408" y="-272"/>
+ <nail x="858" y="-272"/>
</transition>
<transition>
<source ref="id14"/>
@@ -575,14 +614,27 @@ int glass_in_target_pos = 0;</declaration>
<label kind="assignment" x="-280" y="-85">init_retry_count = i, retry_count = init_retry_count</label>
</transition>
</template>
+ <template>
+ <name>testdonecatcher</name>
+ <location id="id41" x="0" y="0">
+ </location>
+ <init ref="id41"/>
+ <transition>
+ <source ref="id41"/>
+ <target ref="id41"/>
+ <label kind="synchronisation" x="8" y="-42">test_done?</label>
+ <nail x="59" y="-17"/>
+ <nail x="59" y="17"/>
+ </transition>
+ </template>
<template>
<name>positionupdatecatcher</name>
- <location id="id38" x="-544" y="-331">
+ <location id="id42" x="-544" y="-331">
</location>
- <init ref="id38"/>
+ <init ref="id42"/>
<transition>
- <source ref="id38"/>
- <target ref="id38"/>
+ <source ref="id42"/>
+ <target ref="id42"/>
<label kind="synchronisation" x="-493" y="-340">position_update?</label>
<nail x="-501" y="-357"/>
<nail x="-501" y="-306"/>
@@ -590,12 +642,12 @@ int glass_in_target_pos = 0;</declaration>
</template>
<template>
<name>positionupdate</name>
- <location id="id39" x="0" y="0">
+ <location id="id43" x="0" y="0">
</location>
- <init ref="id39"/>
+ <init ref="id43"/>
<transition>
- <source ref="id39"/>
- <target ref="id39"/>
+ <source ref="id43"/>
+ <target ref="id43"/>
<label kind="synchronisation" x="59" y="-8">position_update!</label>
<nail x="51" y="-17"/>
<nail x="51" y="17"/>
@@ -603,12 +655,12 @@ int glass_in_target_pos = 0;</declaration>
</template>
<template>
<name>goalcatcher</name>
- <location id="id40" x="-578" y="-263">
+ <location id="id44" x="-578" y="-263">
</location>
- <init ref="id40"/>
+ <init ref="id44"/>
<transition>
- <source ref="id40"/>
- <target ref="id40"/>
+ <source ref="id44"/>
+ <target ref="id44"/>
<label kind="synchronisation" x="-535" y="-272">goal?</label>
<nail x="-535" y="-280"/>
<nail x="-535" y="-246"/>
@@ -616,7 +668,7 @@ int glass_in_target_pos = 0;</declaration>
</template>
<system>// Place template instantiations here.
// List one or more processes to be composed into a system.
-system Cobot, press, move, pickup, place, goal_, goalcatcher, positionupdate, positionupdatecatcher, model_positions;
+system Cobot, press, move, pickup, place, goal_, goalcatcher, positionupdate, positionupdatecatcher, model_positions, testdonecatcher;
</system>
<queries>
<query>
diff --git a/images/cobot1.png b/images/cobot1.png
new file mode 100644
index 0000000000000000000000000000000000000000..8dcea166bbb3bee1289f35dbb87e5a7c1fbfdc01
Binary files /dev/null and b/images/cobot1.png differ
diff --git a/images/cobot1_positionen_modell.png b/images/cobot1_positionen_modell.png
new file mode 100644
index 0000000000000000000000000000000000000000..8ff3e75670be3d8f54dd58facdaec557230ef941
Binary files /dev/null and b/images/cobot1_positionen_modell.png differ
diff --git a/sections/ausfuehrung.tex b/sections/ausfuehrung.tex
index c28a2f4c99baea100d98e27ea1cd28a1c6f90423..78d5f8bccf76f59fa0a9f46e42b3a832862e5370 100644
--- a/sections/ausfuehrung.tex
+++ b/sections/ausfuehrung.tex
@@ -67,10 +67,26 @@ Der Uppaal Verifier kann mit der Anfrage \textit{A<> deadlock} (jeder Pfad führ
\subsection{Topics, Adapter und Modellanpassungen}
Als nächstes müssen ROS-Topics identifiziert werden, die die benötigten Informationen transportieren. Dazu eignet sich das Tool \textit{rostopic}\footnote{\url{http://wiki.ros.org/rostopic}}, mit welchem sich alle aktiven Topics auflisten und deren Nachrichten abhören lassen.\\
-Für den initialen Impuls des Drucksensors ist bereits ein Topic vorhanden und wird vom Cobot verwendet, kann also auch als Output vom Adapter benutzt werden. Dabei lässt sich direkt die Anzahl an erneuten Versuchen vor einem Abbruch übertragen, da diese in einer Konfigurationsdatei des Systems festgelegt wird und daher in der Konfigurationsphase des Adapters ausgelesen werden kann. In dieser Konfigurationsdatei sind auch die Startposition der Flasche sowie die Start- und Zielposition des Glases hinterlegt, sodass auch diese im Adapter gehalten werden können. Das Speichern sowie Vergleichen der Positionen von Flasche und Glas muss im Adapter erfolgen, da Uppaal TRON keine Gleitkommazahlen beim Testen unterstützt. Gazebo veröffentlicht regelmäßig über \textit{/gazebo/link\_states} und \textit{/gazebo/model\_states} die aktuellen Positionen in der Simulationsmodelle, welche folglich mit den Gewünschten im Adapter verglichen und das Ergebnis als Boolean an Uppaal weitergegeben werden kann. Für die Verwendung mit TRON müssen auch diese Booleans in Uppaal als Integer deklariert werden, was allerdings kein Problem darstellt, da innerhalb der Modelle Vergleiche mit \textit{true} oder \textit{false} möglich sind und vom Adapter einfach 0 oder 1 übertragen werden kann. Diese Aspekte schränken zwar das Modell ein und machen eine Auslagerung von Logik in den Adapter notwendig, sorgen aber gleichzeitig dafür, dass das Modell abstrakt bleibt und nicht zu detailliert wird.
-Um die Positionen der Objekte im Uppaal-System festzuhalten wurde ein separates Modell hinzugefügt, welches durch das Topic \textit{/gazebo/link\_states} aktualisiert wird und globale Variablen setzt, die durch das Modell des Cobots verwendet werden.\\
+Für den initialen Impuls des Drucksensors ist bereits ein Topic vorhanden und wird vom Cobot verwendet, kann also auch als Output vom Adapter benutzt werden. Dabei lässt sich direkt die Anzahl an erneuten Versuchen vor einem Abbruch übertragen, da diese in einer Konfigurationsdatei des Systems festgelegt wird und daher in der Konfigurationsphase des Adapters ausgelesen werden kann. In dieser Konfigurationsdatei sind auch die Startposition der Flasche sowie die Start- und Zielposition des Glases hinterlegt, sodass auch diese im Adapter gehalten werden können. Das Speichern sowie Vergleichen der Positionen von Flasche und Glas muss im Adapter erfolgen, da Uppaal TRON keine Gleitkommazahlen beim Testen unterstützt. Gazebo veröffentlicht regelmäßig über \textit{/gazebo/link\_states} und \textit{/gazebo/model\_states} die aktuellen Positionen in der Simulationsmodelle, welche folglich mit den Gewünschten im Adapter verglichen und das Ergebnis als Boolean an Uppaal weitergegeben werden kann. Für die Verwendung mit TRON müssen auch diese Booleans in Uppaal als Integer deklariert werden, was allerdings kein Problem darstellt, da innerhalb der Modelle Vergleiche mit \textit{true} oder \textit{false} möglich sind und vom Adapter einfach 0 oder 1 übertragen werden kann. Die Simulationssoftware beginnt vor dem Initialisieren der Objekte bereits mit dem Veröffentlichen von Nachrichten, sodass vom Adapter mit dem Weitergeben an TRON gewartet wird, bis die Objekte vollständig initialisiert wurden. Außerdem müssen die Positionen mit einer gewissen Toleranz verglichen werden, da (so gut wie) immer leichte Abweichungen auftreten.
+Diese Aspekte schränken zwar das Modell ein und machen eine Auslagerung von Logik in den Adapter notwendig, sorgen aber gleichzeitig dafür, dass das Modell abstrakt bleibt und nicht zu detailliert wird.
+Um die Positionen der Objekte im Uppaal-System festzuhalten wurde ein separates Modell, zu sehen in \cref{positionen_modell_bild} hinzugefügt, welches durch das Topic \textit{/gazebo/link\_states} aktualisiert wird und globale Variablen setzt, die das Modell des Cobots verwendet. Dabei musste auch darauf geachtet werden, dass fehlgeschlagene Versuche passend dargestellt sind. Das Modell des Roboters kann nur in den Zustand \textit{finished\_success} übergehen, wenn sich Flasche und Glas an der Endposition befinden.\\
+\begin{figure}[h]
+ \centering
+ \includegraphics[scale=.25]{./cobot1_positionen_modell.png}
+ \caption{Modell der Positionen von Flasche und Glas}
+ \label{cobot:positionen_modell_bild}
+\end{figure}
Für das Platzieren und Aufheben von Objekten sowie die Bewegungsplanung wird von ROS beziehungsweise MoveIt\footnote{\url{https://moveit.ros.org/}} (Framework unter anderem zur Bewegungsplanung) die actionlib verwendet, sodass sich die dort verwendeten Topics \textit{/pickup/result} und \textit{/place/result} zum Testen eignen. Die dort benutzten Nachrichten besitzen einen eigenen Typ von Fehlercode, durch welchen an TRON der Erfolg oder das Fehlschlagen einer Aktion gemeldet werden kann. Um das Modell eindeutiger zu gestalten, wurde die Variable \textit{success} durch je einen weiteren Channel für einen Fehlschlag ersetzt.\\
Für das Verfolgen von Bewegungen, welche bei der Bewegung zur Flasche, zum Glas und beim Einfüllen relevant sind wird das Topic \textit{/follow\_joint\_trajectory/result} des \textit{position\_joint\_trajectory\_controller} genutzt. Außerdem ist eine Bewegung nach dem Fehlschlagen des Platzierens vom Glas eingefügt worden, da diese hier hinzugefügt wurde, um Abstand zu gewinnen, bevor ein weiterer Versuch ausgeführt wird.
Die restlichen Bewegungen (bis auf die zur Startposition des Roboters) sind als Teilvorgänge des Platzierens und Aufhebens anzusehen, da sie an sich keine essentielle Funktion des Cobots darstellen und sind daher nicht explizit im Modell angegeben.\\
-Da logischerweise auch das Platzieren und Aufheben von Objekten Bewegungen des Arms beinhaltet, müssen bei entsprechenden Knoten im Modell zusätzliche Kanten eingefügt werden, die zum Knoten selbst zurückführen und dabei eine (nicht-) erfolgreiche Ausführung durch einen Channel abfragen. Diese Kanten sorgen dafür, dass die in \cref{cobot:formales_modell} beschriebene Validierung nicht ohne Weiteres so verwendet werden kann, da nun Endlosschleifen möglich sind. Dies könnte beispielsweise durch einen Zähler mit einer (unrealistisch hohen) maximalen Anzahl an Bewegungen realisiert sein. Für die Orientierungsbeschränkung beim Bewegen kommt nur das Topic \textit{/move\_group/goal} in Frage, da nur in diesen Nachrichten eine solche Beschränkung übergeben wird und eine Überprüfung von bereits berechneten Bewegungsbahnen aufwendig wäre. Anzumerken ist hier, dass das Einhalten einer gegebenen Beschränkung genauso wie das Aufheben oder die Bewegungen selbst nicht Teil des Tests darstellen, sondern auf den niedrigeren Testebenen (Unit-Tests oder Integrations-Tests) getestet werden müssen. Daher wird hier nur überprüft, ob eine Orientierungsbeschränkung festgelegt ist. Auch hier wäre ein Abgleich mit einer gewünschten Orientierung innerhalb des Adapters möglich, diese ist jedoch hier nicht zwingend nötig, da eine falsche Orientierung bei einer Simulation extrem auffällig wäre und daher hier ausgeschlossen werden kann. Bei genauerer Analyse des Cobots sind weitere Bewegungsbeschränkungen wie etwa bei der Beschleunigung aufgefallen, diese würden dem gleichen Schema folgen.\\
-Da innerhalb von jedem Modell-Zustand Nachrichten an \textit{/move\_group/goal} gesendet werden, für das Testen allerdings nur eine Änderung bei der Orientierungsbeschränkung relevant ist, wird in das Uppaal-System ein weiteres Modell integriert, welches Outputs an den entsprechenden Channel entgegennimmt, wenn keine Änderung erfolgte. Das gleiche Prinzip wird auf den Channel angewandt, welcher den Drucksensor repräsentiert.
\ No newline at end of file
+Da logischerweise auch das Platzieren und Aufheben von Objekten Bewegungen des Arms beinhaltet, müssen bei entsprechenden Knoten im Modell zusätzliche Kanten eingefügt werden, die zum Knoten selbst zurückführen und dabei eine (nicht-) erfolgreiche Ausführung durch einen Channel abfragen. Diese Kanten sorgen dafür, dass die in \cref{cobot:formales_modell} beschriebene Validierung nicht ohne Weiteres so verwendet werden kann, da nun Endlosschleifen möglich sind. Dies könnte beispielsweise durch einen Zähler mit einer (unrealistisch hohen) maximalen Anzahl an Bewegungen realisiert sein. Für die Orientierungsbeschränkung beim Bewegen kommen nur Topics die ein Ziel festlegen (\textit{/move\_group/goal}, \textit{/pickup/goal}, \textit{/place/goal}) in Frage, da nur in diesen Nachrichten eine solche Beschränkung übergeben wird und eine Überprüfung von bereits berechneten Bewegungsbahnen aufwendig wäre. Anzumerken ist hier, dass das Einhalten einer gegebenen Beschränkung genauso wie das Aufheben oder die Bewegungen selbst nicht Teil des Tests darstellen, sondern auf den niedrigeren Testebenen (Unit-Tests oder Integrations-Tests) getestet werden müssen. Daher wird hier nur überprüft, ob eine Orientierungsbeschränkung festgelegt ist. Auch hier wäre ein Abgleich mit einer gewünschten Orientierung innerhalb des Adapters möglich, diese ist jedoch hier nicht zwingend nötig, da eine falsche Orientierung bei einer Simulation extrem auffällig wäre und daher hier ausgeschlossen werden kann. Bei genauerer Analyse des Cobots sind weitere Bewegungsbeschränkungen wie etwa bei der Beschleunigung aufgefallen, diese würden dem gleichen Schema folgen.\\
+Da innerhalb von jedem Modell-Zustand Nachrichten an \textit{goal} gesendet werden, für das Testen allerdings nur eine Änderung bei der Orientierungsbeschränkung relevant ist, wird in das Uppaal-System ein weiteres Modell integriert, welches Outputs an den entsprechenden Channel entgegennimmt, wenn keine Änderung erfolgte. Das gleiche Prinzip wird auf den Channel angewandt, welcher den Drucksensor repräsentiert.\\
+Das endgültige Testmodell für den Cobot (ohne die erwähnten Zusatzmodelle, siehe Anhang) ist in \cref{cobot:modell_bild} abgebildet.
+\begin{figure}[h]
+ \centering
+ \includegraphics[scale=.22, angle=90]{./cobot1.png}
+ \caption{Modell des Cobot-Verhaltens}
+ \label{cobot:modell_bild}
+\end{figure}
+
+\subsection{Testausführung}
\ No newline at end of file