From a5decc19661ca37aadc53b74353351538fe54e34 Mon Sep 17 00:00:00 2001
From: Jan Travnicek <Jan.Travnicek@fit.cvut.cz>
Date: Sun, 5 Oct 2014 09:35:52 +0200
Subject: [PATCH] RealTimeHeightDeterministicDPDA VisiblyPushdownDPDA

---
 aconvert2/src/DotConverter.cpp                | 261 +++++++++++
 aconvert2/src/DotConverter.h                  |   6 +
 aconvert2/src/GasTexConverter.cpp             | 231 ++++++++++
 aconvert2/src/GasTexConverter.h               |   6 +
 alib2algo/src/automaton/EpsilonClosure.cpp    |   8 +
 alib2algo/src/automaton/EpsilonClosure.h      |   2 +
 .../src/automaton/FSMSingleInitialState.cpp   |   8 +
 .../src/automaton/FSMSingleInitialState.h     |   2 +
 alib2algo/src/automaton/FSMTotal.cpp          |   8 +
 alib2algo/src/automaton/FSMTotal.h            |   2 +
 alib2algo/src/automaton/PDAToRHPDA.cpp        |  88 +++-
 alib2algo/src/automaton/PDAToRHPDA.h          |   4 +
 alib2algo/src/automaton/RHPDAToPDA.cpp        | 131 ++++++
 alib2algo/src/automaton/RHPDAToPDA.h          |   4 +
 alib2algo/src/conversions/fa2re/Algebraic.cpp |   8 +
 alib2algo/src/conversions/fa2re/Algebraic.h   |   2 +
 .../fa2re/formal/StateEliminationFormal.cpp   |  10 +
 .../fa2re/formal/StateEliminationFormal.h     |   2 +
 .../unbounded/StateEliminationUnbounded.cpp   |  10 +
 .../unbounded/StateEliminationUnbounded.h     |   2 +
 .../fa2rg/fa2lrg/FAtoLRGConverter.cpp         |   8 +
 .../fa2rg/fa2lrg/FAtoLRGConverter.h           |   2 +
 .../fa2rg/fa2rrg/FAtoRRGConverter.cpp         |   8 +
 .../fa2rg/fa2rrg/FAtoRRGConverter.h           |   2 +
 .../src/determinize/nfa/NFADeterminizer.cpp   |   8 +
 .../src/determinize/nfa/NFADeterminizer.h     |   2 +
 .../src/epsilon/fsm/FSMEpsilonRemover.cpp     |   8 +
 alib2algo/src/epsilon/fsm/FSMEpsilonRemover.h |   2 +
 alib2algo/src/minimize/dfa/MinimizeDFA.cpp    |   8 +
 alib2algo/src/minimize/dfa/MinimizeDFA.h      |   2 +
 alib2data/src/Api.cpp                         |  24 +
 alib2data/src/Api.hpp                         |  14 +
 alib2data/src/automaton/AutomatonBase.h       |   2 +-
 alib2data/src/automaton/AutomatonFeatures.h   |   2 +
 .../src/automaton/AutomatonFromXMLParser.cpp  | 160 ++++++-
 .../src/automaton/AutomatonFromXMLParser.h    |   7 +
 .../src/automaton/AutomatonToXMLComposer.cpp  | 102 ++++-
 .../src/automaton/AutomatonToXMLComposer.h    |   7 +
 .../FSM/FiniteAutomatonToStringComposer.cpp   |   8 +
 .../FSM/FiniteAutomatonToStringComposer.h     |   2 +
 .../PDA/RealTimeHeightDeterministicDPDA.cpp   | 409 ++++++++++++++++++
 .../PDA/RealTimeHeightDeterministicDPDA.h     | 139 ++++++
 .../src/automaton/PDA/VisiblyPushdownDPDA.cpp | 309 +++++++++++++
 .../src/automaton/PDA/VisiblyPushdownDPDA.h   | 125 ++++++
 alib2data/src/automaton/common/State.cpp      |   4 +
 alib2data/src/automaton/common/State.h        |   2 +
 alib2data/src/object/ObjectBase.h             |   6 +-
 alib2data/src/std/variant.hpp                 |  11 +
 astat2/src/AutomataStat.cpp                   |   8 +
 astat2/src/AutomataStat.h                     |   2 +
 50 files changed, 2162 insertions(+), 26 deletions(-)
 create mode 100644 alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.cpp
 create mode 100644 alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.h
 create mode 100644 alib2data/src/automaton/PDA/VisiblyPushdownDPDA.cpp
 create mode 100644 alib2data/src/automaton/PDA/VisiblyPushdownDPDA.h

diff --git a/aconvert2/src/DotConverter.cpp b/aconvert2/src/DotConverter.cpp
index 0b0d3d5901..687c9cfeb1 100644
--- a/aconvert2/src/DotConverter.cpp
+++ b/aconvert2/src/DotConverter.cpp
@@ -16,7 +16,9 @@
 #include <automaton/PDA/NPDA.h>
 #include <automaton/PDA/SinglePopNPDA.h>
 #include <automaton/PDA/InputDrivenNPDA.h>
+#include <automaton/PDA/VisiblyPushdownDPDA.h>
 #include <automaton/PDA/VisiblyPushdownNPDA.h>
+#include <automaton/PDA/RealTimeHeightDeterministicDPDA.h>
 #include <automaton/PDA/RealTimeHeightDeterministicNPDA.h>
 #include <automaton/PDA/DPDA.h>
 #include <automaton/PDA/SinglePopDPDA.h>
@@ -318,6 +320,39 @@ void DotConverter::convert(const automaton::InputDrivenNPDA& a, std::ostream& ou
 	out << "}";
 }
 
+void DotConverter::convert(const automaton::VisiblyPushdownDPDA& a, std::ostream& out) {
+	label::LabelToStringComposer composer;
+
+	out << "digraph automaton {\n";
+	out << "rankdir=LR;\n";
+	int cnt = 1;
+
+	//Map states to indices
+	std::map<automaton::State, int> states;
+	for (const automaton::State& state : a.getStates()) {
+		states.insert(std::make_pair(state, cnt++));
+	}
+
+	//Print final states
+	for (const automaton::State& state : a.getFinalStates()) {
+		out << "node [shape = doublecircle, label=\"" << composer.compose(state.getName()) << "\"]; " << states.find(state)->second << ";\n";
+	}
+
+	//Print nonfinal states
+	for (const auto& state : states) {
+		if (!a.getFinalStates().count(state.first)) {
+			out << "node [shape = circle, label=\"" << composer.compose(state.first.getName()) << "\" ]; " << state.second << ";\n";
+		}
+	}
+
+	//Mark initial states
+	out << "node [shape = plaintext, label=\"start\"]; 0; \n";
+	out << "0 -> " << a.getInitialState() << ";\n";
+
+	transitions(a, states, out);
+	out << "}";
+}
+
 void DotConverter::convert(const automaton::VisiblyPushdownNPDA& a, std::ostream& out) {
 	label::LabelToStringComposer composer;
 
@@ -353,6 +388,39 @@ void DotConverter::convert(const automaton::VisiblyPushdownNPDA& a, std::ostream
 	out << "}";
 }
 
+void DotConverter::convert(const automaton::RealTimeHeightDeterministicDPDA& a, std::ostream& out) {
+	label::LabelToStringComposer composer;
+
+	out << "digraph automaton {\n";
+	out << "rankdir=LR;\n";
+	int cnt = 1;
+
+	//Map states to indices
+	std::map<automaton::State, int> states;
+	for (const automaton::State& state : a.getStates()) {
+		states.insert(std::make_pair(state, cnt++));
+	}
+
+	//Print final states
+	for (const automaton::State& state : a.getFinalStates()) {
+		out << "node [shape = doublecircle, label=\"" << composer.compose(state.getName()) << "\"]; " << states.find(state)->second << ";\n";
+	}
+
+	//Print nonfinal states
+	for (const auto& state : states) {
+		if (!a.getFinalStates().count(state.first)) {
+			out << "node [shape = circle, label=\"" << composer.compose(state.first.getName()) << "\" ]; " << state.second << ";\n";
+		}
+	}
+
+	//Mark initial states
+	out << "node [shape = plaintext, label=\"start\"]; 0; \n";
+	out << "0 -> " << a.getInitialState() << ";\n";
+
+	transitions(a, states, out);
+	out << "}";
+}
+
 void DotConverter::convert(const automaton::RealTimeHeightDeterministicNPDA& a, std::ostream& out) {
 	label::LabelToStringComposer composer;
 
@@ -800,6 +868,94 @@ void DotConverter::transitions(const automaton::InputDrivenNPDA& pda, const std:
 	}
 }
 
+void DotConverter::transitions(const automaton::VisiblyPushdownDPDA& pda, const std::map<automaton::State, int>& states, std::ostream& out) {
+	std::map<std::pair<int, int>, std::string> transitions;
+
+	for (const auto& transition : pda.getCallTransitions()) {
+		std::string symbol;
+
+		//input symbol
+		alphabet::SymbolToStringComposer composer;
+		symbol = composer.compose(transition.first.second);
+
+		symbol += " |";
+
+		//Pop part
+		symbol += " &epsilon;";
+		symbol += " ->";
+
+		symbol += " " + composer.compose(transition.second.second);
+
+		//Insert into map
+		std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second.first)->second);
+		std::map<std::pair<int, int>, std::string>::iterator mapit = transitions.find(key);
+
+		if (mapit == transitions.end()) {
+			transitions.insert(std::make_pair(key, symbol));
+		} else {
+			mapit->second += ", " + symbol;
+		}
+	}
+
+	for (const auto& transition : pda.getReturnTransitions()) {
+		std::string symbol;
+
+		//input symbol
+		alphabet::SymbolToStringComposer composer;
+		symbol = composer.compose(std::get<1>(transition.first));
+
+		symbol += " |";
+
+		//Pop part
+		symbol += " " + composer.compose(std::get<2>(transition.first));
+		symbol += " ->";
+
+		symbol += " &epsilon;";
+
+		//Insert into map
+		std::pair<int, int> key(states.find(std::get<0>(transition.first))->second, states.find(transition.second)->second);
+		std::map<std::pair<int, int>, std::string>::iterator mapit = transitions.find(key);
+
+		if (mapit == transitions.end()) {
+			transitions.insert(std::make_pair(key, symbol));
+		} else {
+			mapit->second += ", " + symbol;
+		}
+	}
+
+	for (const auto& transition : pda.getLocalTransitions()) {
+		std::string symbol;
+
+		//input symbol
+		alphabet::SymbolToStringComposer composer;
+		symbol = composer.compose(transition.first.second);
+
+		symbol += " |";
+
+		//Pop part
+		symbol += " &epsilon;";
+		symbol += " ->";
+
+		symbol += " &epsilon;";
+
+		//Insert into map
+		std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second)->second);
+		std::map<std::pair<int, int>, std::string>::iterator mapit = transitions.find(key);
+
+		if (mapit == transitions.end()) {
+			transitions.insert(std::make_pair(key, symbol));
+		} else {
+			mapit->second += ", " + symbol;
+		}
+	}
+
+	//print the map
+	for (const std::pair<std::pair<int, int>, std::string>& transition : transitions) {
+		out << transition.first.first << " -> " << transition.first.second;
+		out << "[label=\"" << transition.second << "\"]\n";
+	}
+}
+
 void DotConverter::transitions(const automaton::VisiblyPushdownNPDA& pda, const std::map<automaton::State, int>& states, std::ostream& out) {
 	std::map<std::pair<int, int>, std::string> transitions;
 
@@ -901,6 +1057,103 @@ void DotConverter::transitions(const automaton::VisiblyPushdownNPDA& pda, const
 	}
 }
 
