From 5fae06be735ddb1812671d608b8494ef736634f3 Mon Sep 17 00:00:00 2001
From: Jan Travnicek <Jan.Travnicek@fit.cvut.cz>
Date: Sun, 18 Jan 2015 22:34:55 +0100
Subject: [PATCH] RHDPDA in new internal form

---
 examples/automaton/PDA.xml      |  53 --------
 examples/automaton/RHDPDA1.xml  | 226 --------------------------------
 examples/automaton/RHDPDA2.xml  | 114 ----------------
 examples/automaton/RHDPDA3.xml  |  45 -------
 examples/automaton/RHDPDA4.xml  |  42 ------
 examples2/automaton/DPDA.xml    |  63 +++++++++
 examples2/automaton/RHDPDA1.xml |  65 +++++++++
 examples2/automaton/RHDPDA2.xml |  96 ++++++++++++++
 examples2/automaton/RHDPDA3.xml |  56 ++++++++
 examples2/automaton/RHDPDA4.xml |  40 ++++++
 10 files changed, 320 insertions(+), 480 deletions(-)
 delete mode 100644 examples/automaton/PDA.xml
 delete mode 100644 examples/automaton/RHDPDA1.xml
 delete mode 100644 examples/automaton/RHDPDA2.xml
 delete mode 100644 examples/automaton/RHDPDA3.xml
 delete mode 100644 examples/automaton/RHDPDA4.xml
 create mode 100644 examples2/automaton/DPDA.xml
 create mode 100644 examples2/automaton/RHDPDA1.xml
 create mode 100644 examples2/automaton/RHDPDA2.xml
 create mode 100644 examples2/automaton/RHDPDA3.xml
 create mode 100644 examples2/automaton/RHDPDA4.xml