+void DotConverter::transitions(const automaton::RealTimeHeightDeterministicDPDA& pda, const std::map<automaton::State, int>& states, std::ostream& out) {
+	std::map<std::pair<int, int>, std::string> transitions;
+
+	for (const auto& transition : pda.getCallTransitions()) {
+		std::string symbol;
+
+		//input symbol
+		alphabet::SymbolToStringComposer composer;
+		if(transition.first.second.is<string::Epsilon>())
+			symbol = "&epsilon";
+		else
+			symbol = composer.compose(transition.first.second.get<alphabet::Symbol>());
+
+		symbol += " |";
+
+		//Pop part
+		symbol += " &epsilon;";
+		symbol += " ->";
+
+		symbol += " " + composer.compose(transition.second.second);
+
+		//Insert into map
+		std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second.first)->second);
+		std::map<std::pair<int, int>, std::string>::iterator mapit = transitions.find(key);
+
+		if (mapit == transitions.end()) {
+			transitions.insert(std::make_pair(key, symbol));
+		} else {
+			mapit->second += ", " + symbol;
+		}
+	}
+
+	for (const auto& transition : pda.getReturnTransitions()) {
+		std::string symbol;
+
+		//input symbol
+		alphabet::SymbolToStringComposer composer;
+		if(std::get<1>(transition.first).is<string::Epsilon>())
+			symbol = "&epsilon";
+		else
+			symbol = composer.compose(std::get<1>(transition.first).get<alphabet::Symbol>());
+
+		symbol += " |";
+
+		//Pop part
+		symbol += " " + composer.compose(std::get<2>(transition.first));
+		symbol += " ->";
+
+		symbol += " &epsilon;";
+
+		//Insert into map
+		std::pair<int, int> key(states.find(std::get<0>(transition.first))->second, states.find(transition.second)->second);
+		std::map<std::pair<int, int>, std::string>::iterator mapit = transitions.find(key);
+
+		if (mapit == transitions.end()) {
+			transitions.insert(std::make_pair(key, symbol));
+		} else {
+			mapit->second += ", " + symbol;
+		}
+	}
+
+	for (const auto& transition : pda.getLocalTransitions()) {
+		std::string symbol;
+
+		//input symbol
+		alphabet::SymbolToStringComposer composer;
+		if(transition.first.second.is<string::Epsilon>())
+			symbol = "&epsilon";
+		else
+			symbol = composer.compose(transition.first.second.get<alphabet::Symbol>());
+
+		symbol += " |";
+
+		//Pop part
+		symbol += " &epsilon;";
+		symbol += " ->";
+
+		symbol += " &epsilon;";
+
+		//Insert into map
+		std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second)->second);
+		std::map<std::pair<int, int>, std::string>::iterator mapit = transitions.find(key);
+
+		if (mapit == transitions.end()) {
+			transitions.insert(std::make_pair(key, symbol));
+		} else {
+			mapit->second += ", " + symbol;
+		}
+	}
+
+	//print the map
+	for (const std::pair<std::pair<int, int>, std::string>& transition : transitions) {
+		out << transition.first.first << " -> " << transition.first.second;
+		out << "[label=\"" << transition.second << "\"]\n";
+	}
+}
+
 void DotConverter::transitions(const automaton::RealTimeHeightDeterministicNPDA& pda, const std::map<automaton::State, int>& states, std::ostream& out) {
 	std::map<std::pair<int, int>, std::string> transitions;
 
@@ -1211,10 +1464,18 @@ void DotConverter::Visit(void* data, const automaton::InputDrivenNPDA& automaton
 	DotConverter::convert(automaton, *((std::ostream*) data));
 }
 
+void DotConverter::Visit(void* data, const automaton::VisiblyPushdownDPDA& automaton) const {
+	DotConverter::convert(automaton, *((std::ostream*) data));
+}
+
 void DotConverter::Visit(void* data, const automaton::VisiblyPushdownNPDA& automaton) const {
 	DotConverter::convert(automaton, *((std::ostream*) data));
 }
 
+void DotConverter::Visit(void* data, const automaton::RealTimeHeightDeterministicDPDA& automaton) const {
+	DotConverter::convert(automaton, *((std::ostream*) data));
+}
+
 void DotConverter::Visit(void* data, const automaton::RealTimeHeightDeterministicNPDA& automaton) const {
 	DotConverter::convert(automaton, *((std::ostream*) data));
 }
diff --git a/aconvert2/src/DotConverter.h b/aconvert2/src/DotConverter.h
index 98bdf797c0..cd8c69a095 100644
--- a/aconvert2/src/DotConverter.h
+++ b/aconvert2/src/DotConverter.h
@@ -25,7 +25,9 @@ class DotConverter : public automaton::VisitableAutomatonBase::const_visitor_typ
 	void Visit(void*, const automaton::DPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
 	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const automaton::NPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
@@ -40,7 +42,9 @@ class DotConverter : public automaton::VisitableAutomatonBase::const_visitor_typ
 	static void transitions(const automaton::DPDA& pda, const std::map<automaton::State, int>& states, std::ostream& out);
 	static void transitions(const automaton::SinglePopDPDA& tm, const std::map<automaton::State, int>& states, std::ostream& out);
 	static void transitions(const automaton::InputDrivenNPDA& pda, const std::map<automaton::State, int>& states, std::ostream& out);
+	static void transitions(const automaton::VisiblyPushdownDPDA& tm, const std::map<automaton::State, int>& states, std::ostream& out);
 	static void transitions(const automaton::VisiblyPushdownNPDA& tm, const std::map<automaton::State, int>& states, std::ostream& out);
+	static void transitions(const automaton::RealTimeHeightDeterministicDPDA& tm, const std::map<automaton::State, int>& states, std::ostream& out);
 	static void transitions(const automaton::RealTimeHeightDeterministicNPDA& tm, const std::map<automaton::State, int>& states, std::ostream& out);
 	static void transitions(const automaton::NPDA& pda, const std::map<automaton::State, int>& states, std::ostream& out);
 	static void transitions(const automaton::SinglePopNPDA& tm, const std::map<automaton::State, int>& states, std::ostream& out);
@@ -59,7 +63,9 @@ public:
 	static void convert(const automaton::DPDA& a, std::ostream& out);
 	static void convert(const automaton::SinglePopDPDA& a, std::ostream& out);
 	static void convert(const automaton::InputDrivenNPDA& a, std::ostream& out);
+	static void convert(const automaton::VisiblyPushdownDPDA& a, std::ostream& out);
 	static void convert(const automaton::VisiblyPushdownNPDA& a, std::ostream& out);
+	static void convert(const automaton::RealTimeHeightDeterministicDPDA& a, std::ostream& out);
 	static void convert(const automaton::RealTimeHeightDeterministicNPDA& a, std::ostream& out);
 	static void convert(const automaton::NPDA& a, std::ostream& out);
 	static void convert(const automaton::SinglePopNPDA& a, std::ostream& out);
diff --git a/aconvert2/src/GasTexConverter.cpp b/aconvert2/src/GasTexConverter.cpp
index bca98470c6..6a3592f509 100644
--- a/aconvert2/src/GasTexConverter.cpp
+++ b/aconvert2/src/GasTexConverter.cpp
@@ -15,7 +15,9 @@
 #include <automaton/PDA/DPDA.h>
 #include <automaton/PDA/SinglePopDPDA.h>
 #include <automaton/PDA/InputDrivenNPDA.h>
+#include <automaton/PDA/VisiblyPushdownDPDA.h>
 #include <automaton/PDA/VisiblyPushdownNPDA.h>
+#include <automaton/PDA/RealTimeHeightDeterministicDPDA.h>
 #include <automaton/PDA/RealTimeHeightDeterministicNPDA.h>
 #include <automaton/PDA/NPDA.h>
 #include <automaton/PDA/SinglePopNPDA.h>
@@ -350,6 +352,45 @@ void GasTexConverter::convert(const automaton::InputDrivenNPDA& a, std::ostream&
 	out << "\\end{picture}\n";
 }
 
+void GasTexConverter::convert(const automaton::VisiblyPushdownDPDA& a, std::ostream& out) {
+	out << "\\begin{center}\n";
+	out << "\\begin{picture}(,)(,)\n";
+
+	for (auto& state : a.getStates()) {
+		bool initial = false;
+		bool final = false;
+
+		if(a.getInitialState() == state){
+			initial = true;
+		}
+		if(a.getFinalStates().count(state)){
+			final = true;
+		}
+
+		if(initial || final) {
+			out << "\\node[Nmarks=";
+			if(initial){
+				out << "i";
+			}
+			if(final){
+				out << "r";
+			}
+			out<<"](";
+		} else {
+			out <<"\\node(";
+		}
+
+		out << state.getName();
+		out << ")(,){";
+		out << state.getName();
+		out << "}\n";
+	}
+
+	transitions(a, out);
+	out << "\\end{center}\n";
+	out << "\\end{picture}\n";
+}
+
 void GasTexConverter::convert(const automaton::VisiblyPushdownNPDA& a, std::ostream& out) {
 	out << "\\begin{center}\n";
 	out << "\\begin{picture}(,)(,)\n";
@@ -389,6 +430,45 @@ void GasTexConverter::convert(const automaton::VisiblyPushdownNPDA& a, std::ostr
 	out << "\\end{picture}\n";
 }
 
+void GasTexConverter::convert(const automaton::RealTimeHeightDeterministicDPDA& a, std::ostream& out) {
+	out << "\\begin{center}\n";
+	out << "\\begin{picture}(,)(,)\n";
+
+	for (auto& state : a.getStates()) {
+		bool initial = false;
+		bool final = false;
+
+		if(a.getInitialState() == state){
+			initial = true;
+		}
+		if(a.getFinalStates().count(state)){
+			final = true;
+		}
+
+		if(initial || final) {
+			out << "\\node[Nmarks=";
+			if(initial){
+				out << "i";
+			}
+			if(final){
+				out << "r";
+			}
+			out<<"](";
+		} else {
+			out <<"\\node(";
+		}
+
+		out << state.getName();
+		out << ")(,){";
+		out << state.getName();
+		out << "}\n";
+	}
+
+	transitions(a, out);
+	out << "\\end{center}\n";
+	out << "\\end{picture}\n";
+}
+
 void GasTexConverter::convert(const automaton::RealTimeHeightDeterministicNPDA& a, std::ostream& out) {
 	out << "\\begin{center}\n";
 	out << "\\begin{picture}(,)(,)\n";
@@ -782,6 +862,73 @@ void GasTexConverter::transitions(const automaton::InputDrivenNPDA& pda, std::os
 	printTransitionMap(transitionMap, out);
 }
 
+void GasTexConverter::transitions(const automaton::VisiblyPushdownDPDA& pda, std::ostream& out) {
+	std::map<std::pair<std::string, std::string>, std::string> transitionMap;
+
+	alphabet::SymbolToStringComposer composer;
+	for (const auto& transition : pda.getCallTransitions()) {
+		std::pair<std::string, std::string> key((std::string) transition.first.first.getName(), (std::string) transition.second.first.getName());
+		auto mapIterator = transitionMap.find(key);
+
+		std::string symbol;
+		symbol = composer.compose(transition.first.second);
+
+		symbol += "|";
+
+		symbol += "$\\varepsilon;$";
+		symbol += "\\rarrow";
+		symbol += composer.compose(transition.second.second);
+
+		if (mapIterator == transitionMap.end()) {
+			transitionMap.insert(std::make_pair(key, symbol));
+		} else {
+			mapIterator->second += "; " + symbol;
+		}
+	}
+
+	for (const auto& transition : pda.getReturnTransitions()) {
+		std::pair<std::string, std::string> key((std::string) std::get<0>(transition.first).getName(), (std::string) transition.second.getName());
+		auto mapIterator = transitionMap.find(key);
+
+		std::string symbol;
+		symbol = composer.compose(std::get<1>(transition.first));
+
+		symbol += "|";
+
+		symbol += composer.compose(std::get<2>(transition.first));
+		symbol += "\\rarrow";
+		symbol += "$\\varepsilon;$";
+
+		if (mapIterator == transitionMap.end()) {
+			transitionMap.insert(std::make_pair(key, symbol));
+		} else {
+			mapIterator->second += "; " + symbol;
+		}
+	}
+
+	for (const auto& transition : pda.getLocalTransitions()) {
+		std::pair<std::string, std::string> key((std::string) transition.first.first.getName(), (std::string) transition.second.getName());
+		auto mapIterator = transitionMap.find(key);
+
+		std::string symbol;
+		symbol = composer.compose(transition.first.second);
+
+		symbol += "|";
+
+		symbol += "$\\varepsilon;$";
+		symbol += "\\rarrow";
+		symbol += "$\\varepsilon;$";
+
+		if (mapIterator == transitionMap.end()) {
+			transitionMap.insert(std::make_pair(key, symbol));
+		} else {
+			mapIterator->second += "; " + symbol;
+		}
+	}
+
+	printTransitionMap(transitionMap, out);
+}
+
 void GasTexConverter::transitions(const automaton::VisiblyPushdownNPDA& pda, std::ostream& out) {
 	std::map<std::pair<std::string, std::string>, std::string> transitionMap;
 
@@ -855,6 +1002,82 @@ void GasTexConverter::transitions(const automaton::VisiblyPushdownNPDA& pda, std
 	printTransitionMap(transitionMap, out);
 }
 
+void GasTexConverter::transitions(const automaton::RealTimeHeightDeterministicDPDA& pda, std::ostream& out) {
+	std::map<std::pair<std::string, std::string>, std::string> transitionMap;
+
+	alphabet::SymbolToStringComposer composer;
+	for (const auto& transition : pda.getCallTransitions()) {
+		std::pair<std::string, std::string> key((std::string) transition.first.first.getName(), (std::string) transition.second.first.getName());
+		auto mapIterator = transitionMap.find(key);
+
+		std::string symbol;
+		if(transition.first.second.is<string::Epsilon>())
+			symbol = "$\\varepsilon;$";
+		else
+			symbol = composer.compose(transition.first.second.get<alphabet::Symbol>());
+
+		symbol += "|";
+
+		symbol += "$\\varepsilon;$";
+		symbol += "\\rarrow";
+		symbol += composer.compose(transition.second.second);
+
+		if (mapIterator == transitionMap.end()) {
+			transitionMap.insert(std::make_pair(key, symbol));
+		} else {
+			mapIterator->second += "; " + symbol;
+		}
+	}
+
+	for (const auto& transition : pda.getReturnTransitions()) {
+		std::pair<std::string, std::string> key((std::string) std::get<0>(transition.first).getName(), (std::string) transition.second.getName());
+		auto mapIterator = transitionMap.find(key);
+
+		std::string symbol;
+		if(std::get<1>(transition.first).is<string::Epsilon>())
+			symbol = "$\\varepsilon;$";
+		else
+			symbol = composer.compose(std::get<1>(transition.first).get<alphabet::Symbol>());
+
+		symbol += "|";
+
+		symbol += composer.compose(std::get<2>(transition.first));
+		symbol += "\\rarrow";
+		symbol += "$\\varepsilon;$";
+
+		if (mapIterator == transitionMap.end()) {
+			transitionMap.insert(std::make_pair(key, symbol));
+		} else {
+			mapIterator->second += "; " + symbol;
+		}
+	}
+
+	for (const auto& transition : pda.getLocalTransitions()) {
+		std::pair<std::string, std::string> key((std::string) transition.first.first.getName(), (std::string) transition.second.getName());
+		auto mapIterator = transitionMap.find(key);
+
+		std::string symbol;
+		if(transition.first.second.is<string::Epsilon>())
+			symbol = "$\\varepsilon;$";
+		else
+			symbol = composer.compose(transition.first.second.get<alphabet::Symbol>());
+
+		symbol += "|";
+
+		symbol += "$\\varepsilon;$";
+		symbol += "\\rarrow";
+		symbol += "$\\varepsilon;$";
+
+		if (mapIterator == transitionMap.end()) {
+			transitionMap.insert(std::make_pair(key, symbol));
+		} else {
+			mapIterator->second += "; " + symbol;
+		}
+	}
+
+	printTransitionMap(transitionMap, out);
+}
+
 void GasTexConverter::transitions(const automaton::RealTimeHeightDeterministicNPDA& pda, std::ostream& out) {
 	std::map<std::pair<std::string, std::string>, std::string> transitionMap;
 
@@ -1077,10 +1300,18 @@ void GasTexConverter::Visit(void* data, const automaton::InputDrivenNPDA& automa
 	GasTexConverter::convert(automaton, *((std::ostream*) data));
 }
 
+void GasTexConverter::Visit(void* data, const automaton::VisiblyPushdownDPDA& automaton) const {
+	GasTexConverter::convert(automaton, *((std::ostream*) data));
+}
+
 void GasTexConverter::Visit(void* data, const automaton::VisiblyPushdownNPDA& automaton) const {
 	GasTexConverter::convert(automaton, *((std::ostream*) data));
 }
 
+void GasTexConverter::Visit(void* data, const automaton::RealTimeHeightDeterministicDPDA& automaton) const {
+	GasTexConverter::convert(automaton, *((std::ostream*) data));
+}
+
 void GasTexConverter::Visit(void* data, const automaton::RealTimeHeightDeterministicNPDA& automaton) const {
 	GasTexConverter::convert(automaton, *((std::ostream*) data));
 }
diff --git a/aconvert2/src/GasTexConverter.h b/aconvert2/src/GasTexConverter.h
index 31842aba6a..c02234cb02 100644
--- a/aconvert2/src/GasTexConverter.h
+++ b/aconvert2/src/GasTexConverter.h
@@ -25,7 +25,9 @@ class GasTexConverter : public automaton::VisitableAutomatonBase::const_visitor_
 	void Visit(void*, const automaton::DPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
 	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const automaton::NPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
@@ -43,7 +45,9 @@ class GasTexConverter : public automaton::VisitableAutomatonBase::const_visitor_
 	static void transitions(const automaton::DPDA& pda, std::ostream& out);
 	static void transitions(const automaton::SinglePopDPDA& tm, std::ostream& out);
 	static void transitions(const automaton::InputDrivenNPDA& pda, std::ostream& out);
+	static void transitions(const automaton::VisiblyPushdownDPDA& tm, std::ostream& out);
 	static void transitions(const automaton::VisiblyPushdownNPDA& tm, std::ostream& out);
+	static void transitions(const automaton::RealTimeHeightDeterministicDPDA& tm, std::ostream& out);
 	static void transitions(const automaton::RealTimeHeightDeterministicNPDA& tm, std::ostream& out);
 	static void transitions(const automaton::NPDA& pda, std::ostream& out);
 	static void transitions(const automaton::SinglePopNPDA& tm, std::ostream& out);
@@ -62,7 +66,9 @@ public:
 	static void convert(const automaton::DPDA& a, std::ostream& out);
 	static void convert(const automaton::SinglePopDPDA& a, std::ostream& out);
 	static void convert(const automaton::InputDrivenNPDA& a, std::ostream& out);
+	static void convert(const automaton::VisiblyPushdownDPDA& a, std::ostream& out);
 	static void convert(const automaton::VisiblyPushdownNPDA& a, std::ostream& out);
+	static void convert(const automaton::RealTimeHeightDeterministicDPDA& a, std::ostream& out);
 	static void convert(const automaton::RealTimeHeightDeterministicNPDA& a, std::ostream& out);
 	static void convert(const automaton::NPDA& a, std::ostream& out);
 	static void convert(const automaton::SinglePopNPDA& a, std::ostream& out);
diff --git a/alib2algo/src/automaton/EpsilonClosure.cpp b/alib2algo/src/automaton/EpsilonClosure.cpp
index 39ad0e4221..0130311bba 100644
--- a/alib2algo/src/automaton/EpsilonClosure.cpp
+++ b/alib2algo/src/automaton/EpsilonClosure.cpp
@@ -169,10 +169,18 @@ void EpsilonClosure::Visit(void*, const InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void EpsilonClosure::Visit(void*, const VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void EpsilonClosure::Visit(void*, const VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void EpsilonClosure::Visit(void*, const RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void EpsilonClosure::Visit(void*, const RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/alib2algo/src/automaton/EpsilonClosure.h b/alib2algo/src/automaton/EpsilonClosure.h
index bc4a867a2b..7d64d5399e 100644
--- a/alib2algo/src/automaton/EpsilonClosure.h
+++ b/alib2algo/src/automaton/EpsilonClosure.h
@@ -40,7 +40,9 @@ private:
 	void Visit(void*, const DPDA& automaton) const;
 	void Visit(void*, const SinglePopDPDA& automaton) const;
 	void Visit(void*, const InputDrivenNPDA& automaton) const;
+	void Visit(void*, const VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const NPDA& automaton) const;
 	void Visit(void*, const SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/automaton/FSMSingleInitialState.cpp b/alib2algo/src/automaton/FSMSingleInitialState.cpp
index 286bd05836..4f615c4d4c 100644
--- a/alib2algo/src/automaton/FSMSingleInitialState.cpp
+++ b/alib2algo/src/automaton/FSMSingleInitialState.cpp
@@ -104,10 +104,18 @@ void FSMSingleInitialState::Visit(void*, const InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void FSMSingleInitialState::Visit(void*, const VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void FSMSingleInitialState::Visit(void*, const VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void FSMSingleInitialState::Visit(void*, const RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void FSMSingleInitialState::Visit(void*, const RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/alib2algo/src/automaton/FSMSingleInitialState.h b/alib2algo/src/automaton/FSMSingleInitialState.h
index a1cac7f05d..dca46392a4 100644
--- a/alib2algo/src/automaton/FSMSingleInitialState.h
+++ b/alib2algo/src/automaton/FSMSingleInitialState.h
@@ -42,7 +42,9 @@ private:
 	void Visit(void*, const DPDA& automaton) const;
 	void Visit(void*, const SinglePopDPDA& automaton) const;
 	void Visit(void*, const InputDrivenNPDA& automaton) const;
+	void Visit(void*, const VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const NPDA& automaton) const;
 	void Visit(void*, const SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/automaton/FSMTotal.cpp b/alib2algo/src/automaton/FSMTotal.cpp
index 6b0c83f1a6..b22570c26e 100644
--- a/alib2algo/src/automaton/FSMTotal.cpp
+++ b/alib2algo/src/automaton/FSMTotal.cpp
@@ -96,10 +96,18 @@ void FSMTotal::Visit(void*, const InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void FSMTotal::Visit(void*, const VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void FSMTotal::Visit(void*, const VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void FSMTotal::Visit(void*, const RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void FSMTotal::Visit(void*, const RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/alib2algo/src/automaton/FSMTotal.h b/alib2algo/src/automaton/FSMTotal.h
index 950ec9f659..ef0b7a1ee5 100644
--- a/alib2algo/src/automaton/FSMTotal.h
+++ b/alib2algo/src/automaton/FSMTotal.h
@@ -41,7 +41,9 @@ private:
 	void Visit(void*, const DPDA& automaton) const;
 	void Visit(void*, const SinglePopDPDA& automaton) const;
 	void Visit(void*, const InputDrivenNPDA& automaton) const;
+	void Visit(void*, const VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const NPDA& automaton) const;
 	void Visit(void*, const SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/automaton/PDAToRHPDA.cpp b/alib2algo/src/automaton/PDAToRHPDA.cpp
index ed76fbebf0..983792c491 100644
--- a/alib2algo/src/automaton/PDAToRHPDA.cpp
+++ b/alib2algo/src/automaton/PDAToRHPDA.cpp
@@ -8,7 +8,9 @@
 #include "PDAToRHPDA.h"
 
 #include <exception/AlibException.h>
+#include <automaton/PDA/RealTimeHeightDeterministicDPDA.h>
 #include <automaton/PDA/RealTimeHeightDeterministicNPDA.h>
+#include <automaton/PDA/DPDA.h>
 #include <automaton/PDA/NPDA.h>
 
 #include <alphabet/BottomOfTheStackSymbol.h>
@@ -19,10 +21,82 @@
 
 namespace automaton {
 
+automaton::RealTimeHeightDeterministicDPDA PDAToRHPDA::convert( const automaton::RealTimeHeightDeterministicDPDA & pda ) {
+	return pda;
+}
+
 automaton::RealTimeHeightDeterministicNPDA PDAToRHPDA::convert( const automaton::RealTimeHeightDeterministicNPDA & pda ) {
 	return pda;
 }
 
+automaton::RealTimeHeightDeterministicDPDA PDAToRHPDA::convert( const automaton::DPDA & pda ) {
+/*	RealTimeHeightDeterministicNPDA res(alphabet::Symbol { alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK } );
+
+	res.setInputSymbols(pda.getInputAlphabet());
+	res.setStates(pda.getStates());
+	res.setFinalStates(pda.getFinalStates());
+	std::set<alphabet::Symbol> stackSymbols = pda.getStackAlphabet();
+	stackSymbols.insert( alphabet::Symbol { alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK } );
+	res.setStackSymbols(stackSymbols);
+
+	automaton::State q0 = automaton::createUniqueState(automaton::State("q0"), res.getStates());
+	res.addState(q0);
+	res.addInitialState(q0);
+
+	for(const automaton::State& state : pda.getInitialStates())
+		for(const alphabet::Symbol& symbol : pda.getInitialSymbols())
+			res.addCallTransition(q0, state, symbol);
+
+	std::string us("us");
+	int i = 0;
+	for(const auto& transition : pda.getTransitions()) {
+		for(const auto& to : transition.second) {
+			if(std::get<2>(transition.first).size() == 0 && to.second.size() == 0)
+				res.addLocalTransition(std::get<0>(transition.first), std::get<1>(transition.first), to.first);
+			else if(std::get<2>(transition.first).size() == 1 && to.second.size() == 0)
+				res.addReturnTransition(std::get<0>(transition.first), std::get<1>(transition.first), std::get<2>(transition.first)[0], to.first);
+			else if(std::get<2>(transition.first).size() == 0 && to.second.size() == 1)
+				res.addCallTransition(std::get<0>(transition.first), std::get<1>(transition.first), to.first, to.second[0]);
+			else {
+				int popPushIndex = 0;
+				int popPushSymbols = std::get<2>(transition.first).size() + to.second.size();
+
+				automaton::State lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(i)), res.getStates());
+				for(const alphabet::Symbol& pop : std::get<2>(transition.first)) {
+					automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : lastUS;
+					if(popPushIndex != 0) lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(++i)), res.getStates());
+					automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : lastUS;
+
+					res.addState(fromState);
+					res.addState(toState);
+
+					if(popPushIndex == 0)
+						res.addReturnTransition(fromState, std::get<1>(transition.first), pop, toState);
+					else
+						res.addReturnTransition(fromState, pop, toState);
+					popPushIndex++;
+				}
+				for(const alphabet::Symbol& push : to.second) {
+					automaton::State fromState = (popPushIndex == 0) ? std::get<0>(transition.first) : lastUS;
+					if(popPushIndex != 0) lastUS = automaton::createUniqueState(automaton::State(us + std::to_string(++i)), res.getStates());
+					automaton::State toState = (popPushIndex == popPushSymbols - 1) ? to.first : lastUS;
+
+					res.addState(fromState);
+					res.addState(toState);
+
+					if(popPushIndex == 0)
+						res.addCallTransition(fromState, std::get<1>(transition.first), toState, push);
+					else
+						res.addCallTransition(fromState, toState, push);
+					popPushIndex++;
+				}
+			}
+		}
+	}
+	
+	return res;*/
+}
+
 automaton::RealTimeHeightDeterministicNPDA PDAToRHPDA::convert( const automaton::NPDA & pda ) {
 	RealTimeHeightDeterministicNPDA res(alphabet::Symbol { alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK } );
 
@@ -123,8 +197,9 @@ void PDAToRHPDA::Visit(void*, const CompactNFA&) const {
 	throw exception::AlibException("Unsupported automaton type CompactNFA");
 }
 
-void PDAToRHPDA::Visit(void*, const DPDA&) const {
-	throw exception::AlibException("Unsupported automaton type DPDA");
+void PDAToRHPDA::Visit(void* data, const DPDA& automaton) const {
+	automaton::Automaton*& out = *((automaton::Automaton**) data);
+	out = new automaton::Automaton(this->convert(automaton));
 }
 
 void PDAToRHPDA::Visit(void*, const SinglePopDPDA&) const {
@@ -135,10 +210,19 @@ void PDAToRHPDA::Visit(void*, const InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void PDAToRHPDA::Visit(void*, const VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void PDAToRHPDA::Visit(void*, const VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void PDAToRHPDA::Visit(void* data, const RealTimeHeightDeterministicDPDA& automaton) const {
+	automaton::Automaton*& out = *((automaton::Automaton**) data);
+	out = new automaton::Automaton(this->convert(automaton));
+}
+
 void PDAToRHPDA::Visit(void* data, const RealTimeHeightDeterministicNPDA& automaton) const {
 	automaton::Automaton*& out = *((automaton::Automaton**) data);
 	out = new automaton::Automaton(this->convert(automaton));
diff --git a/alib2algo/src/automaton/PDAToRHPDA.h b/alib2algo/src/automaton/PDAToRHPDA.h
index d37faf1f33..677713a00b 100644
--- a/alib2algo/src/automaton/PDAToRHPDA.h
+++ b/alib2algo/src/automaton/PDAToRHPDA.h
@@ -19,6 +19,8 @@ namespace automaton {
 
 class PDAToRHPDA : public VisitableAutomatonBase::const_visitor_type {
 public:
+	static automaton::RealTimeHeightDeterministicDPDA convert( const automaton::RealTimeHeightDeterministicDPDA & pda);
+	static automaton::RealTimeHeightDeterministicDPDA convert( const automaton::DPDA & pda);
 	static automaton::RealTimeHeightDeterministicNPDA convert( const automaton::RealTimeHeightDeterministicNPDA & pda);
 	static automaton::RealTimeHeightDeterministicNPDA convert( const automaton::NPDA & pda);
 
@@ -36,7 +38,9 @@ private:
 	void Visit(void*, const DPDA& automaton) const;
 	void Visit(void*, const SinglePopDPDA& automaton) const;
 	void Visit(void*, const InputDrivenNPDA& automaton) const;
+	void Visit(void*, const VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const NPDA& automaton) const;
 	void Visit(void*, const SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/automaton/RHPDAToPDA.cpp b/alib2algo/src/automaton/RHPDAToPDA.cpp
index cc3924ef35..2651f43349 100644
--- a/alib2algo/src/automaton/RHPDAToPDA.cpp
+++ b/alib2algo/src/automaton/RHPDAToPDA.cpp
@@ -8,7 +8,9 @@
 #include "RHPDAToPDA.h"
 
 #include <exception/AlibException.h>
+#include <automaton/PDA/RealTimeHeightDeterministicDPDA.h>
 #include <automaton/PDA/RealTimeHeightDeterministicNPDA.h>
+#include <automaton/PDA/DPDA.h>
 #include <automaton/PDA/NPDA.h>
 
 #include <alphabet/BottomOfTheStackSymbol.h>
@@ -20,6 +22,126 @@
 
 namespace automaton {
 
+automaton::DPDA RHPDAToPDA::convert( const automaton::RealTimeHeightDeterministicDPDA & pda ) {
+/*	automaton::NPDA res;
+
+	res.setInputSymbols(pda.getInputAlphabet());
+
+	res.setStackSymbols(pda.getStackAlphabet());
+
+	std::map<std::tuple<automaton::State, alphabet::Symbol, std::vector<alphabet::Symbol>>, std::set<std::pair<automaton::State, std::vector<alphabet::Symbol>>>> readingTransitions;
+	std::map<automaton::State, std::set<std::tuple<std::vector<alphabet::Symbol>, automaton::State, std::vector<alphabet::Symbol>>>> epsilonTransitions;
+
+	for(const auto& transition : pda.getCallTransitions()) {
+		if(std::get<1>(transition.first).is<string::Epsilon>()) {
+			auto& epsT = epsilonTransitions[std::get<0>(transition.first)];
+			for(const auto& to : transition.second) {
+				if(to.second.getData() == alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK) throw exception::AlibException("Cannot convert");
+				epsT.insert(std::make_tuple(std::vector<alphabet::Symbol>{}, to.first, std::vector<alphabet::Symbol>{to.second}));
+			}
+		} else {
+			auto& readT = readingTransitions[std::make_tuple(std::get<0>(transition.first), std::get<1>(transition.first).get<alphabet::Symbol>(), std::vector<alphabet::Symbol>{})];
+			for(const auto& to : transition.second) {
+				readT.insert(std::make_pair(to.first, std::vector<alphabet::Symbol>{to.second}));
+			}
+		}
+	}
+
+	for(const auto& transition : pda.getLocalTransitions()) {
+		if(std::get<1>(transition.first).is<string::Epsilon>()) {
+			auto& epsT = epsilonTransitions[std::get<0>(transition.first)];
+			for(const auto& to : transition.second) {
+				epsT.insert(std::make_tuple(std::vector<alphabet::Symbol>{}, to, std::vector<alphabet::Symbol>{}));
+			}
+		} else {
+			auto& readT = readingTransitions[std::make_tuple(std::get<0>(transition.first), std::get<1>(transition.first).get<alphabet::Symbol>(), std::vector<alphabet::Symbol>{})];
+			for(const auto& to : transition.second) {
+				readT.insert(std::make_pair(to, std::vector<alphabet::Symbol>{}));
+			}
+		}
+	}
+
+	for(const auto& transition : pda.getReturnTransitions()) {
+		if(std::get<1>(transition.first).is<string::Epsilon>()) {
+			auto& epsT = epsilonTransitions[std::get<0>(transition.first)];
+			for(const auto& to : transition.second) {
+				if(std::get<2>(transition.first).getData() == alphabet::BottomOfTheStackSymbol::BOTTOM_OF_THE_STACK) throw exception::AlibException("Cannot convert");
+				epsT.insert(std::make_tuple(std::vector<alphabet::Symbol>{std::get<2>(transition.first)}, to, std::vector<alphabet::Symbol>{}));
+			}
+		} else {
+			auto& readT = readingTransitions[std::make_tuple(std::get<0>(transition.first), std::get<1>(transition.first).get<alphabet::Symbol>(), std::vector<alphabet::Symbol>{std::get<2>(transition.first)})];
+			for(const auto& to : transition.second) {
+				readT.insert(std::make_pair(to, std::vector<alphabet::Symbol>{}));
+			}
+		}
+	}
+
+	for(const auto& st : epsilonTransitions) {
+		if(st.second.size() != 1) throw exception::AlibException("Temporary states has more than one leaving transition");
+	}
+
+	for(const auto& st : readingTransitions) {
+		for(const auto& to : st.second) {
+			std::vector<alphabet::Symbol> pops;
+			std::vector<alphabet::Symbol> pushes;
+
+			pops.insert(pops.end(), std::get<2>(st.first).begin(), std::get<2>(st.first).end());
+			pushes.insert(pushes.end(), to.second.begin(), to.second.end());
+
+			automaton::State toState = to.first;
+			while(!epsilonTransitions[toState].empty()) {
+				const auto& epsilonT = *epsilonTransitions[toState].begin();
+
+				pops.insert(pops.end(), std::get<0>(epsilonT).begin(), std::get<0>(epsilonT).end());
+				pushes.insert(pushes.end(), std::get<2>(epsilonT).begin(), std::get<2>(epsilonT).end());
+
+				toState = std::get<1>(epsilonT);
+			}
+
+			res.addState(std::get<0>(st.first));
+			res.addState(toState);
+
+			res.addTransition(std::get<0>(st.first), std::get<1>(st.first), pops, toState, pushes);
+		}
+	}
+
+	if(pda.getInitialStates().size() != 1)
+		throw exception::AlibException("Cannot convert");
+
+	for(const automaton::State& initialState : pda.getInitialStates()) {
+		if(!epsilonTransitions[initialState].empty()) {
+			const auto& st = *epsilonTransitions[initialState].begin();
+
+			std::vector<alphabet::Symbol> pops;
+			std::vector<alphabet::Symbol> pushes;
+
+			pops.insert(pops.end(), std::get<0>(st).begin(), std::get<0>(st).end());
+			pushes.insert(pushes.end(), std::get<2>(st).begin(), std::get<2>(st).end());
+
+			automaton::State toState = std::get<1>(st);
+			while(!epsilonTransitions[toState].empty()) {
+				const auto& epsilonT = *epsilonTransitions[toState].begin();
+
+				pops.insert(pops.end(), std::get<0>(epsilonT).begin(), std::get<0>(epsilonT).end());
+				pushes.insert(pushes.end(), std::get<2>(epsilonT).begin(), std::get<2>(epsilonT).end());
+
+				toState = std::get<1>(epsilonT);
+			}
+			res.addState(toState);
+
+			if(pops.size() != 0 && pushes.size() != 1)
+				throw exception::AlibException("Cannot convert");
+
+			res.setInitialStates({toState});
+			res.setInitialSymbols({pushes[0]});
+		}
+	}
+
+	res.setFinalStates(pda.getFinalStates());
+
+	return res;*/
+}
+
 automaton::NPDA RHPDAToPDA::convert( const automaton::RealTimeHeightDeterministicNPDA & pda ) {
 	automaton::NPDA res;
 
@@ -184,10 +306,19 @@ void RHPDAToPDA::Visit(void*, const InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void RHPDAToPDA::Visit(void*, const VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void RHPDAToPDA::Visit(void*, const VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void RHPDAToPDA::Visit(void* data, const RealTimeHeightDeterministicDPDA& automaton) const {
+	automaton::Automaton*& out = *((automaton::Automaton**) data);
+	out = new automaton::Automaton(this->convert(automaton));
+}
+
 void RHPDAToPDA::Visit(void* data, const RealTimeHeightDeterministicNPDA& automaton) const {
 	automaton::Automaton*& out = *((automaton::Automaton**) data);
 	out = new automaton::Automaton(this->convert(automaton));
diff --git a/alib2algo/src/automaton/RHPDAToPDA.h b/alib2algo/src/automaton/RHPDAToPDA.h
index 2bc2ef9e42..2ad7a041f2 100644
--- a/alib2algo/src/automaton/RHPDAToPDA.h
+++ b/alib2algo/src/automaton/RHPDAToPDA.h
@@ -19,6 +19,8 @@ namespace automaton {
 
 class RHPDAToPDA : public VisitableAutomatonBase::const_visitor_type {
 public:
+	static automaton::DPDA convert( const automaton::RealTimeHeightDeterministicDPDA & pda);
+	static automaton::DPDA convert( const automaton::DPDA & pda);
 	static automaton::NPDA convert( const automaton::RealTimeHeightDeterministicNPDA & pda);
 	static automaton::NPDA convert( const automaton::NPDA & pda);
 
@@ -36,7 +38,9 @@ private:
 	void Visit(void*, const DPDA& automaton) const;
 	void Visit(void*, const SinglePopDPDA& automaton) const;
 	void Visit(void*, const InputDrivenNPDA& automaton) const;
+	void Visit(void*, const VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const NPDA& automaton) const;
 	void Visit(void*, const SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/conversions/fa2re/Algebraic.cpp b/alib2algo/src/conversions/fa2re/Algebraic.cpp
index 355bc18309..eb7aabaa8f 100644
--- a/alib2algo/src/conversions/fa2re/Algebraic.cpp
+++ b/alib2algo/src/conversions/fa2re/Algebraic.cpp
@@ -154,10 +154,18 @@ void Algebraic::Visit(void*, const automaton::InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void Algebraic::Visit(void*, const automaton::VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void Algebraic::Visit(void*, const automaton::VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void Algebraic::Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void Algebraic::Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/alib2algo/src/conversions/fa2re/Algebraic.h b/alib2algo/src/conversions/fa2re/Algebraic.h
index 6234e7fb8e..da0c67e7f6 100644
--- a/alib2algo/src/conversions/fa2re/Algebraic.h
+++ b/alib2algo/src/conversions/fa2re/Algebraic.h
@@ -49,7 +49,9 @@ private:
 	void Visit(void*, const automaton::ExtendedNFA&) const;
 	void Visit(void*, const automaton::CompactNFA&) const;
 	void Visit(void*, const automaton::InputDrivenNPDA&) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA&) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA&) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const;
 	void Visit(void*, const automaton::NPDA&) const;
 	void Visit(void*, const automaton::SinglePopNPDA&) const;
diff --git a/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.cpp b/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.cpp
index 8b45db111f..b4418f1324 100644
--- a/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.cpp
+++ b/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.cpp
@@ -107,11 +107,21 @@ void StateEliminationFormal::Visit(void*, const automaton::InputDrivenNPDA&) con
     throw exception::AlibException("Unsupported automaton type NPDA");
 }
 
+void StateEliminationFormal::Visit(void*, const automaton::VisiblyPushdownDPDA&) const
+{
+    throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void StateEliminationFormal::Visit(void*, const automaton::VisiblyPushdownNPDA&) const
 {
     throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void StateEliminationFormal::Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const
+{
+    throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void StateEliminationFormal::Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const
 {
     throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
diff --git a/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.h b/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.h
index e71cce1a26..8eba365ccf 100644
--- a/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.h
+++ b/alib2algo/src/conversions/fa2re/formal/StateEliminationFormal.h
@@ -49,7 +49,9 @@ private:
     void Visit(void*, const automaton::DPDA& automaton) const;
     void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
     void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+    void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
     void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+    void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
     void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
     void Visit(void*, const automaton::NPDA& automaton) const;
     void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.cpp b/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.cpp
index 612bceb278..1a0cafd101 100644
--- a/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.cpp
+++ b/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.cpp
@@ -105,11 +105,21 @@ void StateEliminationUnbounded::Visit(void*, const automaton::InputDrivenNPDA&)
     throw exception::AlibException("Unsupported automaton type NPDA");
 }
 
+void StateEliminationUnbounded::Visit(void*, const automaton::VisiblyPushdownDPDA&) const
+{
+    throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void StateEliminationUnbounded::Visit(void*, const automaton::VisiblyPushdownNPDA&) const
 {
     throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void StateEliminationUnbounded::Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const
+{
+    throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void StateEliminationUnbounded::Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const
 {
     throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
diff --git a/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.h b/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.h
index fa6c114a17..29e101811f 100644
--- a/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.h
+++ b/alib2algo/src/conversions/fa2re/unbounded/StateEliminationUnbounded.h
@@ -50,7 +50,9 @@ private:
     void Visit(void*, const automaton::DPDA& automaton) const;
     void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
     void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+    void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
     void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+    void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
     void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
     void Visit(void*, const automaton::NPDA& automaton) const;
     void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/conversions/fa2rg/fa2lrg/FAtoLRGConverter.cpp b/alib2algo/src/conversions/fa2rg/fa2lrg/FAtoLRGConverter.cpp
index 131446fbb6..2a90f93f29 100644
--- a/alib2algo/src/conversions/fa2rg/fa2lrg/FAtoLRGConverter.cpp
+++ b/alib2algo/src/conversions/fa2rg/fa2lrg/FAtoLRGConverter.cpp
@@ -153,10 +153,18 @@ void FAtoLRGConverter::Visit(void*, const automaton::InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void FAtoLRGConverter::Visit(void*, const automaton::VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void FAtoLRGConverter::Visit(void*, const automaton::VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void FAtoLRGConverter::Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void FAtoLRGConverter::Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/alib2algo/src/conversions/fa2rg/fa2lrg/FAtoLRGConverter.h b/alib2algo/src/conversions/fa2rg/fa2lrg/FAtoLRGConverter.h
index 0daa7a5e20..d6b6e7a3db 100644
--- a/alib2algo/src/conversions/fa2rg/fa2lrg/FAtoLRGConverter.h
+++ b/alib2algo/src/conversions/fa2rg/fa2lrg/FAtoLRGConverter.h
@@ -40,7 +40,9 @@ private:
 	void Visit(void*, const automaton::DPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
 	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const automaton::NPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/conversions/fa2rg/fa2rrg/FAtoRRGConverter.cpp b/alib2algo/src/conversions/fa2rg/fa2rrg/FAtoRRGConverter.cpp
index c0a7c4d824..40f0dbfe54 100644
--- a/alib2algo/src/conversions/fa2rg/fa2rrg/FAtoRRGConverter.cpp
+++ b/alib2algo/src/conversions/fa2rg/fa2rrg/FAtoRRGConverter.cpp
@@ -146,10 +146,18 @@ void FAtoRRGConverter::Visit(void*, const automaton::InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void FAtoRRGConverter::Visit(void*, const automaton::VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void FAtoRRGConverter::Visit(void*, const automaton::VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void FAtoRRGConverter::Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void FAtoRRGConverter::Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/alib2algo/src/conversions/fa2rg/fa2rrg/FAtoRRGConverter.h b/alib2algo/src/conversions/fa2rg/fa2rrg/FAtoRRGConverter.h
index 15c9602413..a3c9c7c005 100644
--- a/alib2algo/src/conversions/fa2rg/fa2rrg/FAtoRRGConverter.h
+++ b/alib2algo/src/conversions/fa2rg/fa2rrg/FAtoRRGConverter.h
@@ -38,7 +38,9 @@ private:
 	void Visit(void*, const automaton::ExtendedNFA& automaton) const;
 	void Visit(void*, const automaton::CompactNFA& automaton) const;
 	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const automaton::NPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/determinize/nfa/NFADeterminizer.cpp b/alib2algo/src/determinize/nfa/NFADeterminizer.cpp
index c19dab33d1..0aeb51dd04 100644
--- a/alib2algo/src/determinize/nfa/NFADeterminizer.cpp
+++ b/alib2algo/src/determinize/nfa/NFADeterminizer.cpp
@@ -105,10 +105,18 @@ void NFADeterminizer::Visit(void*, const automaton::InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void NFADeterminizer::Visit(void*, const automaton::VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void NFADeterminizer::Visit(void*, const automaton::VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void NFADeterminizer::Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void NFADeterminizer::Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/alib2algo/src/determinize/nfa/NFADeterminizer.h b/alib2algo/src/determinize/nfa/NFADeterminizer.h
index 196f90fb4d..a0460772ec 100644
--- a/alib2algo/src/determinize/nfa/NFADeterminizer.h
+++ b/alib2algo/src/determinize/nfa/NFADeterminizer.h
@@ -33,7 +33,9 @@ private:
 	void Visit(void*, const automaton::DPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
 	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const automaton::NPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/epsilon/fsm/FSMEpsilonRemover.cpp b/alib2algo/src/epsilon/fsm/FSMEpsilonRemover.cpp
index 158c7b2d79..b6003de68b 100644
--- a/alib2algo/src/epsilon/fsm/FSMEpsilonRemover.cpp
+++ b/alib2algo/src/epsilon/fsm/FSMEpsilonRemover.cpp
@@ -112,10 +112,18 @@ void FSMEpsilonRemover::Visit(void*, const automaton::InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void FSMEpsilonRemover::Visit(void*, const automaton::VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void FSMEpsilonRemover::Visit(void*, const automaton::VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void FSMEpsilonRemover::Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void FSMEpsilonRemover::Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/alib2algo/src/epsilon/fsm/FSMEpsilonRemover.h b/alib2algo/src/epsilon/fsm/FSMEpsilonRemover.h
index 3aa68eaa75..4e4781caa5 100644
--- a/alib2algo/src/epsilon/fsm/FSMEpsilonRemover.h
+++ b/alib2algo/src/epsilon/fsm/FSMEpsilonRemover.h
@@ -41,7 +41,9 @@ private:
 	void Visit(void*, const automaton::DPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
 	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const automaton::NPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
diff --git a/alib2algo/src/minimize/dfa/MinimizeDFA.cpp b/alib2algo/src/minimize/dfa/MinimizeDFA.cpp
index 7988229747..06bdaf0cbd 100644
--- a/alib2algo/src/minimize/dfa/MinimizeDFA.cpp
+++ b/alib2algo/src/minimize/dfa/MinimizeDFA.cpp
@@ -177,10 +177,18 @@ void MinimizeDFA::Visit(void*, const automaton::InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void MinimizeDFA::Visit(void*, const automaton::VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void MinimizeDFA::Visit(void*, const automaton::VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void MinimizeDFA::Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void MinimizeDFA::Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/alib2algo/src/minimize/dfa/MinimizeDFA.h b/alib2algo/src/minimize/dfa/MinimizeDFA.h
index ff5efb966d..b1d50f2c81 100644
--- a/alib2algo/src/minimize/dfa/MinimizeDFA.h
+++ b/alib2algo/src/minimize/dfa/MinimizeDFA.h
@@ -32,7 +32,9 @@ protected:
 	void Visit(void*, const automaton::DPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
 	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const automaton::NPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
diff --git a/alib2data/src/Api.cpp b/alib2data/src/Api.cpp
index 3d95905352..8e626c6e69 100644
--- a/alib2data/src/Api.cpp
+++ b/alib2data/src/Api.cpp
@@ -218,6 +218,14 @@ std::list<sax::Token> api<automaton::InputDrivenNPDA>::compose(const automaton::
 	return ToXMLComposers::automatonComposer.compose(data);
 }
 
+automaton::VisiblyPushdownDPDA api<automaton::VisiblyPushdownDPDA>::parse(std::list<sax::Token>& input) {
+	return FromXMLParsers::automatonParser.parseVisiblyPushdownDPDA(input);
+}
+
+std::list<sax::Token> api<automaton::VisiblyPushdownDPDA>::compose(const automaton::VisiblyPushdownDPDA& data) {
+	return ToXMLComposers::automatonComposer.compose(data);
+}
+
 automaton::VisiblyPushdownNPDA api<automaton::VisiblyPushdownNPDA>::parse(std::list<sax::Token>& input) {
 	return FromXMLParsers::automatonParser.parseVisiblyPushdownNPDA(input);
 }
@@ -226,6 +234,14 @@ std::list<sax::Token> api<automaton::VisiblyPushdownNPDA>::compose(const automat
 	return ToXMLComposers::automatonComposer.compose(data);
 }
 
+automaton::RealTimeHeightDeterministicDPDA api<automaton::RealTimeHeightDeterministicDPDA>::parse(std::list<sax::Token>& input) {
+	return FromXMLParsers::automatonParser.parseRealTimeHeightDeterministicDPDA(input);
+}
+
+std::list<sax::Token> api<automaton::RealTimeHeightDeterministicDPDA>::compose(const automaton::RealTimeHeightDeterministicDPDA& data) {
+	return ToXMLComposers::automatonComposer.compose(data);
+}
+
 automaton::RealTimeHeightDeterministicNPDA api<automaton::RealTimeHeightDeterministicNPDA>::parse(std::list<sax::Token>& input) {
 	return FromXMLParsers::automatonParser.parseRealTimeHeightDeterministicNPDA(input);
 }
@@ -604,10 +620,18 @@ void ToXMLComposers::Visit(void* data, const automaton::InputDrivenNPDA& automat
 	*((std::list<sax::Token>*) data) = std::move(api<automaton::InputDrivenNPDA>::compose(automaton));
 }
 
+void ToXMLComposers::Visit(void* data, const automaton::VisiblyPushdownDPDA& automaton) const {
+	*((std::list<sax::Token>*) data) = std::move(api<automaton::VisiblyPushdownDPDA>::compose(automaton));
+}
+
 void ToXMLComposers::Visit(void* data, const automaton::VisiblyPushdownNPDA& automaton) const {
 	*((std::list<sax::Token>*) data) = std::move(api<automaton::VisiblyPushdownNPDA>::compose(automaton));
 }
 
+void ToXMLComposers::Visit(void* data, const automaton::RealTimeHeightDeterministicDPDA& automaton) const {
+	*((std::list<sax::Token>*) data) = std::move(api<automaton::RealTimeHeightDeterministicDPDA>::compose(automaton));
+}
+
 void ToXMLComposers::Visit(void* data, const automaton::RealTimeHeightDeterministicNPDA& automaton) const {
 	*((std::list<sax::Token>*) data) = std::move(api<automaton::RealTimeHeightDeterministicNPDA>::compose(automaton));
 }
diff --git a/alib2data/src/Api.hpp b/alib2data/src/Api.hpp
index e8dd119aad..0f5dd1f5d0 100644
--- a/alib2data/src/Api.hpp
+++ b/alib2data/src/Api.hpp
@@ -198,12 +198,24 @@ struct api<automaton::InputDrivenNPDA> {
 	static std::list<sax::Token> compose(const automaton::InputDrivenNPDA& data);
 };
 
+template<>
+struct api<automaton::VisiblyPushdownDPDA> {
+	static automaton::VisiblyPushdownDPDA parse(std::list<sax::Token>& input);
+	static std::list<sax::Token> compose(const automaton::VisiblyPushdownDPDA& data);
+};
+
 template<>
 struct api<automaton::VisiblyPushdownNPDA> {
 	static automaton::VisiblyPushdownNPDA parse(std::list<sax::Token>& input);
 	static std::list<sax::Token> compose(const automaton::VisiblyPushdownNPDA& data);
 };
 
+template<>
+struct api<automaton::RealTimeHeightDeterministicDPDA> {
+	static automaton::RealTimeHeightDeterministicDPDA parse(std::list<sax::Token>& input);
+	static std::list<sax::Token> compose(const automaton::RealTimeHeightDeterministicDPDA& data);
+};
+
 template<>
 struct api<automaton::RealTimeHeightDeterministicNPDA> {
 	static automaton::RealTimeHeightDeterministicNPDA parse(std::list<sax::Token>& input);
@@ -482,7 +494,9 @@ class ToXMLComposers : public VisitableObjectBase::const_visitor_type {
 	void Visit(void*, const automaton::DPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
 	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const automaton::NPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
diff --git a/alib2data/src/automaton/AutomatonBase.h b/alib2data/src/automaton/AutomatonBase.h
index ab8fa4f0d0..6869ac08c7 100644
--- a/alib2data/src/automaton/AutomatonBase.h
+++ b/alib2data/src/automaton/AutomatonBase.h
@@ -14,7 +14,7 @@
 namespace automaton {
 
 typedef std::acceptor_base<
-			automaton::UnknownAutomaton, automaton::DFA, automaton::NFA, automaton::EpsilonNFA, automaton::CompactNFA, automaton::ExtendedNFA, automaton::DPDA, automaton::SinglePopDPDA, automaton::InputDrivenNPDA, automaton::VisiblyPushdownNPDA, automaton::RealTimeHeightDeterministicNPDA, automaton::NPDA, automaton::SinglePopNPDA, automaton::OneTapeDTM
+			automaton::UnknownAutomaton, automaton::DFA, automaton::NFA, automaton::EpsilonNFA, automaton::CompactNFA, automaton::ExtendedNFA, automaton::DPDA, automaton::SinglePopDPDA, automaton::InputDrivenNPDA, automaton::VisiblyPushdownDPDA, automaton::VisiblyPushdownNPDA, automaton::RealTimeHeightDeterministicDPDA, automaton::RealTimeHeightDeterministicNPDA, automaton::NPDA, automaton::SinglePopNPDA, automaton::OneTapeDTM
 	> VisitableAutomatonBase;
 
 /**
diff --git a/alib2data/src/automaton/AutomatonFeatures.h b/alib2data/src/automaton/AutomatonFeatures.h
index 8ae376dfda..9e0776ee8e 100644
--- a/alib2data/src/automaton/AutomatonFeatures.h
+++ b/alib2data/src/automaton/AutomatonFeatures.h
@@ -20,7 +20,9 @@ enum class FEATURES {
 	DPDA,
 	SINGLE_POP_DPDA,
 	INPUT_DRIVEN_NPDA,
+	VISIBLY_PUSHDOWN_DPDA,
 	VISIBLY_PUSHDOWN_NPDA,
+	REAL_TIME_HEIGHT_DETERMINISTIC_DPDA,
 	REAL_TIME_HEIGHT_DETERMINISTIC_NPDA,
 	NPDA,
 	SINGLE_POP_NPDA,
diff --git a/alib2data/src/automaton/AutomatonFromXMLParser.cpp b/alib2data/src/automaton/AutomatonFromXMLParser.cpp
index 7d7d4fa8e7..597a5871d0 100644
--- a/alib2data/src/automaton/AutomatonFromXMLParser.cpp
+++ b/alib2data/src/automaton/AutomatonFromXMLParser.cpp
@@ -47,9 +47,15 @@ Automaton AutomatonFromXMLParser::parseAutomaton(std::list<sax::Token>& input, c
 	} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "InputDrivenNPDA")) {
 		if(!features.count(FEATURES::INPUT_DRIVEN_NPDA)) throw exception::AlibException();
 		return Automaton(parseInputDrivenNPDA(input));
+	} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "VisiblyPushdownDPDA")) {
+		if(!features.count(FEATURES::VISIBLY_PUSHDOWN_DPDA)) throw exception::AlibException();
+		return Automaton(parseVisiblyPushdownDPDA(input));
 	} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "VisiblyPushdownNPDA")) {
 		if(!features.count(FEATURES::VISIBLY_PUSHDOWN_NPDA)) throw exception::AlibException();
 		return Automaton(parseVisiblyPushdownNPDA(input));
+	} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "RealTimeHeightDeterministicDPDA")) {
+		if(!features.count(FEATURES::REAL_TIME_HEIGHT_DETERMINISTIC_DPDA)) throw exception::AlibException();
+		return Automaton(parseRealTimeHeightDeterministicDPDA(input));
 	} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "RealTimeHeightDeterministicNPDA")) {
 		if(!features.count(FEATURES::REAL_TIME_HEIGHT_DETERMINISTIC_NPDA)) throw exception::AlibException();
 		return Automaton(parseRealTimeHeightDeterministicNPDA(input));
@@ -74,31 +80,11 @@ bool AutomatonFromXMLParser::first(std::list<sax::Token>& input) const {
 	}
 }
 
-template<>
-void AutomatonFromXMLParser::parseTransitions(std::list<sax::Token> &input, RealTimeHeightDeterministicNPDA& automaton) const {
-	popToken(input, sax::Token::TokenType::START_ELEMENT, "transitions");
-	while (isTokenType(input, sax::Token::TokenType::START_ELEMENT)) {
-		parseTransition(input, automaton);
-	}
-	popToken(input, sax::Token::TokenType::END_ELEMENT, "transitions");
-}
-
-template<>
-void AutomatonFromXMLParser::parseTransitions(std::list<sax::Token> &input, VisiblyPushdownNPDA& automaton) const {
-	popToken(input, sax::Token::TokenType::START_ELEMENT, "transitions");
-	while (isTokenType(input, sax::Token::TokenType::START_ELEMENT)) {
-		parseTransition(input, automaton);
-	}
-	popToken(input, sax::Token::TokenType::END_ELEMENT, "transitions");
-}
-
 template<class T>
 void AutomatonFromXMLParser::parseTransitions(std::list<sax::Token> &input, T& automaton) const {
 	popToken(input, sax::Token::TokenType::START_ELEMENT, "transitions");
 	while (isTokenType(input, sax::Token::TokenType::START_ELEMENT)) {
-		popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 		parseTransition(input, automaton);
-		popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 	}
 	popToken(input, sax::Token::TokenType::END_ELEMENT, "transitions");
 }
@@ -306,6 +292,33 @@ InputDrivenNPDA AutomatonFromXMLParser::parseInputDrivenNPDA(std::list<sax::Toke
 	return automaton;
 }
 
+VisiblyPushdownDPDA AutomatonFromXMLParser::parseVisiblyPushdownDPDA(std::list<sax::Token>& input) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "VisiblyPushdownDPDA");
+
+	std::set<State> states = parseStates(input);
+	std::set<alphabet::Symbol> callInputSymbols = parseCallInputAlphabet(input);
+	std::set<alphabet::Symbol> returnInputSymbols = parseReturnInputAlphabet(input);
+	std::set<alphabet::Symbol> localInputSymbols = parseLocalInputAlphabet(input);
+	std::set<alphabet::Symbol> stackSymbols = parseStackAlphabet(input);
+	State initialState = parseInitialState(input);
+	alphabet::Symbol bottomOfTheStackSymbol = parseBottomOfTheStackSymbol(input);
+	std::set<State> finalStates = parseFinalStates(input);
+
+	VisiblyPushdownDPDA automaton(initialState, bottomOfTheStackSymbol);
+	automaton.setStates(states);
+	automaton.setCallInputSymbols(callInputSymbols);
+	automaton.setReturnInputSymbols(returnInputSymbols);
+	automaton.setLocalInputSymbols(localInputSymbols);
+	automaton.setStackSymbols(stackSymbols);
+	automaton.setFinalStates(finalStates);
+
+	parseTransitions<VisiblyPushdownDPDA>(input, automaton);
+
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "VisiblyPushdownDPDA");
+
+	return automaton;
+}
+
 VisiblyPushdownNPDA AutomatonFromXMLParser::parseVisiblyPushdownNPDA(std::list<sax::Token>& input) const {
 	popToken(input, sax::Token::TokenType::START_ELEMENT, "VisiblyPushdownNPDA");
 
@@ -334,6 +347,29 @@ VisiblyPushdownNPDA AutomatonFromXMLParser::parseVisiblyPushdownNPDA(std::list<s
 	return automaton;
 }
 
+RealTimeHeightDeterministicDPDA AutomatonFromXMLParser::parseRealTimeHeightDeterministicDPDA(std::list<sax::Token>& input) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "RealTimeHeightDeterministicDPDA");
+
+	std::set<State> states = parseStates(input);
+	std::set<alphabet::Symbol> inputSymbols = parseInputAlphabet(input);
+	std::set<alphabet::Symbol> stackSymbols = parseStackAlphabet(input);
+	State initialState = parseInitialState(input);
+	alphabet::Symbol bottomOfTheStackSymbol = parseBottomOfTheStackSymbol(input);
+	std::set<State> finalStates = parseFinalStates(input);
+
+	RealTimeHeightDeterministicDPDA automaton(initialState, bottomOfTheStackSymbol);
+	automaton.setStates(states);
+	automaton.setInputSymbols(inputSymbols);
+	automaton.setStackSymbols(stackSymbols);
+	automaton.setFinalStates(finalStates);
+
+	parseTransitions<RealTimeHeightDeterministicDPDA>(input, automaton);
+
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "RealTimeHeightDeterministicDPDA");
+
+	return automaton;
+}
+
 RealTimeHeightDeterministicNPDA AutomatonFromXMLParser::parseRealTimeHeightDeterministicNPDA(std::list<sax::Token>& input) const {
 	popToken(input, sax::Token::TokenType::START_ELEMENT, "RealTimeHeightDeterministicNPDA");
 
@@ -581,73 +617,119 @@ void AutomatonFromXMLParser::parseInputToPushdownStoreOperation(std::list<sax::T
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, DFA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	alphabet::Symbol inputSymbol = parseTransitionInputSymbol(input);
 	State to = parseTransitionTo(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputSymbol, to);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, NFA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	alphabet::Symbol inputSymbol = parseTransitionInputSymbol(input);
 	State to = parseTransitionTo(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputSymbol, to);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, EpsilonNFA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	std::variant<string::Epsilon, alphabet::Symbol> inputVariant = parseTransitionInputEpsilonSymbol(input);
 	State to = parseTransitionTo(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputVariant, to);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, CompactNFA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	string::LinearString inputString = parseTransitionInputString(input);
 	State to = parseTransitionTo(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputString, to);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, ExtendedNFA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	regexp::RegExp inputRegexp = parseTransitionInputRegexp(input);
 	State to = parseTransitionTo(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputRegexp, to);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, DPDA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	std::variant<string::Epsilon, alphabet::Symbol> inputSymbol = parseTransitionInputEpsilonSymbol(input);
 	std::vector<alphabet::Symbol> pop = parseTransitionPop(input);
 	State to = parseTransitionTo(input);
 	std::vector<alphabet::Symbol> push = parseTransitionPush(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputSymbol, pop, to, push);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, SinglePopDPDA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	std::variant<string::Epsilon, alphabet::Symbol> inputSymbol = parseTransitionInputEpsilonSymbol(input);
 	alphabet::Symbol pop = parseTransitionSinglePop(input);
 	State to = parseTransitionTo(input);
 	std::vector<alphabet::Symbol> push = parseTransitionPush(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputSymbol, pop, to, push);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, InputDrivenNPDA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	alphabet::Symbol inputSymbol = parseTransitionInputSymbol(input);
 	State to = parseTransitionTo(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputSymbol, to);
 }
 
+void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, VisiblyPushdownDPDA& automaton) const {
+	if(isToken(input, sax::Token::TokenType::START_ELEMENT, "callTransition")) {
+		popToken(input, sax::Token::TokenType::START_ELEMENT, "callTransition");
+		State from = parseTransitionFrom(input);
+		alphabet::Symbol inputSymbol = parseTransitionInputSymbol(input);
+		State to = parseTransitionTo(input);
+		alphabet::Symbol push = parseTransitionSinglePush(input);
+
+		automaton.addCallTransition(from, inputSymbol, to, push);
+		popToken(input, sax::Token::TokenType::END_ELEMENT, "callTransition");
+	} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "returnTransition")) {
+		popToken(input, sax::Token::TokenType::START_ELEMENT, "returnTransition");
+		State from = parseTransitionFrom(input);
+		alphabet::Symbol inputSymbol = parseTransitionInputSymbol(input);
+		alphabet::Symbol pop = parseTransitionSinglePop(input);
+		State to = parseTransitionTo(input);
+
+		automaton.addReturnTransition(from, inputSymbol, pop, to);
+		popToken(input, sax::Token::TokenType::END_ELEMENT, "returnTransition");
+	} else {
+		popToken(input, sax::Token::TokenType::START_ELEMENT, "localTransition");
+		State from = parseTransitionFrom(input);
+		alphabet::Symbol inputSymbol = parseTransitionInputSymbol(input);
+		State to = parseTransitionTo(input);
+
+		automaton.addLocalTransition(from, inputSymbol, to);
+		popToken(input, sax::Token::TokenType::END_ELEMENT, "localTransition");
+	}
+}
+
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, VisiblyPushdownNPDA& automaton) const {
 	if(isToken(input, sax::Token::TokenType::START_ELEMENT, "callTransition")) {
 		popToken(input, sax::Token::TokenType::START_ELEMENT, "callTransition");
@@ -678,6 +760,36 @@ void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, Visib
 	}
 }
 
+void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, RealTimeHeightDeterministicDPDA& automaton) const {
+	if(isToken(input, sax::Token::TokenType::START_ELEMENT, "callTransition")) {
+		popToken(input, sax::Token::TokenType::START_ELEMENT, "callTransition");
+		State from = parseTransitionFrom(input);
+		std::variant<string::Epsilon, alphabet::Symbol> inputSymbol = parseTransitionInputEpsilonSymbol(input);
+		State to = parseTransitionTo(input);
+		alphabet::Symbol push = parseTransitionSinglePush(input);
+
+		automaton.addCallTransition(from, inputSymbol, to, push);
+		popToken(input, sax::Token::TokenType::END_ELEMENT, "callTransition");
+	} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "returnTransition")) {
+		popToken(input, sax::Token::TokenType::START_ELEMENT, "returnTransition");
+		State from = parseTransitionFrom(input);
+		std::variant<string::Epsilon, alphabet::Symbol> inputSymbol = parseTransitionInputEpsilonSymbol(input);
+		alphabet::Symbol pop = parseTransitionSinglePop(input);
+		State to = parseTransitionTo(input);
+
+		automaton.addReturnTransition(from, inputSymbol, pop, to);
+		popToken(input, sax::Token::TokenType::END_ELEMENT, "returnTransition");
+	} else {
+		popToken(input, sax::Token::TokenType::START_ELEMENT, "localTransition");
+		State from = parseTransitionFrom(input);
+		std::variant<string::Epsilon, alphabet::Symbol> inputSymbol = parseTransitionInputEpsilonSymbol(input);
+		State to = parseTransitionTo(input);
+
+		automaton.addLocalTransition(from, inputSymbol, to);
+		popToken(input, sax::Token::TokenType::END_ELEMENT, "localTransition");
+	}
+}
+
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, RealTimeHeightDeterministicNPDA& automaton) const {
 	if(isToken(input, sax::Token::TokenType::START_ELEMENT, "callTransition")) {
 		popToken(input, sax::Token::TokenType::START_ELEMENT, "callTransition");
@@ -709,36 +821,43 @@ void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, RealT
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, NPDA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	std::variant<string::Epsilon, alphabet::Symbol> inputSymbol = parseTransitionInputEpsilonSymbol(input);
 	std::vector<alphabet::Symbol> pop = parseTransitionPop(input);
 	State to = parseTransitionTo(input);
 	std::vector<alphabet::Symbol> push = parseTransitionPush(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputSymbol, pop, to, push);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, SinglePopNPDA& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	std::variant<string::Epsilon, alphabet::Symbol> inputSymbol = parseTransitionInputEpsilonSymbol(input);
 	alphabet::Symbol pop = parseTransitionSinglePop(input);
 	State to = parseTransitionTo(input);
 	std::vector<alphabet::Symbol> push = parseTransitionPush(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputSymbol, pop, to, push);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, OneTapeDTM& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	State from = parseTransitionFrom(input);
 	alphabet::Symbol inputSymbol = parseTransitionInputSymbol(input);
 	State to = parseTransitionTo(input);
 	alphabet::Symbol outputSymbol = parseTransitionOutputSymbol(input);
 	Shift shift = parseTransitionShift(input);
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(from, inputSymbol, to, outputSymbol, shift);
 }
 
 void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, UnknownAutomaton& automaton) const {
+	popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
 	UnknownTransition transition;
 
 	while (isTokenType(input, sax::Token::TokenType::START_ELEMENT)) {
@@ -760,6 +879,7 @@ void AutomatonFromXMLParser::parseTransition(std::list<sax::Token>& input, Unkno
 			throw sax::ParserException(sax::Token("transitions", sax::Token::TokenType::END_ELEMENT), input.front());
 		}
 	}
+	popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");
 
 	automaton.addTransition(transition);
 }
diff --git a/alib2data/src/automaton/AutomatonFromXMLParser.h b/alib2data/src/automaton/AutomatonFromXMLParser.h
index 14cd31f399..fc74412c3c 100644
--- a/alib2data/src/automaton/AutomatonFromXMLParser.h
+++ b/alib2data/src/automaton/AutomatonFromXMLParser.h
@@ -20,7 +20,9 @@
 #include "PDA/DPDA.h"
 #include "PDA/SinglePopDPDA.h"
 #include "PDA/InputDrivenNPDA.h"
+#include "PDA/VisiblyPushdownDPDA.h"
 #include "PDA/VisiblyPushdownNPDA.h"
+#include "PDA/RealTimeHeightDeterministicDPDA.h"
 #include "PDA/RealTimeHeightDeterministicNPDA.h"
 #include "PDA/NPDA.h"
 #include "PDA/SinglePopNPDA.h"
@@ -71,6 +73,7 @@ class AutomatonFromXMLParser : public sax::FromXMLParserHelper {
 
 	template<class T>
 	void parseTransitions(std::list<sax::Token> &input, T& automaton) const;
+
 	void parseTransition(std::list<sax::Token>& input, UnknownAutomaton& automaton) const;
 	void parseTransition(std::list<sax::Token>& input, EpsilonNFA& automaton) const;
 	void parseTransition(std::list<sax::Token>& input, NFA& automaton) const;
@@ -80,7 +83,9 @@ class AutomatonFromXMLParser : public sax::FromXMLParserHelper {
 	void parseTransition(std::list<sax::Token>& input, DPDA& automaton) const;
 	void parseTransition(std::list<sax::Token>& input, SinglePopDPDA& automaton) const;
 	void parseTransition(std::list<sax::Token>& input, InputDrivenNPDA& automaton) const;
+	void parseTransition(std::list<sax::Token>& input, VisiblyPushdownDPDA& automaton) const;
 	void parseTransition(std::list<sax::Token>& input, VisiblyPushdownNPDA& automaton) const;
+	void parseTransition(std::list<sax::Token>& input, RealTimeHeightDeterministicDPDA& automaton) const;
 	void parseTransition(std::list<sax::Token>& input, RealTimeHeightDeterministicNPDA& automaton) const;
 	void parseTransition(std::list<sax::Token>& input, NPDA& automaton) const;
 	void parseTransition(std::list<sax::Token>& input, SinglePopNPDA& automaton) const;
@@ -111,7 +116,9 @@ class AutomatonFromXMLParser : public sax::FromXMLParserHelper {
 	DPDA parseDPDA(std::list<sax::Token>& input) const;
 	SinglePopDPDA parseSinglePopDPDA(std::list<sax::Token>& input) const;
 	InputDrivenNPDA parseInputDrivenNPDA(std::list<sax::Token>& input) const;
+	VisiblyPushdownDPDA parseVisiblyPushdownDPDA(std::list<sax::Token>& input) const;
 	VisiblyPushdownNPDA parseVisiblyPushdownNPDA(std::list<sax::Token>& input) const;
+	RealTimeHeightDeterministicDPDA parseRealTimeHeightDeterministicDPDA(std::list<sax::Token>& input) const;
 	RealTimeHeightDeterministicNPDA parseRealTimeHeightDeterministicNPDA(std::list<sax::Token>& input) const;
 	NPDA parseNPDA(std::list<sax::Token>& input) const;
 	SinglePopNPDA parseSinglePopNPDA(std::list<sax::Token>& input) const;
diff --git a/alib2data/src/automaton/AutomatonToXMLComposer.cpp b/alib2data/src/automaton/AutomatonToXMLComposer.cpp
index fcd7096ce8..fd926bb052 100644
--- a/alib2data/src/automaton/AutomatonToXMLComposer.cpp
+++ b/alib2data/src/automaton/AutomatonToXMLComposer.cpp
@@ -299,6 +299,40 @@ void AutomatonToXMLComposer::composeTransitions(std::list<sax::Token>& out, cons
 	out.push_back(sax::Token("transitions", sax::Token::TokenType::END_ELEMENT));
 }
 
+void AutomatonToXMLComposer::composeTransitions(std::list<sax::Token>& out, const VisiblyPushdownDPDA& automaton) const {
+	out.push_back(sax::Token("transitions", sax::Token::TokenType::START_ELEMENT));
+	for(const auto& transition : automaton.getCallTransitions()) {
+		out.push_back(sax::Token("callTransition", sax::Token::TokenType::START_ELEMENT));
+
+		composeTransitionFrom(out, transition.first.first);
+		composeTransitionInputSymbol(out, transition.first.second);
+		composeTransitionTo(out, transition.second.first);
+		composeTransitionSinglePush(out, transition.second.second);
+
+		out.push_back(sax::Token("callTransition", sax::Token::TokenType::END_ELEMENT));
+	}
+	for(const auto& transition : automaton.getReturnTransitions()) {
+		out.push_back(sax::Token("returnTransition", sax::Token::TokenType::START_ELEMENT));
+
+		composeTransitionFrom(out, std::get<0>(transition.first));
+		composeTransitionInputSymbol(out, std::get<1>(transition.first));
+		composeTransitionSinglePop(out, std::get<2>(transition.first));
+		composeTransitionTo(out, transition.second);
+
+		out.push_back(sax::Token("returnTransition", sax::Token::TokenType::END_ELEMENT));
+	}
+	for(const auto& transition : automaton.getLocalTransitions()) {
+		out.push_back(sax::Token("localTransition", sax::Token::TokenType::START_ELEMENT));
+
+		composeTransitionFrom(out, transition.first.first);
+		composeTransitionInputSymbol(out, transition.first.second);
+		composeTransitionTo(out, transition.second);
+
+		out.push_back(sax::Token("localTransition", sax::Token::TokenType::END_ELEMENT));
+	}
+	out.push_back(sax::Token("transitions", sax::Token::TokenType::END_ELEMENT));
+}
+
 void AutomatonToXMLComposer::composeTransitions(std::list<sax::Token>& out, const VisiblyPushdownNPDA& automaton) const {
 	out.push_back(sax::Token("transitions", sax::Token::TokenType::START_ELEMENT));
 	for(const auto& transition : automaton.getCallTransitions()) {
@@ -336,7 +370,40 @@ void AutomatonToXMLComposer::composeTransitions(std::list<sax::Token>& out, cons
 			out.push_back(sax::Token("localTransition", sax::Token::TokenType::END_ELEMENT));
 		}
 	}
+	out.push_back(sax::Token("transitions", sax::Token::TokenType::END_ELEMENT));
+}
+
+void AutomatonToXMLComposer::composeTransitions(std::list<sax::Token>& out, const RealTimeHeightDeterministicDPDA& automaton) const {
+	out.push_back(sax::Token("transitions", sax::Token::TokenType::START_ELEMENT));
+	for(const auto& transition : automaton.getCallTransitions()) {
+		out.push_back(sax::Token("callTransition", sax::Token::TokenType::START_ELEMENT));
 
+		composeTransitionFrom(out, transition.first.first);
+		composeTransitionInputEpsilonSymbol(out, transition.first.second);
+		composeTransitionTo(out, transition.second.first);
+		composeTransitionSinglePush(out, transition.second.second);
+
+		out.push_back(sax::Token("callTransition", sax::Token::TokenType::END_ELEMENT));
+	}
+	for(const auto& transition : automaton.getReturnTransitions()) {
+		out.push_back(sax::Token("returnTransition", sax::Token::TokenType::START_ELEMENT));
+
+		composeTransitionFrom(out, std::get<0>(transition.first));
+		composeTransitionInputEpsilonSymbol(out, std::get<1>(transition.first));
+		composeTransitionSinglePop(out, std::get<2>(transition.first));
+		composeTransitionTo(out, transition.second);
+
+		out.push_back(sax::Token("returnTransition", sax::Token::TokenType::END_ELEMENT));
+	}
+	for(const auto& transition : automaton.getLocalTransitions()) {
+		out.push_back(sax::Token("localTransition", sax::Token::TokenType::START_ELEMENT));
+
+		composeTransitionFrom(out, transition.first.first);
+		composeTransitionInputEpsilonSymbol(out, transition.first.second);
+		composeTransitionTo(out, transition.second);
+
+		out.push_back(sax::Token("localTransition", sax::Token::TokenType::END_ELEMENT));
+	}
 	out.push_back(sax::Token("transitions", sax::Token::TokenType::END_ELEMENT));
 }
 
@@ -377,7 +444,6 @@ void AutomatonToXMLComposer::composeTransitions(std::list<sax::Token>& out, cons
 			out.push_back(sax::Token("localTransition", sax::Token::TokenType::END_ELEMENT));
 		}
 	}
-
 	out.push_back(sax::Token("transitions", sax::Token::TokenType::END_ELEMENT));
 }
 
@@ -694,6 +760,24 @@ std::list<sax::Token> AutomatonToXMLComposer::compose(const InputDrivenNPDA& aut
 	return out;
 }
 
+std::list<sax::Token> AutomatonToXMLComposer::compose(const VisiblyPushdownDPDA& automaton) const {
+	std::list<sax::Token> out;
+	out.push_back(sax::Token("VisiblyPushdownDPDA", sax::Token::TokenType::START_ELEMENT));
+
+	composeStates(out, automaton.getStates());
+	composeCallInputAlphabet(out, automaton.getCallInputAlphabet());
+	composeReturnInputAlphabet(out, automaton.getReturnInputAlphabet());
+	composeLocalInputAlphabet(out, automaton.getLocalInputAlphabet());
+	composeStackAlphabet(out, automaton.getStackAlphabet());
+	composeInitialState(out, automaton.getInitialState());
+	composeBottomOfTheStackSymbol(out, automaton.getBottomOfTheStackSymbol());
+	composeFinalStates(out, automaton.getFinalStates());
+	composeTransitions(out, automaton);
+
+	out.push_back(sax::Token("VisiblyPushdownDPDA", sax::Token::TokenType::END_ELEMENT));
+	return out;
+}
+
 std::list<sax::Token> AutomatonToXMLComposer::compose(const VisiblyPushdownNPDA& automaton) const {
 	std::list<sax::Token> out;
 	out.push_back(sax::Token("VisiblyPushdownNPDA", sax::Token::TokenType::START_ELEMENT));
@@ -712,6 +796,22 @@ std::list<sax::Token> AutomatonToXMLComposer::compose(const VisiblyPushdownNPDA&
 	return out;
 }
 
+std::list<sax::Token> AutomatonToXMLComposer::compose(const RealTimeHeightDeterministicDPDA& automaton) const {
+	std::list<sax::Token> out;
+	out.push_back(sax::Token("RealTimeHeightDeterministicDPDA", sax::Token::TokenType::START_ELEMENT));
+
+	composeStates(out, automaton.getStates());
+	composeInputAlphabet(out, automaton.getInputAlphabet());
+	composeStackAlphabet(out, automaton.getStackAlphabet());
+	composeInitialState(out, automaton.getInitialState());
+	composeBottomOfTheStackSymbol(out, automaton.getBottomOfTheStackSymbol());
+	composeFinalStates(out, automaton.getFinalStates());
+	composeTransitions(out, automaton);
+
+	out.push_back(sax::Token("RealTimeHeightDeterministicDPDA", sax::Token::TokenType::END_ELEMENT));
+	return out;
+}
+
 std::list<sax::Token> AutomatonToXMLComposer::compose(const RealTimeHeightDeterministicNPDA& automaton) const {
 	std::list<sax::Token> out;
 	out.push_back(sax::Token("RealTimeHeightDeterministicNPDA", sax::Token::TokenType::START_ELEMENT));
diff --git a/alib2data/src/automaton/AutomatonToXMLComposer.h b/alib2data/src/automaton/AutomatonToXMLComposer.h
index 79da04ae10..19157b00b0 100644
--- a/alib2data/src/automaton/AutomatonToXMLComposer.h
+++ b/alib2data/src/automaton/AutomatonToXMLComposer.h
@@ -18,7 +18,10 @@
 #include "FSM/CompactNFA.h"
 #include "FSM/ExtendedNFA.h"
 #include "PDA/InputDrivenNPDA.h"
+#include "PDA/VisiblyPushdownDPDA.h"
 #include "PDA/VisiblyPushdownNPDA.h"
+#include "PDA/RealTimeHeightDeterministicDPDA.h"
+#include "PDA/RealTimeHeightDeterministicNPDA.h"
 #include "PDA/NPDA.h"
 #include "PDA/SinglePopNPDA.h"
 #include "TM/OneTapeDTM.h"
@@ -62,7 +65,9 @@ class AutomatonToXMLComposer {
 	void composeTransitions(std::list<sax::Token>&, const DPDA& automaton) const;
 	void composeTransitions(std::list<sax::Token>&, const SinglePopDPDA& automaton) const;
 	void composeTransitions(std::list<sax::Token>&, const InputDrivenNPDA& automaton) const;
+	void composeTransitions(std::list<sax::Token>&, const VisiblyPushdownDPDA& automaton) const;
 	void composeTransitions(std::list<sax::Token>&, const VisiblyPushdownNPDA& automaton) const;
+	void composeTransitions(std::list<sax::Token>&, const RealTimeHeightDeterministicDPDA& automaton) const;
 	void composeTransitions(std::list<sax::Token>&, const RealTimeHeightDeterministicNPDA& automaton) const;
 	void composeTransitions(std::list<sax::Token>&, const NPDA& automaton) const;
 	void composeTransitions(std::list<sax::Token>&, const SinglePopNPDA& automaton) const;
@@ -101,7 +106,9 @@ class AutomatonToXMLComposer {
 	std::list<sax::Token> compose(const SinglePopDPDA& automaton) const;
 	std::list<sax::Token> compose(const InputDrivenNPDA& automaton) const;
 	std::list<sax::Token> compose(const VisiblyPushdownNPDA& automaton) const;
+	std::list<sax::Token> compose(const VisiblyPushdownDPDA& automaton) const;
 	std::list<sax::Token> compose(const RealTimeHeightDeterministicNPDA& automaton) const;
+	std::list<sax::Token> compose(const RealTimeHeightDeterministicDPDA& automaton) const;
 	std::list<sax::Token> compose(const NPDA& automaton) const;
 	std::list<sax::Token> compose(const SinglePopNPDA& automaton) const;
 	std::list<sax::Token> compose(const OneTapeDTM& automaton) const;
diff --git a/alib2data/src/automaton/FSM/FiniteAutomatonToStringComposer.cpp b/alib2data/src/automaton/FSM/FiniteAutomatonToStringComposer.cpp
index 46c180a133..131453e23c 100644
--- a/alib2data/src/automaton/FSM/FiniteAutomatonToStringComposer.cpp
+++ b/alib2data/src/automaton/FSM/FiniteAutomatonToStringComposer.cpp
@@ -198,10 +198,18 @@ void FiniteAutomatonToStringComposer::Visit(void*, const InputDrivenNPDA&) const
 	throw exception::AlibException();
 }
 
+void FiniteAutomatonToStringComposer::Visit(void*, const VisiblyPushdownDPDA&) const {
+	throw exception::AlibException();
+}
+
 void FiniteAutomatonToStringComposer::Visit(void*, const VisiblyPushdownNPDA&) const {
 	throw exception::AlibException();
 }
 
+void FiniteAutomatonToStringComposer::Visit(void*, const RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException();
+}
+
 void FiniteAutomatonToStringComposer::Visit(void*, const RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException();
 }
diff --git a/alib2data/src/automaton/FSM/FiniteAutomatonToStringComposer.h b/alib2data/src/automaton/FSM/FiniteAutomatonToStringComposer.h
index 74eac6ac19..7fa8f73e32 100644
--- a/alib2data/src/automaton/FSM/FiniteAutomatonToStringComposer.h
+++ b/alib2data/src/automaton/FSM/FiniteAutomatonToStringComposer.h
@@ -19,7 +19,9 @@ class FiniteAutomatonToStringComposer : public VisitableAutomatonBase::const_vis
 	void Visit(void*, const DPDA& automaton) const;
 	void Visit(void*, const SinglePopDPDA& automaton) const;
 	void Visit(void*, const InputDrivenNPDA& automaton) const;
+	void Visit(void*, const VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const NPDA& automaton) const;
 	void Visit(void*, const SinglePopNPDA& automaton) const;
diff --git a/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.cpp b/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.cpp
new file mode 100644
index 0000000000..039f42e8bd
--- /dev/null
+++ b/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.cpp
@@ -0,0 +1,409 @@
+/*
+ * RealTimeHeightDeterministicDPDA.cpp
+ *
+ *  Created on: Apr 10, 2013
+ *      Author: Jan Travnicek
+ */
+
+#include "RealTimeHeightDeterministicDPDA.h"
+#include "../../std/map.hpp"
+#include "../AutomatonException.h"
+#include <algorithm>
+#include <sstream>
+
+namespace automaton {
+
+RealTimeHeightDeterministicDPDA::RealTimeHeightDeterministicDPDA(const State& initialState, const alphabet::Symbol& bottomOfTheStackSymbol) : BottomOfTheStackSymbolPushdownStoreAlphabet(bottomOfTheStackSymbol), SingleInitialState(initialState) {
+
+}
+
+AutomatonBase* RealTimeHeightDeterministicDPDA::clone() const {
+	return new RealTimeHeightDeterministicDPDA(*this);
+}
+
+AutomatonBase* RealTimeHeightDeterministicDPDA::plunder() && {
+	return new RealTimeHeightDeterministicDPDA(std::move(*this));
+}
+
+bool RealTimeHeightDeterministicDPDA::removeState(const State& state) {
+	if (initialState == state) {
+		throw AutomatonException("State \"" + (std::string) state.getName() + "\" is initial state.");
+	}
+
+	if (finalStates.find(state) != finalStates.end()) {
+		throw AutomatonException("State \"" + (std::string) state.getName() + "\" is final state.");
+	}
+
+	for (const std::pair<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> >& callTransition : callTransitions) {
+		if (state == callTransition.first.first)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+		if(callTransition.second.first == state)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State>& returnTransition : returnTransitions) {
+		if (state == std::get<0>(returnTransition.first))
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+		if(returnTransition.second == state)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, State>& localTransition : localTransitions) {
+		if (state == localTransition.first.first)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+		if(localTransition.second == state)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+	}
+
+	return states.erase(state);
+}
+
+bool RealTimeHeightDeterministicDPDA::removeInputSymbol(const alphabet::Symbol& symbol) {
+	for (const std::pair<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> >& callTransition : callTransitions) {
+		if (callTransition.first.second.is<alphabet::Symbol>() && symbol == callTransition.first.second.get<alphabet::Symbol>())
+			throw AutomatonException("Input symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State>& returnTransition : returnTransitions) {
+		if (std::get<1>(returnTransition.first).is<alphabet::Symbol>() && symbol == std::get<1>(returnTransition.first).get<alphabet::Symbol>())
+			throw AutomatonException("Input symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, State>& localTransition : localTransitions) {
+		if (localTransition.first.second.is<alphabet::Symbol>() && symbol == localTransition.first.second.get<alphabet::Symbol>())
+			throw AutomatonException("Input symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	return inputAlphabet.erase(symbol);
+}
+
+bool RealTimeHeightDeterministicDPDA::removeStackSymbol(const alphabet::Symbol& symbol) {
+	for (const std::pair<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> >& callTransition : callTransitions) {
+		if (symbol == callTransition.second.second)
+			throw AutomatonException("Stack symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State>& returnTransition : returnTransitions) {
+		if (symbol == std::get<2>(returnTransition.first))
+			throw AutomatonException("Stack symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	if(bottomOfTheStackSymbol == symbol) {
+		throw AutomatonException("Stack symbol \"" + (std::string) symbol + "\" is start symbol.");
+	}
+
+	return stackAlphabet.erase(symbol);
+}
+
+bool RealTimeHeightDeterministicDPDA::addCallTransition(const State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const State& to, const alphabet::Symbol& push) {
+	if (states.find(from) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) from.getName() + "\" doesn't exist.");
+	}
+
+	if (input.is<alphabet::Symbol>() && inputAlphabet.find(input.get<alphabet::Symbol>()) == inputAlphabet.end()) {
+		throw AutomatonException("Input symbol \"" + (std::string) input.get<alphabet::Symbol>() + "\" doesn't exist.");
+	}
+
+	if (states.find(to) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) to.getName() + "\" doesn't exist.");
+	}
+
+	if (stackAlphabet.find(push) == stackAlphabet.end()) {
+		throw AutomatonException("Stack symbol \"" + (std::string) push + "\" doesn't exist.");
+	}
+
+	std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>> key(from, input);
+	std::pair<automaton::State, alphabet::Symbol> value = std::make_pair(to, push);
+
+	if(callTransitions.find(key) != callTransitions.end() && callTransitions.find(key)->second == value)
+		return false;
+
+	if(input.is<string::Epsilon>()) {
+		for(const auto& transition : callTransitions)
+			if(transition.first.first == from )
+				throw AutomatonException("Can't add epsilon transition from state \"" + (std::string) from + "\" when other transitions are present.");
+
+		for(const auto& transition : returnTransitions)
+			if(std::get<0>(transition.first) == from)
+				throw AutomatonException("Can't add epsilon transition from state \"" + (std::string) from + "\" when other transitions are present.");
+
+		for(const auto& transition : localTransitions)
+			if(transition.first.first == from)
+				throw AutomatonException("Can't add epsilon transition from state \"" + (std::string) from + "\" when other transitions are present.");
+	} else {
+		for(const auto& transition : callTransitions)
+			if(transition.first.first == from && (transition.first.second.is<string::Epsilon>() || transition.first.second == input))
+				throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+		for(const auto& transition : returnTransitions)
+			if(std::get<0>(transition.first) == from && (std::get<1>(transition.first).is<string::Epsilon>() || std::get<1>(transition.first) == input))
+				throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+		for(const auto& transition : localTransitions)
+			if(transition.first.first == from && (transition.first.second.is<string::Epsilon>() || transition.first.second == input))
+				throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+	}
+
+	callTransitions.insert(std::make_pair(key, value));
+	return true;
+}
+
+bool RealTimeHeightDeterministicDPDA::addCallTransition(const State& from, const State& to, const alphabet::Symbol& push) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(string::Epsilon::EPSILON);
+	return addCallTransition(from, inputVariant, to, push);
+}
+
+bool RealTimeHeightDeterministicDPDA::addCallTransition(const State& from, const alphabet::Symbol& input, const State& to, const alphabet::Symbol& push) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(input);
+	return addCallTransition(from, inputVariant, to, push);
+}
+
+bool RealTimeHeightDeterministicDPDA::addReturnTransition(const State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const alphabet::Symbol& pop, const State& to) {
+	if (states.find(from) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) from.getName() + "\" doesn't exist.");
+	}
+
+	if (input.is<alphabet::Symbol>() && inputAlphabet.find(input.get<alphabet::Symbol>()) == inputAlphabet.end()) {
+		throw AutomatonException("Input symbol \"" + (std::string) input.get<alphabet::Symbol>() + "\" doesn't exist.");
+	}
+
+	if (states.find(to) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) to.getName() + "\" doesn't exist.");
+	}
+
+	if (stackAlphabet.find(pop) == stackAlphabet.end()) {
+		throw AutomatonException("Stack symbol \"" + (std::string) pop + "\" doesn't exist.");
+	}
+
+	std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol> key(from, input, pop);
+
+	if(returnTransitions.find(key) != returnTransitions.end() && returnTransitions.find(key)->second == to)
+		return false;
+
+	if(input.is<string::Epsilon>()) {
+		for(const auto& transition : callTransitions)
+			if(transition.first.first == from )
+				throw AutomatonException("Can't add epsilon transition from state \"" + (std::string) from + "\" when other transitions are present.");
+
+		for(const auto& transition : returnTransitions)
+			if(std::get<0>(transition.first) == from && std::get<2>(transition.first) == pop)
+				throw AutomatonException("Can't add epsilon transition from state \"" + (std::string) from + "\" when other transitions are present.");
+
+		for(const auto& transition : localTransitions)
+			if(transition.first.first == from)
+				throw AutomatonException("Can't add epsilon transition from state \"" + (std::string) from + "\" when other transitions are present.");
+	} else {
+		for(const auto& transition : callTransitions)
+			if(transition.first.first == from && (transition.first.second.is<string::Epsilon>() || transition.first.second == input))
+				throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+		for(const auto& transition : returnTransitions)
+			if(std::get<0>(transition.first) == from && (std::get<1>(transition.first).is<string::Epsilon>() || std::get<1>(transition.first) == input) && std::get<2>(transition.first) == pop)
+				throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+		for(const auto& transition : localTransitions)
+			if(transition.first.first == from && (transition.first.second.is<string::Epsilon>() || transition.first.second == input))
+				throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+	}
+
+	returnTransitions.insert(std::make_pair(key, to));
+	return true;
+}
+
+bool RealTimeHeightDeterministicDPDA::addReturnTransition(const State& from, const alphabet::Symbol& pop, const State& to) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(string::Epsilon::EPSILON);
+	return addReturnTransition(from, inputVariant, pop, to);
+}
+
+bool RealTimeHeightDeterministicDPDA::addReturnTransition(const State& from, const alphabet::Symbol& input, const alphabet::Symbol& pop, const State& to) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(input);
+	return addReturnTransition(from, inputVariant, pop, to);
+}
+
+bool RealTimeHeightDeterministicDPDA::addLocalTransition(const State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const State& to) {
+	if (states.find(from) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) from.getName() + "\" doesn't exist.");
+	}
+
+	if (input.is<alphabet::Symbol>() && inputAlphabet.find(input.get<alphabet::Symbol>()) == inputAlphabet.end()) {
+		throw AutomatonException("Input symbol \"" + (std::string) input.get<alphabet::Symbol>() + "\" doesn't exist.");
+	}
+
+	if (states.find(to) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) to.getName() + "\" doesn't exist.");
+	}
+
+	std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>> key(from, input);
+	
+	if(localTransitions.find(key) != localTransitions.end() && localTransitions.find(key)->second == to)
+		return false;
+
+	if(input.is<string::Epsilon>()) {
+		for(const auto& transition : callTransitions)
+			if(transition.first.first == from )
+				throw AutomatonException("Can't add epsilon transition from state \"" + (std::string) from + "\" when other transitions are present.");
+
+		for(const auto& transition : returnTransitions)
+			if(std::get<0>(transition.first) == from)
+				throw AutomatonException("Can't add epsilon transition from state \"" + (std::string) from + "\" when other transitions are present.");
+
+		for(const auto& transition : localTransitions)
+			if(transition.first.first == from)
+				throw AutomatonException("Can't add epsilon transition from state \"" + (std::string) from + "\" when other transitions are present.");
+	} else {
+		for(const auto& transition : callTransitions)
+			if(transition.first.first == from && (transition.first.second.is<string::Epsilon>() || transition.first.second == input))
+				throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+		for(const auto& transition : returnTransitions)
+			if(std::get<0>(transition.first) == from && (std::get<1>(transition.first).is<string::Epsilon>() || std::get<1>(transition.first) == input))
+				throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+		for(const auto& transition : localTransitions)
+			if(transition.first.first == from && (transition.first.second.is<string::Epsilon>() || transition.first.second == input))
+				throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+	}
+
+	localTransitions.insert(std::make_pair(key, to));
+	return true;
+}
+
+bool RealTimeHeightDeterministicDPDA::addLocalTransition(const State& from, const State& to) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(string::Epsilon::EPSILON);
+	return addLocalTransition(from, inputVariant, to);
+}
+
+bool RealTimeHeightDeterministicDPDA::addLocalTransition(const State& from, const alphabet::Symbol& input, const State& to) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(input);
+	return addLocalTransition(from, inputVariant, to);
+}
+
+bool RealTimeHeightDeterministicDPDA::removeCallTransition(const State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const State& to, const alphabet::Symbol& push) {
+	std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>> key(from, input);
+	std::pair<automaton::State, alphabet::Symbol> value = std::make_pair(to, push);
+
+	if (callTransitions.find(key) == callTransitions.end())
+		return false;
+
+	if(callTransitions.find(key)->second != value)
+		throw AutomatonException(
+				"Transition (\"" + (std::string) from.getName() + "\", \"" + (std::string) input
+						+ "\") -> \"" + (std::string) to.getName() + "\" doesn't exist.");
+
+	callTransitions.erase(key);
+	return true;
+}
+
+bool RealTimeHeightDeterministicDPDA::removeCallTransition(const State& from, const State& to, const alphabet::Symbol& push) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(string::Epsilon::EPSILON);
+	return removeCallTransition(from, inputVariant, to, push);
+}
+
+bool RealTimeHeightDeterministicDPDA::removeCallTransition(const State& from, const alphabet::Symbol& input, const State& to, const alphabet::Symbol& push) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(input);
+	return removeCallTransition(from, inputVariant, to, push);
+}
+
+bool RealTimeHeightDeterministicDPDA::removeReturnTransition(const State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const alphabet::Symbol& pop, const State& to) {
+	std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol> key(from, input, pop);
+
+	if (returnTransitions.find(key) == returnTransitions.end())
+		return false;
+
+	if(returnTransitions.find(key)->second != to)
+		throw AutomatonException(
+				"Transition (\"" + (std::string) from.getName() + "\", \"" + (std::string) input
+						+ "\") -> \"" + (std::string) to.getName() + "\" doesn't exist.");
+
+	returnTransitions.erase(key);
+	return true;
+}
+
+bool RealTimeHeightDeterministicDPDA::removeReturnTransition(const State& from, const alphabet::Symbol& pop, const State& to) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(string::Epsilon::EPSILON);
+	return removeReturnTransition(from, inputVariant, pop, to);
+}
+
+bool RealTimeHeightDeterministicDPDA::removeReturnTransition(const State& from, const alphabet::Symbol& input, const alphabet::Symbol& pop, const State& to) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(input);
+	return removeReturnTransition(from, inputVariant, pop, to);
+}
+
+bool RealTimeHeightDeterministicDPDA::removeLocalTransition(const State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const State& to) {
+	std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>> key(from, input);
+
+	if (localTransitions.find(key) == localTransitions.end())
+		return false;
+
+	if(localTransitions.find(key)->second != to)
+		throw AutomatonException(
+				"Transition (\"" + (std::string) from.getName() + "\", \"" + (std::string) input
+						+ "\") -> \"" + (std::string) to.getName() + "\" doesn't exist.");
+
+	localTransitions.erase(key);
+	return true;
+}
+
+bool RealTimeHeightDeterministicDPDA::removeLocalTransition(const State& from, const State& to) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(string::Epsilon::EPSILON);
+	return removeLocalTransition(from, inputVariant, to);
+}
+
+bool RealTimeHeightDeterministicDPDA::removeLocalTransition(const State& from, const alphabet::Symbol& input, const State& to) {
+	std::variant<string::Epsilon, alphabet::Symbol> inputVariant(input);
+	return removeLocalTransition(from, inputVariant, to);
+}
+
+const std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> >& RealTimeHeightDeterministicDPDA::getCallTransitions() const {
+		return callTransitions;
+}
+
+const std::map<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State>& RealTimeHeightDeterministicDPDA::getReturnTransitions() const {
+		return returnTransitions;
+}
+
+const std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, State>& RealTimeHeightDeterministicDPDA::getLocalTransitions() const {
+		return localTransitions;
+}
+
+bool RealTimeHeightDeterministicDPDA::operator==(const ObjectBase& other) const {
+	return other == *this;
+}
+
+bool RealTimeHeightDeterministicDPDA::operator<(const ObjectBase& other) const {
+	return other > *this;
+}
+
+bool RealTimeHeightDeterministicDPDA::operator>(const ObjectBase& other) const {
+	return other < *this;
+}
+
+bool RealTimeHeightDeterministicDPDA::operator==(const RealTimeHeightDeterministicDPDA& other) const {
+	return this->states == other.states && this->inputAlphabet == other.inputAlphabet && this->initialState == other.initialState && this->finalStates == other.finalStates && this->stackAlphabet == other.stackAlphabet && this->bottomOfTheStackSymbol == other.bottomOfTheStackSymbol && this->callTransitions == other.callTransitions && this->returnTransitions == other.returnTransitions && this->localTransitions == other.localTransitions;
+}
+
+bool RealTimeHeightDeterministicDPDA::operator<(const RealTimeHeightDeterministicDPDA& other) const {
+	return std::tie(states, inputAlphabet, initialState, finalStates, stackAlphabet, bottomOfTheStackSymbol, callTransitions, returnTransitions, localTransitions) < std::tie(other.states, other.inputAlphabet, other.initialState, other.finalStates, other.stackAlphabet, other.bottomOfTheStackSymbol, other.callTransitions, other.returnTransitions, other.localTransitions);
+}
+
+void RealTimeHeightDeterministicDPDA::operator>>(std::ostream& out) const {
+	out << "(RealTimeHeightDeterministicDPDA"
+		<< "states = " << states
+		<< "inputAlphabet = " << inputAlphabet
+		<< "initialState = " << initialState
+		<< "finalStates = " << finalStates
+		<< "stackAlphabet = " << stackAlphabet
+		<< "bottomOfTheStackSymbol = " << bottomOfTheStackSymbol
+		<< "callTransitions = " << callTransitions
+		<< "returnTransitions = " << returnTransitions
+		<< "localTransitions = " << localTransitions
+		<< ")";
+}
+
+RealTimeHeightDeterministicDPDA::operator std::string () const {
+	std::stringstream ss;
+	ss << *this;
+	return ss.str();
+}
+
+} /* namespace automaton */
diff --git a/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.h b/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.h
new file mode 100644
index 0000000000..d6eda02718
--- /dev/null
+++ b/alib2data/src/automaton/PDA/RealTimeHeightDeterministicDPDA.h
@@ -0,0 +1,139 @@
+/*
+ * REAL_TIME_HEIGHT_DETERMINISTIC_DPDA.h
+ *
+ *  Created on: Mar 25, 2013
+ *      Author: Jan Travnicek
+ */
+
+#ifndef REAL_TIME_HEIGHT_DETERMINISTIC_DPDA_H_
+#define REAL_TIME_HEIGHT_DETERMINISTIC_DPDA_H_
+
+#include <map>
+#include <vector>
+#include "../../std/map.hpp"
+#include "../../std/variant.hpp"
+#include "../AutomatonBase.h"
+#include "../common/SingleInitialState.h"
+#include "../common/InputAlphabet.h"
+#include "../common/BottomOfTheStackSymbolPushdownStoreAlphabet.h"
+#include "../../alphabet/Symbol.h"
+#include "../../string/Epsilon.h"
+
+namespace automaton {
+
+/**
+ * Represents Finite Automaton.
+ * Can store nondeterministic finite automaton without epsilon transitions.
+ */
+class RealTimeHeightDeterministicDPDA : public std::acceptor<RealTimeHeightDeterministicDPDA, VisitableAutomatonBase, std::acceptor<RealTimeHeightDeterministicDPDA, alib::VisitableObjectBase, AutomatonBase> >, public InputAlphabet, public SingleInitialState, public BottomOfTheStackSymbolPushdownStoreAlphabet {
+protected:
+	std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> > callTransitions;
+	std::map<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State> returnTransitions;
+	std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, State> localTransitions;
+public:
+	explicit RealTimeHeightDeterministicDPDA(const State& initialState, const alphabet::Symbol& bottomOfTheStackSymbol);
+
+	virtual AutomatonBase* clone() const;
+	
+	virtual AutomatonBase* plunder() &&;
+
+	/**
+	 * @copydoc Automaton::removeState(const State&)
+	 */
+	virtual bool removeState(const State& state);
+
+	/**
+	 * @copydoc Automaton::removeInputSymbol(const Symbol&)
+	 */
+	virtual bool removeInputSymbol(const alphabet::Symbol& symbol);
+
+	/*
+	 * @copydoc Automaton::removeStackSymbol(const Symbol&)
+	 */
+	virtual bool removeStackSymbol(const alphabet::Symbol& symbol);
+
+	/**
+	 * Adds call transition defined by parameters to the automaton.
+	 * @param current current state
+	 * @param input input symbol
+	 * @param next next state
+	 * @throws AutomatonException when transition already exists or when transition contains state or symbol not present in the automaton
+	 */
+	bool addCallTransition(const State& current, const std::variant<string::Epsilon, alphabet::Symbol>& input, const State& next, const alphabet::Symbol& push);
+	bool addCallTransition(const State& current, const State& next, const alphabet::Symbol& push);
+	bool addCallTransition(const State& current, const alphabet::Symbol& input, const State& next, const alphabet::Symbol& push);
+
+	/**
+	 * Adds return transition defined by parameters to the automaton.
+	 * @param current current state
+	 * @param input input symbol
+	 * @param next next state
+	 * @throws AutomatonException when transition already exists or when transition contains state or symbol not present in the automaton
+	 */
+	bool addReturnTransition(const State& current, const std::variant<string::Epsilon, alphabet::Symbol>& input, const alphabet::Symbol& pop, const State& next);
+	bool addReturnTransition(const State& current, const alphabet::Symbol& pop, const State& next);
+	bool addReturnTransition(const State& current, const alphabet::Symbol& input, const alphabet::Symbol& pop, const State& next);
+
+	/**
+	 * Adds local transition defined by parameters to the automaton.
+	 * @param current current state
+	 * @param input input symbol
+	 * @param next next state
+	 * @throws AutomatonException when transition already exists or when transition contains state or symbol not present in the automaton
+	 */
+	bool addLocalTransition(const State& current, const std::variant<string::Epsilon, alphabet::Symbol>& input, const State& next);
+	bool addLocalTransition(const State& current, const State& next);
+	bool addLocalTransition(const State& current, const alphabet::Symbol& input, const State& next);
+
+	/**
+	 * Removes call transition from the automaton.
+	 * @param transition transition to remove
+	 * @throws AutomatonException when transition doesn't exists.
+	 */
+	bool removeCallTransition(const State& current, const std::variant<string::Epsilon, alphabet::Symbol>& input, const State& next, const alphabet::Symbol& push);
+	bool removeCallTransition(const State& current, const State& next, const alphabet::Symbol& push);
+	bool removeCallTransition(const State& current, const alphabet::Symbol& input, const State& next, const alphabet::Symbol& push);
+
+	/**
+	 * Removes return transition from the automaton.
+	 * @param transition transition to remove
+	 * @throws AutomatonException when transition doesn't exists.
+	 */
+	bool removeReturnTransition(const State& current, const std::variant<string::Epsilon, alphabet::Symbol>& input, const alphabet::Symbol& pop, const State& next);
+	bool removeReturnTransition(const State& current, const alphabet::Symbol& pop, const State& next);
+	bool removeReturnTransition(const State& current, const alphabet::Symbol& input, const alphabet::Symbol& pop, const State& next);
+
+	/**
+	 * Removes transition local from the automaton.
+	 * @param transition transition to remove
+	 * @throws AutomatonException when transition doesn't exists.
+	 */
+	bool removeLocalTransition(const State& current, const std::variant<string::Epsilon, alphabet::Symbol>& input, const State& next);
+	bool removeLocalTransition(const State& current, const State& next);
+	bool removeLocalTransition(const State& current, const alphabet::Symbol& input, const State& next);
+
+	const std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, std::pair<State, alphabet::Symbol> >& getCallTransitions() const;
+
+	const std::map<std::tuple<State, std::variant<string::Epsilon, alphabet::Symbol>, alphabet::Symbol>, State>& getReturnTransitions() const;
+
+	const std::map<std::pair<State, std::variant<string::Epsilon, alphabet::Symbol>>, State>& getLocalTransitions() const;
+
+	virtual bool operator<(const alib::ObjectBase& other) const;
+	virtual bool operator==(const alib::ObjectBase& other) const;
+	virtual bool operator>(const alib::ObjectBase& other) const;
+
+	virtual bool operator==(const RealTimeHeightDeterministicDPDA& other) const;
+	virtual bool operator<(const RealTimeHeightDeterministicDPDA& other) const;
+
+	virtual void operator>>(std::ostream& os) const;
+
+	virtual operator std::string() const;
+
+	virtual int selfTypeId() const {
+		return typeId(*this);
+	}
+};
+
+} /* namespace automaton */
+
+#endif /* REAL_TIME_HEIGHT_DETERMINISTIC_DPDA_H_ */
diff --git a/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.cpp b/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.cpp
new file mode 100644
index 0000000000..40fd741337
--- /dev/null
+++ b/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.cpp
@@ -0,0 +1,309 @@
+/*
+ * VisiblyPushdownDPDA.cpp
+ *
+ *  Created on: Apr 10, 2013
+ *      Author: Jan Travnicek
+ */
+
+#include "VisiblyPushdownDPDA.h"
+#include "../../std/map.hpp"
+#include "../AutomatonException.h"
+#include <algorithm>
+#include <sstream>
+
+namespace automaton {
+
+VisiblyPushdownDPDA::VisiblyPushdownDPDA(const State& initialState, const alphabet::Symbol& bottomOfTheStackSymbol) : SingleInitialState(initialState), BottomOfTheStackSymbolPushdownStoreAlphabet(bottomOfTheStackSymbol) {
+
+}
+
+AutomatonBase* VisiblyPushdownDPDA::clone() const {
+	return new VisiblyPushdownDPDA(*this);
+}
+
+AutomatonBase* VisiblyPushdownDPDA::plunder() && {
+	return new VisiblyPushdownDPDA(std::move(*this));
+}
+
+bool VisiblyPushdownDPDA::removeState(const State& state) {
+	if (initialState == state) {
+		throw AutomatonException("State \"" + (std::string) state.getName() + "\" is initial state.");
+	}
+
+	if (finalStates.find(state) != finalStates.end()) {
+		throw AutomatonException("State \"" + (std::string) state.getName() + "\" is final state.");
+	}
+
+	for (const std::pair<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> >& callTransition : callTransitions) {
+		if (state == callTransition.first.first)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+		if(callTransition.second.first == state)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::tuple<State, alphabet::Symbol, alphabet::Symbol>, State>& returnTransition : returnTransitions) {
+		if (state == std::get<0>(returnTransition.first))
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+		if(returnTransition.second == state)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::pair<State, alphabet::Symbol>, State>& localTransition : localTransitions) {
+		if (state == localTransition.first.first)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+		if(localTransition.second == state)
+			throw AutomatonException("State \"" + (std::string) state.getName() + "\" is used in transition.");
+	}
+
+	return states.erase(state);
+}
+
+bool VisiblyPushdownDPDA::removeInputSymbol(const alphabet::Symbol& symbol) {
+	for (const std::pair<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> >& callTransition : callTransitions) {
+		if (symbol == callTransition.first.second)
+			throw AutomatonException("Input symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::tuple<State, alphabet::Symbol, alphabet::Symbol>, State>& returnTransition : returnTransitions) {
+		if (symbol == std::get<1>(returnTransition.first))
+			throw AutomatonException("Input symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::pair<State, alphabet::Symbol>, State>& localTransition : localTransitions) {
+		if (symbol == localTransition.first.second)
+			throw AutomatonException("Input symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	return callInputAlphabet.erase(symbol) || returnInputAlphabet.erase(symbol) || localInputAlphabet.erase(symbol);
+}
+
+bool VisiblyPushdownDPDA::removeStackSymbol(const alphabet::Symbol& symbol) {
+	for (const std::pair<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> >& callTransition : callTransitions) {
+		if (symbol == callTransition.second.second)
+			throw AutomatonException("Stack symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	for (const std::pair<std::tuple<State, alphabet::Symbol, alphabet::Symbol>, State>& returnTransition : returnTransitions) {
+		if (symbol == std::get<2>(returnTransition.first))
+			throw AutomatonException("Stack symbol \"" + (std::string) symbol + "\" is used in transition.");
+	}
+
+	if(bottomOfTheStackSymbol == symbol) {
+		throw AutomatonException("Stack symbol \"" + (std::string) symbol + "\" is start symbol.");
+	}
+
+	return stackAlphabet.erase(symbol);
+}
+
+bool VisiblyPushdownDPDA::addCallTransition(const State& from, const alphabet::Symbol& input, const State& to, const alphabet::Symbol& push) {
+	if (states.find(from) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) from.getName() + "\" doesn't exist.");
+	}
+
+	if (callInputAlphabet.find(input) == callInputAlphabet.end()) {
+		throw AutomatonException("Input symbol \"" + (std::string) input + "\" doesn't exist.");
+	}
+
+	if (states.find(to) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) to.getName() + "\" doesn't exist.");
+	}
+
+	if (stackAlphabet.find(push) == stackAlphabet.end()) {
+		throw AutomatonException("Stack symbol \"" + (std::string) push + "\" doesn't exist.");
+	}
+
+	std::pair<State, alphabet::Symbol> key(from, input);
+	std::pair<automaton::State, alphabet::Symbol> value = std::make_pair(to, push);
+
+	if(callTransitions.find(key) != callTransitions.end() && callTransitions.find(key)->second == value)
+		return false;
+
+	for(const auto& transition : callTransitions)
+		if(transition.first.first == from && transition.first.second == input)
+			throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+	for(const auto& transition : returnTransitions)
+		if(std::get<0>(transition.first) == from && std::get<1>(transition.first) == input)
+			throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+	for(const auto& transition : localTransitions)
+		if(transition.first.first == from && transition.first.second == input)
+			throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+	callTransitions.insert(std::make_pair(key, value));
+	return true;
+}
+
+bool VisiblyPushdownDPDA::addReturnTransition(const State& from, const alphabet::Symbol& input, const alphabet::Symbol& pop, const State& to) {
+	if (states.find(from) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) from.getName() + "\" doesn't exist.");
+	}
+
+	if (returnInputAlphabet.find(input) == returnInputAlphabet.end()) {
+		throw AutomatonException("Input symbol \"" + (std::string) input + "\" doesn't exist.");
+	}
+
+	if (states.find(to) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) to.getName() + "\" doesn't exist.");
+	}
+
+	if (stackAlphabet.find(pop) == stackAlphabet.end()) {
+		throw AutomatonException("Stack symbol \"" + (std::string) pop + "\" doesn't exist.");
+	}
+
+	std::tuple<State, alphabet::Symbol, alphabet::Symbol> key(from, input, pop);
+
+	if(returnTransitions.find(key) != returnTransitions.end() && returnTransitions.find(key)->second == to)
+		return false;
+
+	for(const auto& transition : callTransitions)
+		if(transition.first.first == from && transition.first.second == input)
+			throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+	for(const auto& transition : returnTransitions)
+		if(std::get<0>(transition.first) == from && std::get<1>(transition.first) == input && std::get<2>(transition.first) == pop)
+			throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+	for(const auto& transition : localTransitions)
+		if(transition.first.first == from && transition.first.second == input)
+			throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+	returnTransitions.insert(std::make_pair(key, to));
+	return true;
+}
+
+bool VisiblyPushdownDPDA::addLocalTransition(const State& from, const alphabet::Symbol& input, const State& to) {
+	if (states.find(from) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) from.getName() + "\" doesn't exist.");
+	}
+
+	if (localInputAlphabet.find(input) == localInputAlphabet.end()) {
+		throw AutomatonException("Input symbol \"" + (std::string) input + "\" doesn't exist.");
+	}
+
+	if (states.find(to) == states.end()) {
+		throw AutomatonException("State \"" + (std::string) to.getName() + "\" doesn't exist.");
+	}
+
+	std::pair<State, alphabet::Symbol> key(from, input);
+	
+	if(localTransitions.find(key) != localTransitions.end() && localTransitions.find(key)->second == to)
+		return false;
+
+	for(const auto& transition : callTransitions)
+		if(transition.first.first == from && transition.first.second == input)
+			throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+	for(const auto& transition : returnTransitions)
+		if(std::get<0>(transition.first) == from && std::get<1>(transition.first) == input)
+			throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+	for(const auto& transition : localTransitions)
+		if(transition.first.first == from && transition.first.second == input)
+			throw AutomatonException("Can't add transition from state \"" + (std::string) from + "\" when transition reading \"" + (std::string) input + "\" is present.");
+
+	localTransitions.insert(std::make_pair(key, to));
+	return true;
+}
+
+bool VisiblyPushdownDPDA::removeCallTransition(const State& from, const alphabet::Symbol& input, const State& to, const alphabet::Symbol& push) {
+	std::pair<State, alphabet::Symbol> key(from, input);
+	std::pair<automaton::State, alphabet::Symbol> value = std::make_pair(to, push);
+	
+	if (callTransitions.find(key) == callTransitions.end())
+		return false;
+
+	if(callTransitions.find(key)->second != value)
+		throw AutomatonException(
+				"Transition (\"" + (std::string) from.getName() + "\", \"" + (std::string) input
+						+ "\") -> \"" + (std::string) to.getName() + "\" doesn't exist.");
+
+	callTransitions.erase(key);
+	return true;
+}
+
+bool VisiblyPushdownDPDA::removeReturnTransition(const State& from, const alphabet::Symbol& input, const alphabet::Symbol& pop, const State& to) {
+	std::tuple<State, alphabet::Symbol, alphabet::Symbol> key(from, input, pop);
+
+	if (returnTransitions.find(key) == returnTransitions.end())
+		return false;
+
+	if(returnTransitions.find(key)->second != to)
+		throw AutomatonException(
+				"Transition (\"" + (std::string) from.getName() + "\", \"" + (std::string) input
+						+ "\") -> \"" + (std::string) to.getName() + "\" doesn't exist.");
+
+	returnTransitions.erase(key);
+	return true;
+}
+
+bool VisiblyPushdownDPDA::removeLocalTransition(const State& from, const alphabet::Symbol& input, const State& to) {
+	std::pair<State, alphabet::Symbol> key(from, input);
+
+	if (localTransitions.find(key) == localTransitions.end())
+		return false;
+
+	if(localTransitions.find(key)->second != to)
+		throw AutomatonException(
+				"Transition (\"" + (std::string) from.getName() + "\", \"" + (std::string) input
+						+ "\") -> \"" + (std::string) to.getName() + "\" doesn't exist.");
+
+	localTransitions.erase(key);
+	return true;
+}
+
+const std::map<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> >& VisiblyPushdownDPDA::getCallTransitions() const {
+		return callTransitions;
+}
+
+const std::map<std::tuple<State, alphabet::Symbol, alphabet::Symbol>, State>& VisiblyPushdownDPDA::getReturnTransitions() const {
+		return returnTransitions;
+}
+
+const std::map<std::pair<State, alphabet::Symbol>, State>& VisiblyPushdownDPDA::getLocalTransitions() const {
+		return localTransitions;
+}
+
+bool VisiblyPushdownDPDA::operator==(const ObjectBase& other) const {
+	return other == *this;
+}
+
+bool VisiblyPushdownDPDA::operator<(const ObjectBase& other) const {
+	return other > *this;
+}
+
+bool VisiblyPushdownDPDA::operator>(const ObjectBase& other) const {
+	return other < *this;
+}
+
+bool VisiblyPushdownDPDA::operator==(const VisiblyPushdownDPDA& other) const {
+	return this->states == other.states && this->callInputAlphabet == other.callInputAlphabet && this->returnInputAlphabet == other.returnInputAlphabet && this->localInputAlphabet == other.localInputAlphabet && this->initialState == other.initialState && this->finalStates == other.finalStates && this->stackAlphabet == other.stackAlphabet && this->bottomOfTheStackSymbol == other.bottomOfTheStackSymbol && this->callTransitions == other.callTransitions && this->returnTransitions == other.returnTransitions && this->localTransitions == other.localTransitions;
+}
+
+bool VisiblyPushdownDPDA::operator<(const VisiblyPushdownDPDA& other) const {
+	return std::tie(states, callInputAlphabet, returnInputAlphabet, localInputAlphabet, initialState, finalStates, stackAlphabet, bottomOfTheStackSymbol, callTransitions, returnTransitions, localTransitions) < std::tie(other.states, other.callInputAlphabet, other.returnInputAlphabet, other.localInputAlphabet, other.initialState, other.finalStates, other.stackAlphabet, other.bottomOfTheStackSymbol, other.callTransitions, other.returnTransitions, other.localTransitions);
+}
+
+void VisiblyPushdownDPDA::operator>>(std::ostream& out) const {
+	out << "(VisiblyPushdownDPDA"
+		<< "states = " << states
+		<< "callInputAlphabet = " << callInputAlphabet
+		<< "returnInputAlphabet = " << returnInputAlphabet
+		<< "localInputAlphabet = " << localInputAlphabet
+		<< "initialState = " << initialState
+		<< "finalStates = " << finalStates
+		<< "stackAlphabet = " << stackAlphabet
+		<< "bottomOfTheStackSymbol = " << bottomOfTheStackSymbol
+		<< "callTransitions = " << callTransitions
+		<< "returnTransitions = " << returnTransitions
+		<< "localTransitions = " << localTransitions
+		<< ")";
+}
+
+VisiblyPushdownDPDA::operator std::string () const {
+	std::stringstream ss;
+	ss << *this;
+	return ss.str();
+}
+
+} /* namespace automaton */
diff --git a/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.h b/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.h
new file mode 100644
index 0000000000..b4d21594df
--- /dev/null
+++ b/alib2data/src/automaton/PDA/VisiblyPushdownDPDA.h
@@ -0,0 +1,125 @@
+/*
+ * VISIBLY_PUSHDOWN_DPDA.h
+ *
+ *  Created on: Mar 25, 2013
+ *      Author: Jan Travnicek
+ */
+
+#ifndef VISIBLY_PUSHDOWN_DPDA_H_
+#define VISIBLY_PUSHDOWN_DPDA_H_
+
+#include <map>
+#include <vector>
+#include "../../std/map.hpp"
+#include "../AutomatonBase.h"
+#include "../common/SingleInitialState.h"
+#include "../common/CallReturnLocalInputAlphabet.h"
+#include "../common/BottomOfTheStackSymbolPushdownStoreAlphabet.h"
+#include "../../alphabet/Symbol.h"
+
+namespace automaton {
+
+/**
+ * Represents Finite Automaton.
+ * Can store nondeterministic finite automaton without epsilon transitions.
+ */
+class VisiblyPushdownDPDA : public std::acceptor<VisiblyPushdownDPDA, VisitableAutomatonBase, std::acceptor<VisiblyPushdownDPDA, alib::VisitableObjectBase, AutomatonBase> >, public CallReturnLocalInputAlphabet, public SingleInitialState, public BottomOfTheStackSymbolPushdownStoreAlphabet {
+protected:
+	std::map<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> > callTransitions;
+	std::map<std::tuple<State, alphabet::Symbol, alphabet::Symbol>, State > returnTransitions;
+	std::map<std::pair<State, alphabet::Symbol>, State > localTransitions;
+public:
+	explicit VisiblyPushdownDPDA(const State& initialSymbol, const alphabet::Symbol& bottomOfTheStackSymbol);
+
+	virtual AutomatonBase* clone() const;
+	
+	virtual AutomatonBase* plunder() &&;
+
+	/**
+	 * @copydoc Automaton::removeState(const State&)
+	 */
+	virtual bool removeState(const State& state);
+
+	/**
+	 * @copydoc Automaton::removeInputSymbol(const Symbol&)
+	 */
+	virtual bool removeInputSymbol(const alphabet::Symbol& symbol);
+
+	/*
+	 * @copydoc Automaton::removeStackSymbol(const Symbol&)
+	 */
+	virtual bool removeStackSymbol(const alphabet::Symbol& symbol);
+
+	/**
+	 * Adds call transition defined by parameters to the automaton.
+	 * @param current current state
+	 * @param input input symbol
+	 * @param next next state
+	 * @throws AutomatonException when transition already exists or when transition contains state or symbol not present in the automaton
+	 */
+	bool addCallTransition(const State& current, const alphabet::Symbol& input, const State& next, const alphabet::Symbol& push);
+
+	/**
+	 * Adds return transition defined by parameters to the automaton.
+	 * @param current current state
+	 * @param input input symbol
+	 * @param next next state
+	 * @throws AutomatonException when transition already exists or when transition contains state or symbol not present in the automaton
+	 */
+	bool addReturnTransition(const State& current, const alphabet::Symbol& input, const alphabet::Symbol& pop, const State& next);
+
+	/**
+	 * Adds local transition defined by parameters to the automaton.
+	 * @param current current state
+	 * @param input input symbol
+	 * @param next next state
+	 * @throws AutomatonException when transition already exists or when transition contains state or symbol not present in the automaton
+	 */
+	bool addLocalTransition(const State& current, const alphabet::Symbol& input, const State& next);
+
+	/**
+	 * Removes call transition from the automaton.
+	 * @param transition transition to remove
+	 * @throws AutomatonException when transition doesn't exists.
+	 */
+	bool removeCallTransition(const State& current, const alphabet::Symbol& input, const State& next, const alphabet::Symbol& push);
+
+	/**
+	 * Removes return transition from the automaton.
+	 * @param transition transition to remove
+	 * @throws AutomatonException when transition doesn't exists.
+	 */
+	bool removeReturnTransition(const State& current, const alphabet::Symbol& input, const alphabet::Symbol& pop, const State& next);
+
+	/**
+	 * Removes transition local from the automaton.
+	 * @param transition transition to remove
+	 * @throws AutomatonException when transition doesn't exists.
+	 */
+	bool removeLocalTransition(const State& current, const alphabet::Symbol& input, const State& next);
+
+	const std::map<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> >& getCallTransitions() const;
+
+	const std::map<std::tuple<State, alphabet::Symbol, alphabet::Symbol>, State>& getReturnTransitions() const;
+
+	const std::map<std::pair<State, alphabet::Symbol>, State>& getLocalTransitions() const;
+
+	virtual bool operator<(const alib::ObjectBase& other) const;
+	virtual bool operator==(const alib::ObjectBase& other) const;
+	virtual bool operator>(const alib::ObjectBase& other) const;
+
+	virtual bool operator==(const VisiblyPushdownDPDA& other) const;
+	virtual bool operator<(const VisiblyPushdownDPDA& other) const;
+
+	virtual void operator>>(std::ostream& os) const;
+
+	virtual operator std::string() const;
+
+	virtual int selfTypeId() const {
+		return typeId(*this);
+	}
+};
+
+} /* namespace automaton */
+
+#endif /* VISIBLY_PUSHDOWN_DPDA_H_ */
diff --git a/alib2data/src/automaton/common/State.cpp b/alib2data/src/automaton/common/State.cpp
index 27a1385879..894899895f 100644
--- a/alib2data/src/automaton/common/State.cpp
+++ b/alib2data/src/automaton/common/State.cpp
@@ -46,4 +46,8 @@ std::ostream& operator<<(std::ostream& out, const State& state) {
 	return out;
 }
 
+State::operator std::string () const {
+	return (std::string) name;
+}
+
 } /* namespace automaton */
diff --git a/alib2data/src/automaton/common/State.h b/alib2data/src/automaton/common/State.h
index 9455390f99..747bdf0711 100644
--- a/alib2data/src/automaton/common/State.h
+++ b/alib2data/src/automaton/common/State.h
@@ -35,6 +35,8 @@ public:
 	bool operator != (const State& other) const;
 
 	friend std::ostream& operator<<(std::ostream&, const State&);
+
+	operator std::string () const;
 };
 
 } /* namespace automaton */
diff --git a/alib2data/src/object/ObjectBase.h b/alib2data/src/object/ObjectBase.h
index 9063b6d5c2..9adfbe563b 100644
--- a/alib2data/src/object/ObjectBase.h
+++ b/alib2data/src/object/ObjectBase.h
@@ -36,7 +36,9 @@ class SinglePopDPDA;
 class NPDA;
 class SinglePopNPDA;
 class InputDrivenNPDA;
+class VisiblyPushdownDPDA;
 class VisiblyPushdownNPDA;
+class RealTimeHeightDeterministicDPDA;
 class RealTimeHeightDeterministicNPDA;
 class OneTapeDTM;
 
@@ -117,7 +119,7 @@ namespace alib {
 typedef std::acceptor_base<
 			Void,
 			exception::AlibException,
-			automaton::UnknownAutomaton, automaton::DFA, automaton::NFA, automaton::EpsilonNFA, automaton::CompactNFA, automaton::ExtendedNFA, automaton::DPDA, automaton::SinglePopDPDA, automaton::InputDrivenNPDA, automaton::VisiblyPushdownNPDA, automaton::RealTimeHeightDeterministicNPDA, automaton::NPDA, automaton::SinglePopNPDA, automaton::OneTapeDTM,
+			automaton::UnknownAutomaton, automaton::DFA, automaton::NFA, automaton::EpsilonNFA, automaton::CompactNFA, automaton::ExtendedNFA, automaton::DPDA, automaton::SinglePopDPDA, automaton::InputDrivenNPDA, automaton::VisiblyPushdownDPDA, automaton::VisiblyPushdownNPDA, automaton::RealTimeHeightDeterministicDPDA, automaton::RealTimeHeightDeterministicNPDA, automaton::NPDA, automaton::SinglePopNPDA, automaton::OneTapeDTM,
 			grammar::UnknownGrammar, grammar::LeftLG, grammar::LeftRG, grammar::RightLG, grammar::RightRG, grammar::LG, grammar::CFG, grammar::EpsilonFreeCFG, grammar::CNF, grammar::GNF, grammar::CSG, grammar::NonContractingGrammar, grammar::ContextPreservingUnrestrictedGrammar, grammar::UnrestrictedGrammar,
 			label::PrimitiveLabel, label::HexavigesimalLabel, label::ObjectLabel, label::LabelSetLabel, label::LabelPairLabel,
 			regexp::UnboundedRegExp, regexp::FormalRegExp,
@@ -132,7 +134,7 @@ class ObjectBase :
 			ObjectBase,
 			Void,
 			exception::AlibException,
-			automaton::UnknownAutomaton, automaton::DFA, automaton::NFA, automaton::EpsilonNFA, automaton::CompactNFA, automaton::ExtendedNFA, automaton::DPDA, automaton::SinglePopDPDA, automaton::InputDrivenNPDA, automaton::VisiblyPushdownNPDA, automaton::RealTimeHeightDeterministicNPDA, automaton::NPDA, automaton::SinglePopNPDA, automaton::OneTapeDTM,
+			automaton::UnknownAutomaton, automaton::DFA, automaton::NFA, automaton::EpsilonNFA, automaton::CompactNFA, automaton::ExtendedNFA, automaton::DPDA, automaton::SinglePopDPDA, automaton::InputDrivenNPDA, automaton::VisiblyPushdownDPDA, automaton::VisiblyPushdownNPDA, automaton::RealTimeHeightDeterministicDPDA, automaton::RealTimeHeightDeterministicNPDA, automaton::NPDA, automaton::SinglePopNPDA, automaton::OneTapeDTM,
 			grammar::UnknownGrammar, grammar::LeftLG, grammar::LeftRG, grammar::RightLG, grammar::RightRG, grammar::LG, grammar::CFG, grammar::EpsilonFreeCFG, grammar::CNF, grammar::GNF, grammar::CSG, grammar::NonContractingGrammar, grammar::ContextPreservingUnrestrictedGrammar, grammar::UnrestrictedGrammar,
 			label::PrimitiveLabel, label::HexavigesimalLabel, label::ObjectLabel, label::LabelSetLabel, label::LabelPairLabel,
 			regexp::UnboundedRegExp, regexp::FormalRegExp,
diff --git a/alib2data/src/std/variant.hpp b/alib2data/src/std/variant.hpp
index d551bd66e8..fc19fc4e4e 100644
--- a/alib2data/src/std/variant.hpp
+++ b/alib2data/src/std/variant.hpp
@@ -76,6 +76,12 @@ struct variant_helper<F, Ts...> {
 			variant_helper<Ts...>::print(out, id, data);
 	}
 
+	inline static std::string string(const size_t id, const void* data) {
+		if (id == typeid(F).hash_code())
+			return (std::string) *reinterpret_cast<const F*>(data);
+		else
+			return variant_helper<Ts...>::string(id, data);
+	}
 
 	inline static bool compareLess(size_t this_t, const void * this_v, size_t other_t, const void * other_v)
 	{
@@ -96,6 +102,7 @@ inline static void copy(size_t, const void *, void *) { }
 inline static void move(size_t, void *, void *) { }
 inline static bool compareEq(size_t, const void *, size_t, const void *) { return true; }
 inline static void print(ostream&, const size_t, const void *) {}
+inline static std::string string(const size_t, const void *) { return ""; }
 inline static bool compareLess(size_t, const void *, size_t, const void *) { return false; }
 };
 
@@ -243,6 +250,10 @@ public:
 		helper_t::print(out, obj.type_id, &obj.data);
 		return out;
 	}
+
+	operator std::string() const {
+		return helper_t::string(this->type_id, &this->data);
+	}
 };
 
 } /* namespace std */
diff --git a/astat2/src/AutomataStat.cpp b/astat2/src/AutomataStat.cpp
index feedb1e678..ffd031a1b6 100644
--- a/astat2/src/AutomataStat.cpp
+++ b/astat2/src/AutomataStat.cpp
@@ -210,10 +210,18 @@ void AutomataStat::Visit(void*, const automaton::InputDrivenNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type InputDrivenNPDA");
 }
 
+void AutomataStat::Visit(void*, const automaton::VisiblyPushdownDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type VisiblyPushdownDPDA");
+}
+
 void AutomataStat::Visit(void*, const automaton::VisiblyPushdownNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type VisiblyPushdownNPDA");
 }
 
+void AutomataStat::Visit(void*, const automaton::RealTimeHeightDeterministicDPDA&) const {
+	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicDPDA");
+}
+
 void AutomataStat::Visit(void*, const automaton::RealTimeHeightDeterministicNPDA&) const {
 	throw exception::AlibException("Unsupported automaton type RealTimeHeightDeterministicNPDA");
 }
diff --git a/astat2/src/AutomataStat.h b/astat2/src/AutomataStat.h
index a532281949..00ce306279 100644
--- a/astat2/src/AutomataStat.h
+++ b/astat2/src/AutomataStat.h
@@ -34,7 +34,9 @@ private:
 	void Visit(void*, const automaton::DPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
 	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
+	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
 	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
+	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
 	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
 	void Visit(void*, const automaton::NPDA& automaton) const;
 	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
-- 
GitLab