diff --git a/examples/automaton/PDA.xml b/examples/automaton/PDA.xml
deleted file mode 100644
index bc44a65ead..0000000000
--- a/examples/automaton/PDA.xml
+++ /dev/null
@@ -1,53 +0,0 @@
-<automaton>
-	<states>
-		<state>a</state>
-		<state>b</state>
-	</states>
-	<inputAlphabet>
-		<symbol>{</symbol>
-		<symbol>}</symbol>
-	</inputAlphabet>
-	<stackAlphabet>
-		<symbol>0</symbol>
-	</stackAlphabet>
-	<transitions>
-		<transition>
-			<from>a</from>
-			<input>{</input>
-			<to>a</to>
-			<pop>
-			</pop>
-			<push>
-				<symbol>0</symbol>
-			</push>
-		</transition>
-		<transition>
-			<from>a</from>
-			<input>}</input>
-			<to>b</to>
-			<pop>
-				<symbol>0</symbol>
-			</pop>
-			<push>
-			</push>
-		</transition>
-		<transition>
-			<from>b</from>
-			<input>}</input>
-			<to>b</to>
-			<pop>
-				<symbol>0</symbol>
-			</pop>
-			<push>
-			</push>
-		</transition>
-
-	</transitions>
-	<initialStates>
-		<state>a</state>
-	</initialStates>
-	<startSymbols>
-	</startSymbols>
-	<finalStates>
-	</finalStates>
-</automaton>
diff --git a/examples/automaton/RHDPDA1.xml b/examples/automaton/RHDPDA1.xml
deleted file mode 100644
index b6ee03f349..0000000000
--- a/examples/automaton/RHDPDA1.xml
+++ /dev/null
@@ -1,226 +0,0 @@
-<automaton>
-  <states>
-    <state>0</state>
-    <state>1</state>
-    <state>2</state>
-    <state>3</state>
-    <state>ERR</state>
-  </states>
-  <inputAlphabet>
-    <symbol>a</symbol>
-    <symbol>b</symbol>
-  </inputAlphabet>
-  <stackAlphabet>
-    <symbol>a</symbol>
-    <symbol>x</symbol>
-    <symbol>_</symbol>
-  </stackAlphabet>
-  <transitions>
-    <transition>
-      <from>0</from>
-      <input>a</input>
-      <to>1</to>
-      <pop>
-        <symbol>_</symbol>
-      </pop>
-      <push>
-        <symbol>x</symbol>
-        <symbol>_</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>0</from>
-      <input>b</input>
-      <to>3</to>
-      <pop>
-        <symbol>_</symbol>
-      </pop>
-      <push>
-        <symbol>_</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>1</from>
-      <input>a</input>
-      <to>1</to>
-      <pop>
-        <symbol>a</symbol>
-      </pop>
-      <push>
-        <symbol>a</symbol>
-        <symbol>a</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>1</from>
-      <input>a</input>
-      <to>1</to>
-      <pop>
-        <symbol>x</symbol>
-      </pop>
-      <push>
-        <symbol>a</symbol>
-        <symbol>x</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>1</from>
-      <input>b</input>
-      <to>2</to>
-      <pop>
-        <symbol>a</symbol>
-      </pop>
-      <push>
-        <symbol>a</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>1</from>
-      <input>b</input>
-      <to>2</to>
-      <pop>
-        <symbol>x</symbol>
-      </pop>
-      <push>
-        <symbol>x</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>2</from>
-      <input>a</input>
-      <to>2</to>
-      <pop>
-        <symbol>a</symbol>
-      </pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>2</from>
-      <input>a</input>
-      <to>3</to>
-      <pop>
-        <symbol>x</symbol>
-      </pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>2</from>
-      <input>b</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>a</symbol>
-      </pop>
-      <push>
-        <symbol>a</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>2</from>
-      <input>b</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>x</symbol>
-      </pop>
-      <push>
-        <symbol>x</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>3</from>
-      <input>a</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>_</symbol>
-      </pop>
-      <push>
-        <symbol>_</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>3</from>
-      <input>b</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>_</symbol>
-      </pop>
-      <push>
-        <symbol>_</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>ERR</from>
-      <input>a</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>_</symbol>
-      </pop>
-      <push>
-        <symbol>_</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>ERR</from>
-      <input>a</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>a</symbol>
-      </pop>
-      <push>
-        <symbol>a</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>ERR</from>
-      <input>a</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>x</symbol>
-      </pop>
-      <push>
-        <symbol>x</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>ERR</from>
-      <input>b</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>_</symbol>
-      </pop>
-      <push>
-        <symbol>_</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>ERR</from>
-      <input>b</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>a</symbol>
-      </pop>
-      <push>
-        <symbol>a</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>ERR</from>
-      <input>b</input>
-      <to>ERR</to>
-      <pop>
-        <symbol>x</symbol>
-      </pop>
-      <push>
-        <symbol>x</symbol>
-      </push>
-    </transition>
-  </transitions>
-  <initialStates>
-    <state>0</state>
-  </initialStates>
-  <startSymbols>
-    <symbol>_</symbol>
-  </startSymbols>
-  <finalStates>
-    <state>3</state>
-  </finalStates>
-</automaton>
diff --git a/examples/automaton/RHDPDA2.xml b/examples/automaton/RHDPDA2.xml
deleted file mode 100644
index 772fa58790..0000000000
--- a/examples/automaton/RHDPDA2.xml
+++ /dev/null
@@ -1,114 +0,0 @@
-<automaton>
-  <states>
-    <state>0</state>
-    <state>1</state>
-    <state>2</state>
-    <state>3</state>
-    <state>ERR</state>
-  </states>
-  <inputAlphabet>
-    <symbol>a</symbol>
-    <symbol>b</symbol>
-  </inputAlphabet>
-  <stackAlphabet>
-    <symbol>a</symbol>
-    <symbol>x</symbol>
-    <symbol>_</symbol>
-  </stackAlphabet>
-  <transitions>
-    <transition>
-      <from>0</from>
-      <input>a</input>
-      <to>1</to>
-      <pop></pop>
-      <push>
-        <symbol>x</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>0</from>
-      <input>b</input>
-      <to>3</to>
-      <pop></pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>1</from>
-      <input>a</input>
-      <to>1</to>
-      <pop></pop>
-      <push>
-        <symbol>a</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>1</from>
-      <input>b</input>
-      <to>2</to>
-      <pop></pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>2</from>
-      <input>a</input>
-      <to>2</to>
-      <pop>
-        <symbol>a</symbol>
-      </pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>2</from>
-      <input>a</input>
-      <to>3</to>
-      <pop>
-        <symbol>x</symbol>
-      </pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>2</from>
-      <input>b</input>
-      <to>ERR</to>
-      <pop></pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>3</from>
-      <input>a</input>
-      <to>ERR</to>
-      <pop></pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>3</from>
-      <input>b</input>
-      <to>ERR</to>
-      <pop></pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>ERR</from>
-      <input>a</input>
-      <to>ERR</to>
-      <pop></pop>
-      <push></push>
-    </transition>
-    <transition>
-      <from>ERR</from>
-      <input>b</input>
-      <to>ERR</to>
-      <pop></pop>
-      <push></push>
-    </transition>
-  </transitions>
-  <initialStates>
-    <state>0</state>
-  </initialStates>
-  <startSymbols>
-    <symbol>_</symbol>
-  </startSymbols>
-  <finalStates>
-    <state>3</state>
-  </finalStates>
-</automaton>
diff --git a/examples/automaton/RHDPDA3.xml b/examples/automaton/RHDPDA3.xml
deleted file mode 100644
index 8ca65104a1..0000000000
--- a/examples/automaton/RHDPDA3.xml
+++ /dev/null
@@ -1,45 +0,0 @@
-<automaton>
-  <states>
-    <state>0</state>
-    <state>1</state>
-  </states>
-  <inputAlphabet>
-    <symbol>a</symbol>
-  </inputAlphabet>
-  <stackAlphabet>
-    <symbol>a</symbol>
-    <symbol>_</symbol>
-  </stackAlphabet>
-  <transitions>
-    <transition>
-      <from>0</from>
-      <input>a</input>
-      <to>1</to>
-      <pop>
-        <symbol>_</symbol>
-      </pop>
-      <push>
-        <symbol>a</symbol>
-        <symbol>_</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>1</from>
-      <input>a</input>
-      <to>0</to>
-      <pop>
-        <symbol>a</symbol>
-      </pop>
-      <push></push>
-    </transition>
-  </transitions>
-  <initialStates>
-    <state>0</state>
-  </initialStates>
-  <startSymbols>
-    <symbol>_</symbol>
-  </startSymbols>
-  <finalStates>
-    <state>0</state>
-  </finalStates>
-</automaton>
diff --git a/examples/automaton/RHDPDA4.xml b/examples/automaton/RHDPDA4.xml
deleted file mode 100644
index 91a822d4ee..0000000000
--- a/examples/automaton/RHDPDA4.xml
+++ /dev/null
@@ -1,42 +0,0 @@
-<automaton>
-  <states>
-    <state>0</state>
-    <state>1</state>
-  </states>
-  <inputAlphabet>
-    <symbol>a</symbol>
-  </inputAlphabet>
-  <stackAlphabet>
-    <symbol>a</symbol>
-    <symbol>_</symbol>
-  </stackAlphabet>
-  <transitions>
-    <transition>
-      <from>0</from>
-      <input>a</input>
-      <to>1</to>
-      <pop></pop>
-      <push>
-        <symbol>a</symbol>
-      </push>
-    </transition>
-    <transition>
-      <from>1</from>
-      <input>a</input>
-      <to>0</to>
-      <pop>
-        <symbol>a</symbol>
-      </pop>
-      <push></push>
-    </transition>
-  </transitions>
-  <initialStates>
-    <state>0</state>
-  </initialStates>
-  <startSymbols>
-    <symbol>_</symbol>
-  </startSymbols>
-  <finalStates>
-    <state>0</state>
-  </finalStates>
-</automaton>
diff --git a/examples2/automaton/DPDA.xml b/examples2/automaton/DPDA.xml
new file mode 100644
index 0000000000..2b361628e4
--- /dev/null
+++ b/examples2/automaton/DPDA.xml
@@ -0,0 +1,63 @@
+<DPDA>
+	<states>
+		<PrimitiveLabel><String>a</String></PrimitiveLabel>
+		<PrimitiveLabel><String>b</String></PrimitiveLabel>
+		<PrimitiveLabel><String>c</String></PrimitiveLabel>
+	</states>
+	<inputAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>{</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>}</Character></PrimitiveLabel></LabeledSymbol>
+	</inputAlphabet>
+	<stackAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>0</Character></PrimitiveLabel></LabeledSymbol>
+	</stackAlphabet>
+	<initialState>
+		<PrimitiveLabel><String>a</String></PrimitiveLabel>
+	</initialState>
+	<initialStackSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>0</Character></PrimitiveLabel></LabeledSymbol>
+	</initialStackSymbol>
+	<finalStates>
+	</finalStates>
+	<transitions>
+		<transition>
+			<from><PrimitiveLabel><String>a</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>{</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+			</pop>
+			<to><PrimitiveLabel><String>b</String></PrimitiveLabel></to>
+			<push>
+			</push>
+		</transition>
+		<transition>
+			<from><PrimitiveLabel><String>b</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>{</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+			</pop>
+			<to><PrimitiveLabel><String>b</String></PrimitiveLabel></to>
+			<push>
+				<LabeledSymbol><PrimitiveLabel><Character>0</Character></PrimitiveLabel></LabeledSymbol>
+			</push>
+		</transition>
+		<transition>
+			<from><PrimitiveLabel><String>b</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>}</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+				<LabeledSymbol><PrimitiveLabel><Character>0</Character></PrimitiveLabel></LabeledSymbol>
+			</pop>
+			<to><PrimitiveLabel><String>c</String></PrimitiveLabel></to>
+			<push>
+			</push>
+		</transition>
+		<transition>
+			<from><PrimitiveLabel><String>c</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>}</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+				<LabeledSymbol><PrimitiveLabel><Character>0</Character></PrimitiveLabel></LabeledSymbol>
+			</pop>
+			<to><PrimitiveLabel><String>c</String></PrimitiveLabel></to>
+			<push>
+			</push>
+		</transition>
+	</transitions>
+</DPDA>
diff --git a/examples2/automaton/RHDPDA1.xml b/examples2/automaton/RHDPDA1.xml
new file mode 100644
index 0000000000..232e256fa9
--- /dev/null
+++ b/examples2/automaton/RHDPDA1.xml
@@ -0,0 +1,65 @@
+<RealTimeHeightDeterministicNPDA>
+	<states>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+		<PrimitiveLabel><String>1</String></PrimitiveLabel>
+	</states>
+	<inputAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>b</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>c</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>d</Character></PrimitiveLabel></LabeledSymbol>
+	</inputAlphabet>
+	<stackAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>A</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>B</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>_</Character></PrimitiveLabel></LabeledSymbol>
+	</stackAlphabet>
+	<initialStates>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+	</initialStates>
+	<bottomOfTheStackSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>_</Character></PrimitiveLabel></LabeledSymbol>
+	</bottomOfTheStackSymbol>
+	<finalStates>
+		<PrimitiveLabel><String>1</String></PrimitiveLabel>
+	</finalStates>
+	<transitions>
+		<callTransition>
+			<from><PrimitiveLabel><String>0</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>0</String></PrimitiveLabel></to>
+			<push>
+				<LabeledSymbol><PrimitiveLabel><Character>A</Character></PrimitiveLabel></LabeledSymbol>
+			</push>
+		</callTransition>
+		<localTransition>
+			<from><PrimitiveLabel><String>0</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>c</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>1</String></PrimitiveLabel></to>
+		</localTransition>
+		<callTransition>
+			<from><PrimitiveLabel><String>0</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>1</String></PrimitiveLabel></to>
+			<push>
+				<LabeledSymbol><PrimitiveLabel><Character>B</Character></PrimitiveLabel></LabeledSymbol>
+			</push>
+		</callTransition>
+		<returnTransition>
+			<from><PrimitiveLabel><String>1</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>b</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+				<LabeledSymbol><PrimitiveLabel><Character>A</Character></PrimitiveLabel></LabeledSymbol>
+			</pop>
+			<to><PrimitiveLabel><String>1</String></PrimitiveLabel></to>
+		</returnTransition>
+		<returnTransition>
+			<from><PrimitiveLabel><String>1</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>d</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+				<LabeledSymbol><PrimitiveLabel><Character>B</Character></PrimitiveLabel></LabeledSymbol>
+			</pop>
+			<to><PrimitiveLabel><String>1</String></PrimitiveLabel></to>
+		</returnTransition>
+	</transitions>
+</RealTimeHeightDeterministicNPDA>
diff --git a/examples2/automaton/RHDPDA2.xml b/examples2/automaton/RHDPDA2.xml
new file mode 100644
index 0000000000..d3323fa25a
--- /dev/null
+++ b/examples2/automaton/RHDPDA2.xml
@@ -0,0 +1,96 @@
+<RealTimeHeightDeterministicNPDA>
+	<states>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+		<PrimitiveLabel><String>1</String></PrimitiveLabel>
+		<PrimitiveLabel><String>2</String></PrimitiveLabel>
+		<PrimitiveLabel><String>3</String></PrimitiveLabel>
+		<PrimitiveLabel><String>ERR</String></PrimitiveLabel>
+	</states>
+	<inputAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>b</Character></PrimitiveLabel></LabeledSymbol>
+	</inputAlphabet>
+	<stackAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>x</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>_</Character></PrimitiveLabel></LabeledSymbol>
+	</stackAlphabet>
+	<initialStates>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+	</initialStates>
+	<bottomOfTheStackSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>_</Character></PrimitiveLabel></LabeledSymbol>
+	</bottomOfTheStackSymbol>
+	<finalStates>
+		<PrimitiveLabel><String>3</String></PrimitiveLabel>
+	</finalStates>
+	<transitions>
+		<callTransition>
+			<from><PrimitiveLabel><String>0</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>1</String></PrimitiveLabel></to>
+			<push>
+				<LabeledSymbol><PrimitiveLabel><Character>x</Character></PrimitiveLabel></LabeledSymbol>
+			</push>
+		</callTransition>
+		<localTransition>
+			<from><PrimitiveLabel><String>0</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>b</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>3</String></PrimitiveLabel></to>
+		</localTransition>
+		<callTransition>
+			<from><PrimitiveLabel><String>1</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>1</String></PrimitiveLabel></to>
+			<push>
+				<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+			</push>
+		</callTransition>
+		<localTransition>
+			<from><PrimitiveLabel><String>1</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>b</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>2</String></PrimitiveLabel></to>
+		</localTransition>
+		<returnTransition>
+			<from><PrimitiveLabel><String>2</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+				<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+			</pop>
+			<to><PrimitiveLabel><String>2</String></PrimitiveLabel></to>
+		</returnTransition>
+		<returnTransition>
+			<from><PrimitiveLabel><String>2</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+				<LabeledSymbol><PrimitiveLabel><Character>x</Character></PrimitiveLabel></LabeledSymbol>
+			</pop>
+			<to><PrimitiveLabel><String>3</String></PrimitiveLabel></to>
+		</returnTransition>
+		<localTransition>
+			<from><PrimitiveLabel><String>2</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>b</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>ERR</String></PrimitiveLabel></to>
+		</localTransition>
+		<localTransition>
+			<from><PrimitiveLabel><String>3</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>ERR</String></PrimitiveLabel></to>
+		</localTransition>
+		<localTransition>
+			<from><PrimitiveLabel><String>3</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>b</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>ERR</String></PrimitiveLabel></to>
+		</localTransition>
+		<localTransition>
+			<from><PrimitiveLabel><String>ERR</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>ERR</String></PrimitiveLabel></to>
+		</localTransition>
+		<localTransition>
+			<from><PrimitiveLabel><String>ERR</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>b</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>ERR</String></PrimitiveLabel></to>
+		</localTransition>
+	</transitions>
+</RealTimeHeightDeterministicNPDA>
diff --git a/examples2/automaton/RHDPDA3.xml b/examples2/automaton/RHDPDA3.xml
new file mode 100644
index 0000000000..da6fec6293
--- /dev/null
+++ b/examples2/automaton/RHDPDA3.xml
@@ -0,0 +1,56 @@
+<RealTimeHeightDeterministicNPDA>
+	<states>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+		<PrimitiveLabel><String>1</String></PrimitiveLabel>
+	</states>
+	<inputAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+	</inputAlphabet>
+	<stackAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>_</Character></PrimitiveLabel></LabeledSymbol>
+	</stackAlphabet>
+	<initialStates>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+	</initialStates>
+	<bottomOfTheStackSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>_</Character></PrimitiveLabel></LabeledSymbol>
+	</bottomOfTheStackSymbol>
+	<finalStates>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+	</finalStates>
+	<transitions>
+		<callTransition>
+			<from><PrimitiveLabel><String>0</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>1</String></PrimitiveLabel></to>
+			<push>
+				<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+			</push>
+		</callTransition>
+		<callTransition>
+			<from><PrimitiveLabel><String>0</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>0</String></PrimitiveLabel></to>
+			<push>
+				<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+			</push>
+		</callTransition>
+		<returnTransition>
+			<from><PrimitiveLabel><String>1</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+				<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+			</pop>
+			<to><PrimitiveLabel><String>0</String></PrimitiveLabel></to>
+		</returnTransition>
+		<returnTransition>
+			<from><PrimitiveLabel><String>1</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+				<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+			</pop>
+			<to><PrimitiveLabel><String>1</String></PrimitiveLabel></to>
+		</returnTransition>
+	</transitions>
+</RealTimeHeightDeterministicNPDA>
diff --git a/examples2/automaton/RHDPDA4.xml b/examples2/automaton/RHDPDA4.xml
new file mode 100644
index 0000000000..f8a7848437
--- /dev/null
+++ b/examples2/automaton/RHDPDA4.xml
@@ -0,0 +1,40 @@
+<RealTimeHeightDeterministicNPDA>
+	<states>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+		<PrimitiveLabel><String>1</String></PrimitiveLabel>
+	</states>
+	<inputAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+	</inputAlphabet>
+	<stackAlphabet>
+		<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>_</Character></PrimitiveLabel></LabeledSymbol>
+	</stackAlphabet>
+	<initialStates>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+	</initialStates>
+	<bottomOfTheStackSymbol>
+		<LabeledSymbol><PrimitiveLabel><Character>_</Character></PrimitiveLabel></LabeledSymbol>
+	</bottomOfTheStackSymbol>
+	<finalStates>
+		<PrimitiveLabel><String>0</String></PrimitiveLabel>
+	</finalStates>
+	<transitions>
+		<callTransition>
+			<from><PrimitiveLabel><String>0</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<to><PrimitiveLabel><String>1</String></PrimitiveLabel></to>
+			<push>
+				<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+			</push>
+		</callTransition>
+		<returnTransition>
+			<from><PrimitiveLabel><String>1</String></PrimitiveLabel></from>
+			<input><LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol></input>
+			<pop>
+				<LabeledSymbol><PrimitiveLabel><Character>a</Character></PrimitiveLabel></LabeledSymbol>
+			</pop>
+			<to><PrimitiveLabel><String>0</String></PrimitiveLabel></to>
+		</returnTransition>
+	</transitions>
+</RealTimeHeightDeterministicNPDA>
-- 
GitLab