From 9433d7fb3a27f00a509fd258baa929c4756c5aba Mon Sep 17 00:00:00 2001
From: Jan Travnicek <Jan.Travnicek@fit.cvut.cz>
Date: Wed, 21 Jan 2015 08:49:42 +0100
Subject: [PATCH] add compare capability to all automata

---
 acompare2/src/AutomatonCompare.cpp | 771 +++++++++++++++++++++++++++--
 acompare2/src/AutomatonCompare.h   |  61 ++-
 acompare2/src/GrammarCompare.cpp   | 101 ++--
 acompare2/src/GrammarCompare.h     |  24 +-
 4 files changed, 843 insertions(+), 114 deletions(-)

diff --git a/acompare2/src/AutomatonCompare.cpp b/acompare2/src/AutomatonCompare.cpp
index 4f2303772c..969f80f041 100644
--- a/acompare2/src/AutomatonCompare.cpp
+++ b/acompare2/src/AutomatonCompare.cpp
@@ -26,7 +26,15 @@
 #include "automaton/FSM/ExtendedNFA.h"
 #include "automaton/FSM/CompactNFA.h"
 #include "automaton/PDA/NPDA.h"
+#include "automaton/PDA/DPDA.h"
+#include "automaton/PDA/InputDrivenNPDA.h"
+#include "automaton/PDA/InputDrivenDPDA.h"
+#include "automaton/PDA/VisiblyPushdownNPDA.h"
+#include "automaton/PDA/VisiblyPushdownDPDA.h"
+#include "automaton/PDA/RealTimeHeightDeterministicNPDA.h"
+#include "automaton/PDA/RealTimeHeightDeterministicDPDA.h"
 #include "automaton/PDA/SinglePopNPDA.h"
+#include "automaton/PDA/SinglePopDPDA.h"
 #include "automaton/TM/OneTapeDTM.h"
 
 #include "exception/AlibException.h"
@@ -79,6 +87,16 @@ bool AutomatonCompare::testCompare(const automaton::CompactNFA& a, const automat
 			a.getTransitions()    == b.getTransitions()    ;
 }
 
+bool AutomatonCompare::testCompare(const automaton::DPDA& a, const automaton::DPDA& b) {
+	return  	a.getFinalStates()    == b.getFinalStates()    &&
+			a.getInitialState()   == b.getInitialState()   &&
+//			a.getInputAlphabet()  == b.getInputAlphabet()  &&
+//			a.getStackAlphabet()  == b.getStackAlphabet()  &&
+			a.getInitialSymbol()  == b.getInitialSymbol()  &&
+			a.getStates()         == b.getStates()         &&
+			a.getTransitions()    == b.getTransitions()    ;
+}
+
 bool AutomatonCompare::testCompare(const automaton::NPDA& a, const automaton::NPDA& b) {
 	return  	a.getFinalStates()    == b.getFinalStates()    &&
 			a.getInitialState()   == b.getInitialState()   &&
@@ -89,6 +107,90 @@ bool AutomatonCompare::testCompare(const automaton::NPDA& a, const automaton::NP
 			a.getTransitions()    == b.getTransitions()    ;
 }
 
+bool AutomatonCompare::testCompare(const automaton::InputDrivenDPDA& a, const automaton::InputDrivenDPDA& b) {
+	return  	a.getFinalStates()             == b.getFinalStates()             &&
+			a.getInitialState()            == b.getInitialState()            &&
+//			a.getInputAlphabet()           == b.getInputAlphabet()           &&
+//			a.getStackAlphabet()           == b.getStackAlphabet()           &&
+			a.getInitialSymbol()           == b.getInitialSymbol()           &&
+			a.getStates()                  == b.getStates()                  &&
+			a.getPushdownStoreOperations() == b.getPushdownStoreOperations() &&
+			a.getTransitions()             == b.getTransitions()             ;
+}
+
+bool AutomatonCompare::testCompare(const automaton::InputDrivenNPDA& a, const automaton::InputDrivenNPDA& b) {
+	return  	a.getFinalStates()             == b.getFinalStates()             &&
+			a.getInitialState()            == b.getInitialState()            &&
+//			a.getInputAlphabet()           == b.getInputAlphabet()           &&
+//			a.getStackAlphabet()           == b.getStackAlphabet()           &&
+			a.getInitialSymbol()           == b.getInitialSymbol()           &&
+			a.getStates()                  == b.getStates()                  &&
+			a.getPushdownStoreOperations() == b.getPushdownStoreOperations() &&
+			a.getTransitions()             == b.getTransitions()             ;
+}
+
+bool AutomatonCompare::testCompare(const automaton::VisiblyPushdownDPDA& a, const automaton::VisiblyPushdownDPDA& b) {
+	return  	a.getFinalStates()            == b.getFinalStates()            &&
+			a.getInitialState()           == b.getInitialState()           &&
+//			a.getCallInputAlphabet()      == b.getCallInputAlphabet()      &&
+//			a.getReturnnputAlphabet()     == b.getReturnInputAlphabet()    &&
+//			a.getLocalInputAlphabet()     == b.getLocalInputAlphabet()     &&
+//			a.getStackAlphabet()          == b.getStackAlphabet()          &&
+			a.getBottomOfTheStackSymbol() == b.getBottomOfTheStackSymbol() &&
+			a.getStates()                 == b.getStates()                 &&
+			a.getCallTransitions()        == b.getCallTransitions()        &&
+			a.getReturnTransitions()      == b.getReturnTransitions()      &&
+			a.getLocalTransitions()       == b.getLocalTransitions()       ;
+}
+
+bool AutomatonCompare::testCompare(const automaton::VisiblyPushdownNPDA& a, const automaton::VisiblyPushdownNPDA& b) {
+	return  	a.getFinalStates()            == b.getFinalStates()            &&
+			a.getInitialStates()          == b.getInitialStates()          &&
+//			a.getCallInputAlphabet()      == b.getCallInputAlphabet()      &&
+//			a.getReturnnputAlphabet()     == b.getReturnInputAlphabet()    &&
+//			a.getLocalInputAlphabet()     == b.getLocalInputAlphabet()     &&
+//			a.getStackAlphabet()          == b.getStackAlphabet()          &&
+			a.getBottomOfTheStackSymbol() == b.getBottomOfTheStackSymbol() &&
+			a.getStates()                 == b.getStates()                 &&
+			a.getCallTransitions()        == b.getCallTransitions()        &&
+			a.getReturnTransitions()      == b.getReturnTransitions()      &&
+			a.getLocalTransitions()       == b.getLocalTransitions()       ;
+}
+
+bool AutomatonCompare::testCompare(const automaton::RealTimeHeightDeterministicDPDA& a, const automaton::RealTimeHeightDeterministicDPDA& b) {
+	return  	a.getFinalStates()            == b.getFinalStates()            &&
+			a.getInitialState()           == b.getInitialState()           &&
+//			a.getInputAlphabet()          == b.getInputAlphabet()          &&
+//			a.getStackAlphabet()          == b.getStackAlphabet()          &&
+			a.getBottomOfTheStackSymbol() == b.getBottomOfTheStackSymbol() &&
+			a.getStates()                 == b.getStates()                 &&
+			a.getCallTransitions()        == b.getCallTransitions()        &&
+			a.getReturnTransitions()      == b.getReturnTransitions()      &&
+			a.getLocalTransitions()       == b.getLocalTransitions()       ;
+}
+
+bool AutomatonCompare::testCompare(const automaton::RealTimeHeightDeterministicNPDA& a, const automaton::RealTimeHeightDeterministicNPDA& b) {
+	return  	a.getFinalStates()            == b.getFinalStates()            &&
+			a.getInitialStates()          == b.getInitialStates()          &&
+//			a.getInputAlphabet()          == b.getInputAlphabet()          &&
+//			a.getStackAlphabet()          == b.getStackAlphabet()          &&
+			a.getBottomOfTheStackSymbol() == b.getBottomOfTheStackSymbol() &&
+			a.getStates()                 == b.getStates()                 &&
+			a.getCallTransitions()        == b.getCallTransitions()        &&
+			a.getReturnTransitions()      == b.getReturnTransitions()      &&
+			a.getLocalTransitions()       == b.getLocalTransitions()       ;
+}
+
+bool AutomatonCompare::testCompare(const automaton::SinglePopDPDA& a, const automaton::SinglePopDPDA& b) {
+	return  	a.getFinalStates()    == b.getFinalStates()    &&
+			a.getInitialState()   == b.getInitialState()   &&
+//			a.getInputAlphabet()  == b.getInputAlphabet()  &&
+//			a.getStackAlphabet()  == b.getStackAlphabet()  &&
+			a.getInitialSymbol()  == b.getInitialSymbol()  &&
+			a.getStates()         == b.getStates()         &&
+			a.getTransitions()    == b.getTransitions()    ;
+}
+
 bool AutomatonCompare::testCompare(const automaton::SinglePopNPDA& a, const automaton::SinglePopNPDA& b) {
 	return  	a.getFinalStates()    == b.getFinalStates()    &&
 			a.getInitialState()   == b.getInitialState()   &&
@@ -158,7 +260,7 @@ template <class T, class R> void AutomatonCompare::mapCompare(const std::map<T,
 }
 
 void AutomatonCompare::printCompare(const automaton::DFA& a, const automaton::DFA& b) {
-	std::cout << "AutomataCompareer" << std::endl;
+	std::cout << "AutomatonCompareer" << std::endl;
 
 	if(a.getFinalStates() != b.getFinalStates()){
 		std::cout << "FinalStates" << std::endl;
@@ -194,7 +296,7 @@ void AutomatonCompare::printCompare(const automaton::DFA& a, const automaton::DF
 }
 
 void AutomatonCompare::printCompare(const automaton::MultiInitialStateNFA& a, const automaton::MultiInitialStateNFA& b) {
-	std::cout << "AutomataCompareer" << std::endl;
+	std::cout << "AutomatonCompareer" << std::endl;
 
 	if(a.getFinalStates() != b.getFinalStates()){
 		std::cout << "FinalStates" << std::endl;
@@ -228,7 +330,7 @@ void AutomatonCompare::printCompare(const automaton::MultiInitialStateNFA& a, co
 }
 
 void AutomatonCompare::printCompare(const automaton::NFA& a, const automaton::NFA& b) {
-	std::cout << "AutomataCompareer" << std::endl;
+	std::cout << "AutomatonCompareer" << std::endl;
 
 	if(a.getFinalStates() != b.getFinalStates()){
 		std::cout << "FinalStates" << std::endl;
@@ -264,7 +366,7 @@ void AutomatonCompare::printCompare(const automaton::NFA& a, const automaton::NF
 }
 
 void AutomatonCompare::printCompare(const automaton::EpsilonNFA& a, const automaton::EpsilonNFA& b) {
-	std::cout << "AutomataCompareer" << std::endl;
+	std::cout << "AutomatonCompareer" << std::endl;
 
 	if(a.getFinalStates() != b.getFinalStates()){
 		std::cout << "FinalStates" << std::endl;
@@ -300,7 +402,7 @@ void AutomatonCompare::printCompare(const automaton::EpsilonNFA& a, const automa
 }
 
 void AutomatonCompare::printCompare(const automaton::ExtendedNFA& a, const automaton::ExtendedNFA& b) {
-	std::cout << "AutomataCompareer" << std::endl;
+	std::cout << "AutomatonCompareer" << std::endl;
 
 	if(a.getFinalStates() != b.getFinalStates()){
 		std::cout << "FinalStates" << std::endl;
@@ -336,7 +438,43 @@ void AutomatonCompare::printCompare(const automaton::ExtendedNFA& a, const autom
 }
 
 void AutomatonCompare::printCompare(const automaton::CompactNFA& a, const automaton::CompactNFA& b) {
-	std::cout << "AutomataCompareer" << std::endl;
+	std::cout << "AutomatonCompareer" << std::endl;
+
+	if(a.getFinalStates() != b.getFinalStates()){
+		std::cout << "FinalStates" << std::endl;
+
+		AutomatonCompare::setCompare(a.getFinalStates(), b.getFinalStates());
+	}
+
+	if(a.getInitialState() != b.getInitialState()) {
+		std::cout << "Initial state" << std::endl;
+
+		std::cout << "< " << a.getInitialState() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialState() << std::endl;
+	}
+
+	if(a.getInputAlphabet() != b.getInputAlphabet()) {
+		std::cout << "InputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getInputAlphabet(), b.getInputAlphabet());
+	}
+
+	if(a.getStates() != b.getStates()) {
+		std::cout << "States" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStates(), b.getStates());
+	}
+
+	if(a.getTransitions() != b.getTransitions()) {
+		std::cout << "Transitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getTransitions(), b.getTransitions());
+	}
+}
+
+void AutomatonCompare::printCompare(const automaton::DPDA& a, const automaton::DPDA& b) {
+	std::cout << "AutomatonCompareer" << std::endl;
 
 	if(a.getFinalStates() != b.getFinalStates()){
 		std::cout << "FinalStates" << std::endl;
@@ -358,6 +496,20 @@ void AutomatonCompare::printCompare(const automaton::CompactNFA& a, const automa
 		AutomatonCompare::setCompare(a.getInputAlphabet(), b.getInputAlphabet());
 	}
 
+	if(a.getStackAlphabet() != b.getStackAlphabet()) {
+		std::cout << "StackAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStackAlphabet(), b.getStackAlphabet());
+	}
+
+	if(a.getInitialSymbol() != b.getInitialSymbol()) {
+		std::cout << "InitialSymbol" << std::endl;
+
+		std::cout << "< " << a.getInitialSymbol() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialSymbol() << std::endl;
+	}
+
 	if(a.getStates() != b.getStates()) {
 		std::cout << "States" << std::endl;
 
@@ -372,7 +524,437 @@ void AutomatonCompare::printCompare(const automaton::CompactNFA& a, const automa
 }
 
 void AutomatonCompare::printCompare(const automaton::NPDA& a, const automaton::NPDA& b) {
-	std::cout << "AutomataCompareer" << std::endl;
+	std::cout << "AutomatonCompareer" << std::endl;
+
+	if(a.getFinalStates() != b.getFinalStates()){
+		std::cout << "FinalStates" << std::endl;
+
+		AutomatonCompare::setCompare(a.getFinalStates(), b.getFinalStates());
+	}
+
+	if(a.getInitialState() != b.getInitialState()) {
+		std::cout << "Initial state" << std::endl;
+
+		std::cout << "< " << a.getInitialState() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialState() << std::endl;
+	}
+
+	if(a.getInputAlphabet() != b.getInputAlphabet()) {
+		std::cout << "InputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getInputAlphabet(), b.getInputAlphabet());
+	}
+
+	if(a.getStackAlphabet() != b.getStackAlphabet()) {
+		std::cout << "StackAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStackAlphabet(), b.getStackAlphabet());
+	}
+
+	if(a.getInitialSymbol() != b.getInitialSymbol()) {
+		std::cout << "InitialSymbol" << std::endl;
+
+		std::cout << "< " << a.getInitialSymbol() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialSymbol() << std::endl;
+	}
+
+	if(a.getStates() != b.getStates()) {
+		std::cout << "States" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStates(), b.getStates());
+	}
+
+	if(a.getTransitions() != b.getTransitions()) {
+		std::cout << "Transitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getTransitions(), b.getTransitions());
+	}
+}
+
+void AutomatonCompare::printCompare(const automaton::InputDrivenDPDA& a, const automaton::InputDrivenDPDA& b) {
+	std::cout << "AutomatonCompareer" << std::endl;
+
+	if(a.getFinalStates() != b.getFinalStates()){
+		std::cout << "FinalStates" << std::endl;
+
+		AutomatonCompare::setCompare(a.getFinalStates(), b.getFinalStates());
+	}
+
+	if(a.getInitialState() != b.getInitialState()) {
+		std::cout << "Initial state" << std::endl;
+
+		std::cout << "< " << a.getInitialState() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialState() << std::endl;
+	}
+
+	if(a.getInputAlphabet() != b.getInputAlphabet()) {
+		std::cout << "InputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getInputAlphabet(), b.getInputAlphabet());
+	}
+
+	if(a.getStackAlphabet() != b.getStackAlphabet()) {
+		std::cout << "StackAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStackAlphabet(), b.getStackAlphabet());
+	}
+
+	if(a.getInitialSymbol() != b.getInitialSymbol()) {
+		std::cout << "InitialSymbol" << std::endl;
+
+		std::cout << "< " << a.getInitialSymbol() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialSymbol() << std::endl;
+	}
+
+	if(a.getStates() != b.getStates()) {
+		std::cout << "States" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStates(), b.getStates());
+	}
+
+	if(a.getPushdownStoreOperations() != b.getPushdownStoreOperations()) {
+		std::cout << "PushdownStoreOperations" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getPushdownStoreOperations(), b.getPushdownStoreOperations());
+	}
+
+	if(a.getTransitions() != b.getTransitions()) {
+		std::cout << "Transitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getTransitions(), b.getTransitions());
+	}
+}
+
+void AutomatonCompare::printCompare(const automaton::InputDrivenNPDA& a, const automaton::InputDrivenNPDA& b) {
+	std::cout << "AutomatonCompareer" << std::endl;
+
+	if(a.getFinalStates() != b.getFinalStates()){
+		std::cout << "FinalStates" << std::endl;
+
+		AutomatonCompare::setCompare(a.getFinalStates(), b.getFinalStates());
+	}
+
+	if(a.getInitialState() != b.getInitialState()) {
+		std::cout << "Initial state" << std::endl;
+
+		std::cout << "< " << a.getInitialState() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialState() << std::endl;
+	}
+
+	if(a.getInputAlphabet() != b.getInputAlphabet()) {
+		std::cout << "InputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getInputAlphabet(), b.getInputAlphabet());
+	}
+
+	if(a.getStackAlphabet() != b.getStackAlphabet()) {
+		std::cout << "StackAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStackAlphabet(), b.getStackAlphabet());
+	}
+
+	if(a.getInitialSymbol() != b.getInitialSymbol()) {
+		std::cout << "InitialSymbol" << std::endl;
+
+		std::cout << "< " << a.getInitialSymbol() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialSymbol() << std::endl;
+	}
+
+	if(a.getStates() != b.getStates()) {
+		std::cout << "States" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStates(), b.getStates());
+	}
+
+	if(a.getPushdownStoreOperations() != b.getPushdownStoreOperations()) {
+		std::cout << "PushdownStoreOperations" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getPushdownStoreOperations(), b.getPushdownStoreOperations());
+	}
+
+	if(a.getTransitions() != b.getTransitions()) {
+		std::cout << "Transitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getTransitions(), b.getTransitions());
+	}
+}
+
+void AutomatonCompare::printCompare(const automaton::VisiblyPushdownDPDA& a, const automaton::VisiblyPushdownDPDA& b) {
+	std::cout << "AutomatonCompareer" << std::endl;
+
+	if(a.getFinalStates() != b.getFinalStates()){
+		std::cout << "FinalStates" << std::endl;
+
+		AutomatonCompare::setCompare(a.getFinalStates(), b.getFinalStates());
+	}
+
+	if(a.getInitialState() != b.getInitialState()) {
+		std::cout << "Initial state" << std::endl;
+
+		std::cout << "< " << a.getInitialState() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialState() << std::endl;
+	}
+
+	if(a.getCallInputAlphabet() != b.getCallInputAlphabet()) {
+		std::cout << "CallInputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getCallInputAlphabet(), b.getCallInputAlphabet());
+	}
+
+	if(a.getReturnInputAlphabet() != b.getReturnInputAlphabet()) {
+		std::cout << "ReturnInputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getReturnInputAlphabet(), b.getReturnInputAlphabet());
+	}
+
+	if(a.getLocalInputAlphabet() != b.getLocalInputAlphabet()) {
+		std::cout << "LocalInputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getLocalInputAlphabet(), b.getLocalInputAlphabet());
+	}
+
+	if(a.getStackAlphabet() != b.getStackAlphabet()) {
+		std::cout << "StackAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStackAlphabet(), b.getStackAlphabet());
+	}
+
+	if(a.getBottomOfTheStackSymbol() != b.getBottomOfTheStackSymbol()) {
+		std::cout << "BottomOfTheStackSymbol" << std::endl;
+
+		std::cout << "< " << a.getBottomOfTheStackSymbol() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getBottomOfTheStackSymbol() << std::endl;
+	}
+
+	if(a.getStates() != b.getStates()) {
+		std::cout << "States" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStates(), b.getStates());
+	}
+
+	if(a.getCallTransitions() != b.getCallTransitions()) {
+		std::cout << "CallTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getCallTransitions(), b.getCallTransitions());
+	}
+
+	if(a.getReturnTransitions() != b.getReturnTransitions()) {
+		std::cout << "ReturnTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getReturnTransitions(), b.getReturnTransitions());
+	}
+
+	if(a.getLocalTransitions() != b.getLocalTransitions()) {
+		std::cout << "LocalTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getLocalTransitions(), b.getLocalTransitions());
+	}
+}
+
+void AutomatonCompare::printCompare(const automaton::VisiblyPushdownNPDA& a, const automaton::VisiblyPushdownNPDA& b) {
+	std::cout << "AutomatonCompareer" << std::endl;
+
+	if(a.getFinalStates() != b.getFinalStates()){
+		std::cout << "FinalStates" << std::endl;
+
+		AutomatonCompare::setCompare(a.getFinalStates(), b.getFinalStates());
+	}
+
+	if(a.getInitialStates() != b.getInitialStates()) {
+		std::cout << "Initial states" << std::endl;
+
+		AutomatonCompare::setCompare(a.getInitialStates(), b.getInitialStates());
+	}
+
+	if(a.getCallInputAlphabet() != b.getCallInputAlphabet()) {
+		std::cout << "CallInputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getCallInputAlphabet(), b.getCallInputAlphabet());
+	}
+
+	if(a.getReturnInputAlphabet() != b.getReturnInputAlphabet()) {
+		std::cout << "ReturnInputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getReturnInputAlphabet(), b.getReturnInputAlphabet());
+	}
+
+	if(a.getLocalInputAlphabet() != b.getLocalInputAlphabet()) {
+		std::cout << "LocalInputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getLocalInputAlphabet(), b.getLocalInputAlphabet());
+	}
+
+	if(a.getStackAlphabet() != b.getStackAlphabet()) {
+		std::cout << "StackAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStackAlphabet(), b.getStackAlphabet());
+	}
+
+	if(a.getBottomOfTheStackSymbol() != b.getBottomOfTheStackSymbol()) {
+		std::cout << "BottomOfTheStackSymbol" << std::endl;
+
+		std::cout << "< " << a.getBottomOfTheStackSymbol() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getBottomOfTheStackSymbol() << std::endl;
+	}
+
+	if(a.getStates() != b.getStates()) {
+		std::cout << "States" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStates(), b.getStates());
+	}
+
+	if(a.getCallTransitions() != b.getCallTransitions()) {
+		std::cout << "CallTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getCallTransitions(), b.getCallTransitions());
+	}
+
+	if(a.getReturnTransitions() != b.getReturnTransitions()) {
+		std::cout << "ReturnTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getReturnTransitions(), b.getReturnTransitions());
+	}
+
+	if(a.getLocalTransitions() != b.getLocalTransitions()) {
+		std::cout << "LocalTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getLocalTransitions(), b.getLocalTransitions());
+	}
+}
+
+void AutomatonCompare::printCompare(const automaton::RealTimeHeightDeterministicDPDA& a, const automaton::RealTimeHeightDeterministicDPDA& b) {
+	std::cout << "AutomatonCompareer" << std::endl;
+
+	if(a.getFinalStates() != b.getFinalStates()){
+		std::cout << "FinalStates" << std::endl;
+
+		AutomatonCompare::setCompare(a.getFinalStates(), b.getFinalStates());
+	}
+
+	if(a.getInitialState() != b.getInitialState()) {
+		std::cout << "Initial state" << std::endl;
+
+		std::cout << "< " << a.getInitialState() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getInitialState() << std::endl;
+	}
+
+	if(a.getInputAlphabet() != b.getInputAlphabet()) {
+		std::cout << "InputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getInputAlphabet(), b.getInputAlphabet());
+	}
+
+	if(a.getStackAlphabet() != b.getStackAlphabet()) {
+		std::cout << "StackAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStackAlphabet(), b.getStackAlphabet());
+	}
+
+	if(a.getBottomOfTheStackSymbol() != b.getBottomOfTheStackSymbol()) {
+		std::cout << "BottomOfTheStackSymbol" << std::endl;
+
+		std::cout << "< " << a.getBottomOfTheStackSymbol() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getBottomOfTheStackSymbol() << std::endl;
+	}
+
+	if(a.getStates() != b.getStates()) {
+		std::cout << "States" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStates(), b.getStates());
+	}
+
+	if(a.getCallTransitions() != b.getCallTransitions()) {
+		std::cout << "CallTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getCallTransitions(), b.getCallTransitions());
+	}
+
+	if(a.getReturnTransitions() != b.getReturnTransitions()) {
+		std::cout << "ReturnTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getReturnTransitions(), b.getReturnTransitions());
+	}
+
+	if(a.getLocalTransitions() != b.getLocalTransitions()) {
+		std::cout << "LocalTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getLocalTransitions(), b.getLocalTransitions());
+	}
+}
+
+void AutomatonCompare::printCompare(const automaton::RealTimeHeightDeterministicNPDA& a, const automaton::RealTimeHeightDeterministicNPDA& b) {
+	std::cout << "AutomatonCompareer" << std::endl;
+
+	if(a.getFinalStates() != b.getFinalStates()){
+		std::cout << "FinalStates" << std::endl;
+
+		AutomatonCompare::setCompare(a.getFinalStates(), b.getFinalStates());
+	}
+
+	if(a.getInitialStates() != b.getInitialStates()) {
+		std::cout << "Initial states" << std::endl;
+
+		AutomatonCompare::setCompare(a.getInitialStates(), b.getInitialStates());
+	}
+
+	if(a.getInputAlphabet() != b.getInputAlphabet()) {
+		std::cout << "InputAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getInputAlphabet(), b.getInputAlphabet());
+	}
+
+	if(a.getStackAlphabet() != b.getStackAlphabet()) {
+		std::cout << "StackAlphabet" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStackAlphabet(), b.getStackAlphabet());
+	}
+
+	if(a.getBottomOfTheStackSymbol() != b.getBottomOfTheStackSymbol()) {
+		std::cout << "BottomOfTheStackSymbol" << std::endl;
+
+		std::cout << "< " << a.getBottomOfTheStackSymbol() << std::endl;
+		std::cout << "---" << std::endl;
+		std::cout << "> " << b.getBottomOfTheStackSymbol() << std::endl;
+	}
+
+	if(a.getStates() != b.getStates()) {
+		std::cout << "States" << std::endl;
+
+		AutomatonCompare::setCompare(a.getStates(), b.getStates());
+	}
+
+	if(a.getCallTransitions() != b.getCallTransitions()) {
+		std::cout << "CallTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getCallTransitions(), b.getCallTransitions());
+	}
+
+	if(a.getReturnTransitions() != b.getReturnTransitions()) {
+		std::cout << "ReturnTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getReturnTransitions(), b.getReturnTransitions());
+	}
+
+	if(a.getLocalTransitions() != b.getLocalTransitions()) {
+		std::cout << "LocalTransitions" << std::endl;
+
+		AutomatonCompare::mapCompare(a.getLocalTransitions(), b.getLocalTransitions());
+	}
+}
+
+void AutomatonCompare::printCompare(const automaton::SinglePopDPDA& a, const automaton::SinglePopDPDA& b) {
+	std::cout << "AutomatonCompareer" << std::endl;
 
 	if(a.getFinalStates() != b.getFinalStates()){
 		std::cout << "FinalStates" << std::endl;
@@ -422,7 +1004,7 @@ void AutomatonCompare::printCompare(const automaton::NPDA& a, const automaton::N
 }
 
 void AutomatonCompare::printCompare(const automaton::SinglePopNPDA& a, const automaton::SinglePopNPDA& b) {
-	std::cout << "AutomataCompareer" << std::endl;
+	std::cout << "AutomatonCompareer" << std::endl;
 
 	if(a.getFinalStates() != b.getFinalStates()){
 		std::cout << "FinalStates" << std::endl;
@@ -472,7 +1054,7 @@ void AutomatonCompare::printCompare(const automaton::SinglePopNPDA& a, const aut
 }
 
 void AutomatonCompare::printCompare(const automaton::OneTapeDTM& a, const automaton::OneTapeDTM& b) {
-	std::cout << "AutomataCompareer" << std::endl;
+	std::cout << "AutomatonCompareer" << std::endl;
 
 	if(a.getBlankSymbol() != b.getBlankSymbol()) {
 		std::cout << "Blank symbol" << std::endl;
@@ -575,6 +1157,15 @@ int AutomatonCompare::compare(const automaton::CompactNFA& a, const automaton::C
 	}
 }
 
+int AutomatonCompare::compare(const automaton::DPDA& a, const automaton::DPDA& b) {
+	if(!AutomatonCompare::testCompare(a, b)) {
+	  AutomatonCompare::printCompare(a, b);
+	  return 1;
+	} else {
+	  return 0;
+	}
+}
+
 int AutomatonCompare::compare(const automaton::NPDA& a, const automaton::NPDA& b) {
 	if(!AutomatonCompare::testCompare(a, b)) {
 	  AutomatonCompare::printCompare(a, b);
@@ -584,7 +1175,7 @@ int AutomatonCompare::compare(const automaton::NPDA& a, const automaton::NPDA& b
 	}
 }
 
-int AutomatonCompare::compare(const automaton::SinglePopNPDA& a, const automaton::SinglePopNPDA& b) {
+int AutomatonCompare::compare(const automaton::InputDrivenDPDA& a, const automaton::InputDrivenDPDA& b) {
 	if(!AutomatonCompare::testCompare(a, b)) {
 	  AutomatonCompare::printCompare(a, b);
 	  return 1;
@@ -593,7 +1184,34 @@ int AutomatonCompare::compare(const automaton::SinglePopNPDA& a, const automaton
 	}
 }
 
-int AutomatonCompare::compare(const automaton::OneTapeDTM& a, const automaton::OneTapeDTM& b) {
+int AutomatonCompare::compare(const automaton::InputDrivenNPDA& a, const automaton::InputDrivenNPDA& b) {
+	if(!AutomatonCompare::testCompare(a, b)) {
+	  AutomatonCompare::printCompare(a, b);
+	  return 1;
+	} else {
+	  return 0;
+	}
+}
+
+int AutomatonCompare::compare(const automaton::VisiblyPushdownDPDA& a, const automaton::VisiblyPushdownDPDA& b) {
+	if(!AutomatonCompare::testCompare(a, b)) {
+	  AutomatonCompare::printCompare(a, b);
+	  return 1;
+	} else {
+	  return 0;
+	}
+}
+
+int AutomatonCompare::compare(const automaton::VisiblyPushdownNPDA& a, const automaton::VisiblyPushdownNPDA& b) {
+	if(!AutomatonCompare::testCompare(a, b)) {
+	  AutomatonCompare::printCompare(a, b);
+	  return 1;
+	} else {
+	  return 0;
+	}
+}
+
+int AutomatonCompare::compare(const automaton::RealTimeHeightDeterministicDPDA& a, const automaton::RealTimeHeightDeterministicDPDA& b) {
 	if(!AutomatonCompare::testCompare(a, b)) {
 	  AutomatonCompare::printCompare(a, b);
 	  return 1;
@@ -602,60 +1220,115 @@ int AutomatonCompare::compare(const automaton::OneTapeDTM& a, const automaton::O
 	}
 }
 
-template<typename T>
-int AutomatonCompare::dynamicCompare(const automaton::Automaton& a, const automaton::Automaton& b) {
-	const T* ap = dynamic_cast<const T*>(&a.getData());
-	const T* bp = dynamic_cast<const T*>(&b.getData());
+int AutomatonCompare::compare(const automaton::RealTimeHeightDeterministicNPDA& a, const automaton::RealTimeHeightDeterministicNPDA& b) {
+	if(!AutomatonCompare::testCompare(a, b)) {
+	  AutomatonCompare::printCompare(a, b);
+	  return 1;
+	} else {
+	  return 0;
+	}
+}
 
-	if(ap && bp) {
-		return compare(*ap, *bp);
-	} else if(ap || bp) {
-		std::cout << "Automata Differ By Type" << std::endl;
-		return 1;
+int AutomatonCompare::compare(const automaton::SinglePopDPDA& a, const automaton::SinglePopDPDA& b) {
+	if(!AutomatonCompare::testCompare(a, b)) {
+	  AutomatonCompare::printCompare(a, b);
+	  return 1;
 	} else {
-		return -1;
+	  return 0;
 	}
+}
 
+int AutomatonCompare::compare(const automaton::SinglePopNPDA& a, const automaton::SinglePopNPDA& b) {
+	if(!AutomatonCompare::testCompare(a, b)) {
+	  AutomatonCompare::printCompare(a, b);
+	  return 1;
+	} else {
+	  return 0;
+	}
+}
+
+int AutomatonCompare::compare(const automaton::OneTapeDTM& a, const automaton::OneTapeDTM& b) {
+	if(!AutomatonCompare::testCompare(a, b)) {
+	  AutomatonCompare::printCompare(a, b);
+	  return 1;
+	} else {
+	  return 0;
+	}
 }
 
 int AutomatonCompare::compare(const automaton::Automaton& a, const automaton::Automaton& b) {
 	int res;
+	Accept((void*) &res, a.getData(), b.getData(), AutomatonCompare::AUTOMATON_COMPARE);
+	return res;
+}
 
-	res = dynamicCompare<automaton::DFA>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void AutomatonCompare::Visit(void* data, const automaton::EpsilonNFA& first, const automaton::EpsilonNFA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
 
-	res = dynamicCompare<automaton::NFA>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void AutomatonCompare::Visit(void* data, const automaton::CompactNFA& first, const automaton::CompactNFA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
 
-	res = dynamicCompare<automaton::MultiInitialStateNFA>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void AutomatonCompare::Visit(void* data, const automaton::DFA& first, const automaton::DFA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
 
-	res = dynamicCompare<automaton::EpsilonNFA>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void AutomatonCompare::Visit(void* data, const automaton::ExtendedNFA& first, const automaton::ExtendedNFA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
 
-	res = dynamicCompare<automaton::ExtendedNFA>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void AutomatonCompare::Visit(void* data, const automaton::MultiInitialStateNFA& first, const automaton::MultiInitialStateNFA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
 
-	res = dynamicCompare<automaton::CompactNFA>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void AutomatonCompare::Visit(void* data, const automaton::NFA& first, const automaton::NFA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
 
-	res = dynamicCompare<automaton::NPDA>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void AutomatonCompare::Visit(void* data, const automaton::DPDA& first, const automaton::DPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
 
-	res = dynamicCompare<automaton::SinglePopNPDA>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void AutomatonCompare::Visit(void* data, const automaton::NPDA& first, const automaton::NPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
 
-	res = dynamicCompare<automaton::OneTapeDTM>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void AutomatonCompare::Visit(void* data, const automaton::InputDrivenDPDA& first, const automaton::InputDrivenDPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
 
-	throw exception::AlibException("Unknown automata type");
+void AutomatonCompare::Visit(void* data, const automaton::InputDrivenNPDA& first, const automaton::InputDrivenNPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
 }
+
+void AutomatonCompare::Visit(void* data, const automaton::RealTimeHeightDeterministicDPDA& first, const automaton::RealTimeHeightDeterministicDPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
+
+void AutomatonCompare::Visit(void* data, const automaton::RealTimeHeightDeterministicNPDA& first, const automaton::RealTimeHeightDeterministicNPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
+
+void AutomatonCompare::Visit(void* data, const automaton::SinglePopNPDA& first, const automaton::SinglePopNPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
+
+void AutomatonCompare::Visit(void* data, const automaton::SinglePopDPDA& first, const automaton::SinglePopDPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
+
+void AutomatonCompare::Visit(void* data, const automaton::VisiblyPushdownDPDA& first, const automaton::VisiblyPushdownDPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
+
+void AutomatonCompare::Visit(void* data, const automaton::VisiblyPushdownNPDA& first, const automaton::VisiblyPushdownNPDA& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
+
+void AutomatonCompare::Visit(void* data, const automaton::OneTapeDTM& first, const automaton::OneTapeDTM& second) const {
+	*((int*) data) = AutomatonCompare::compare(first, second);
+}
+
+const AutomatonCompare AutomatonCompare::AUTOMATON_COMPARE;
+
diff --git a/acompare2/src/AutomatonCompare.h b/acompare2/src/AutomatonCompare.h
index df7b8d0b76..ac97ae0513 100644
--- a/acompare2/src/AutomatonCompare.h
+++ b/acompare2/src/AutomatonCompare.h
@@ -16,7 +16,7 @@
 #include <map>
 #include <utility>
 
-class AutomatonCompare {
+class AutomatonCompare : public automaton::VisitableAutomatonBase::const_same_visitor_type {
 	static bool testCompare(const automaton::DFA& a, const automaton::DFA& b);
 	static void printCompare(const automaton::DFA& a, const automaton::DFA& b);
 
@@ -35,9 +35,33 @@ class AutomatonCompare {
 	static bool testCompare(const automaton::CompactNFA& a, const automaton::CompactNFA& b);
 	static void printCompare(const automaton::CompactNFA& a, const automaton::CompactNFA& b);
 
+	static bool testCompare(const automaton::DPDA& a, const automaton::DPDA& b);
+	static void printCompare(const automaton::DPDA& a, const automaton::DPDA& b);
+
 	static bool testCompare(const automaton::NPDA& a, const automaton::NPDA& b);
 	static void printCompare(const automaton::NPDA& a, const automaton::NPDA& b);
 
+	static bool testCompare(const automaton::InputDrivenDPDA& a, const automaton::InputDrivenDPDA& b);
+	static void printCompare(const automaton::InputDrivenDPDA& a, const automaton::InputDrivenDPDA& b);
+
+	static bool testCompare(const automaton::InputDrivenNPDA& a, const automaton::InputDrivenNPDA& b);
+	static void printCompare(const automaton::InputDrivenNPDA& a, const automaton::InputDrivenNPDA& b);
+
+	static bool testCompare(const automaton::VisiblyPushdownDPDA& a, const automaton::VisiblyPushdownDPDA& b);
+	static void printCompare(const automaton::VisiblyPushdownDPDA& a, const automaton::VisiblyPushdownDPDA& b);
+
+	static bool testCompare(const automaton::VisiblyPushdownNPDA& a, const automaton::VisiblyPushdownNPDA& b);
+	static void printCompare(const automaton::VisiblyPushdownNPDA& a, const automaton::VisiblyPushdownNPDA& b);
+
+	static bool testCompare(const automaton::RealTimeHeightDeterministicDPDA& a, const automaton::RealTimeHeightDeterministicDPDA& b);
+	static void printCompare(const automaton::RealTimeHeightDeterministicDPDA& a, const automaton::RealTimeHeightDeterministicDPDA& b);
+
+	static bool testCompare(const automaton::RealTimeHeightDeterministicNPDA& a, const automaton::RealTimeHeightDeterministicNPDA& b);
+	static void printCompare(const automaton::RealTimeHeightDeterministicNPDA& a, const automaton::RealTimeHeightDeterministicNPDA& b);
+
+	static bool testCompare(const automaton::SinglePopDPDA& a, const automaton::SinglePopDPDA& b);
+	static void printCompare(const automaton::SinglePopDPDA& a, const automaton::SinglePopDPDA& b);
+
 	static bool testCompare(const automaton::SinglePopNPDA& a, const automaton::SinglePopNPDA& b);
 	static void printCompare(const automaton::SinglePopNPDA& a, const automaton::SinglePopNPDA& b);
 
@@ -48,20 +72,49 @@ class AutomatonCompare {
 	template <class T> static void listCompare(const std::list<T> a, const std::list<T> b);
 	template <class T, class R> static void mapCompare(const std::map<T, R> a, const std::map<T, R> b);
 public:
+	void Visit(void* data, const automaton::CompactNFA& first, const automaton::CompactNFA& second) const;
+	void Visit(void* data, const automaton::DFA& first, const automaton::DFA& second) const;
+	void Visit(void* data, const automaton::EpsilonNFA& first, const automaton::EpsilonNFA& second) const;
+	void Visit(void* data, const automaton::ExtendedNFA& first, const automaton::ExtendedNFA& second) const;
+	void Visit(void* data, const automaton::MultiInitialStateNFA& first, const automaton::MultiInitialStateNFA& second) const;
+	void Visit(void* data, const automaton::NFA& first, const automaton::NFA& second) const;
+
+	void Visit(void* data, const automaton::DPDA& first, const automaton::DPDA& second) const;
+	void Visit(void* data, const automaton::NPDA& first, const automaton::NPDA& second) const;
+	void Visit(void* data, const automaton::InputDrivenNPDA& first, const automaton::InputDrivenNPDA& second) const;
+	void Visit(void* data, const automaton::InputDrivenDPDA& first, const automaton::InputDrivenDPDA& second) const;
+	void Visit(void* data, const automaton::RealTimeHeightDeterministicDPDA& first, const automaton::RealTimeHeightDeterministicDPDA& second) const;
+	void Visit(void* data, const automaton::RealTimeHeightDeterministicNPDA& first, const automaton::RealTimeHeightDeterministicNPDA& second) const;
+	void Visit(void* data, const automaton::SinglePopNPDA& first, const automaton::SinglePopNPDA& second) const;
+	void Visit(void* data, const automaton::SinglePopDPDA& first, const automaton::SinglePopDPDA& second) const;
+	void Visit(void* data, const automaton::VisiblyPushdownDPDA& first, const automaton::VisiblyPushdownDPDA& second) const;
+	void Visit(void* data, const automaton::VisiblyPushdownNPDA& first, const automaton::VisiblyPushdownNPDA& second) const;
+
+	void Visit(void* data, const automaton::OneTapeDTM& first, const automaton::OneTapeDTM& second) const;
+
 	static int compare(const automaton::DFA& a, const automaton::DFA& b);
 	static int compare(const automaton::NFA& a, const automaton::NFA& b);
 	static int compare(const automaton::MultiInitialStateNFA& a, const automaton::MultiInitialStateNFA& b);
 	static int compare(const automaton::EpsilonNFA& a, const automaton::EpsilonNFA& b);
 	static int compare(const automaton::ExtendedNFA& a, const automaton::ExtendedNFA& b);
 	static int compare(const automaton::CompactNFA& a, const automaton::CompactNFA& b);
+
+	static int compare(const automaton::DPDA& a, const automaton::DPDA& b);
 	static int compare(const automaton::NPDA& a, const automaton::NPDA& b);
+	static int compare(const automaton::InputDrivenDPDA& a, const automaton::InputDrivenDPDA& b);
+	static int compare(const automaton::InputDrivenNPDA& a, const automaton::InputDrivenNPDA& b);
+	static int compare(const automaton::RealTimeHeightDeterministicDPDA& a, const automaton::RealTimeHeightDeterministicDPDA& b);
+	static int compare(const automaton::RealTimeHeightDeterministicNPDA& a, const automaton::RealTimeHeightDeterministicNPDA& b);
+	static int compare(const automaton::SinglePopDPDA& a, const automaton::SinglePopDPDA& b);
 	static int compare(const automaton::SinglePopNPDA& a, const automaton::SinglePopNPDA& b);
-	static int compare(const automaton::OneTapeDTM& a, const automaton::OneTapeDTM& b);
+	static int compare(const automaton::VisiblyPushdownDPDA& a, const automaton::VisiblyPushdownDPDA& b);
+	static int compare(const automaton::VisiblyPushdownNPDA& a, const automaton::VisiblyPushdownNPDA& b);
 
-	template<typename T>
-	static int dynamicCompare(const automaton::Automaton& a, const automaton::Automaton& b);
+	static int compare(const automaton::OneTapeDTM& a, const automaton::OneTapeDTM& b);
 
 	static int compare(const automaton::Automaton& a, const automaton::Automaton& b);
+
+	static const AutomatonCompare AUTOMATON_COMPARE;
 };
 
 #endif /* AUTOMATON_COMPARE_H_ */
diff --git a/acompare2/src/GrammarCompare.cpp b/acompare2/src/GrammarCompare.cpp
index 9cdd155679..0423fc6ead 100644
--- a/acompare2/src/GrammarCompare.cpp
+++ b/acompare2/src/GrammarCompare.cpp
@@ -680,76 +680,63 @@ int GrammarCompare::compare(const grammar::UnrestrictedGrammar& a, const grammar
 	}
 }
 
-template<typename T>
-int GrammarCompare::dynamicCompare(const grammar::Grammar& a, const grammar::Grammar& b) {
-	const T* ap = dynamic_cast<const T*>(&a.getData());
-	const T* bp = dynamic_cast<const T*>(&b.getData());
-
-	if(ap && bp) {
-		return compare(*ap, *bp);
-	} else if(ap || bp) {
-		std::cout << "Grammars Differ By Type" << std::endl;
-		return 1;
-	} else {
-		return -1;
-	}
-
-}
-
 int GrammarCompare::compare(const grammar::Grammar& a, const grammar::Grammar& b) {
 	int res;
+	Accept((void*) &res, a.getData(), b.getData(), GrammarCompare::GRAMMAR_COMPARE);
+	return res;
+}
 
-	res = dynamicCompare<grammar::LeftLG>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
-
-	res = dynamicCompare<grammar::LeftRG>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::RightRG& first, const grammar::RightRG& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::RightLG>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::LeftRG& first, const grammar::LeftRG& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::RightRG>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::RightLG& first, const grammar::RightLG& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::LG>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::LeftLG& first, const grammar::LeftLG& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::CFG>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::LG& first, const grammar::LG& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::EpsilonFreeCFG>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::CFG& first, const grammar::CFG& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::CNF>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::EpsilonFreeCFG& first, const grammar::EpsilonFreeCFG& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::GNF>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::CNF& first, const grammar::CNF& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::CSG>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::GNF& first, const grammar::GNF& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::NonContractingGrammar>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::CSG& first, const grammar::CSG& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::ContextPreservingUnrestrictedGrammar>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::NonContractingGrammar& first, const grammar::NonContractingGrammar& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	res = dynamicCompare<grammar::UnrestrictedGrammar>(a, b);
-	if(res == 0) return 0;
-	if(res == 1) return 1;
+void GrammarCompare::Visit(void* data, const grammar::ContextPreservingUnrestrictedGrammar& first, const grammar::ContextPreservingUnrestrictedGrammar& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
+}
 
-	throw exception::AlibException("Unknown grammar type");
+void GrammarCompare::Visit(void* data, const grammar::UnrestrictedGrammar& first, const grammar::UnrestrictedGrammar& second) const {
+	*((int*) data) = GrammarCompare::compare(first, second);
 }
+
+const GrammarCompare GrammarCompare::GRAMMAR_COMPARE;
+
diff --git a/acompare2/src/GrammarCompare.h b/acompare2/src/GrammarCompare.h
index aa91c36668..5075b5de74 100644
--- a/acompare2/src/GrammarCompare.h
+++ b/acompare2/src/GrammarCompare.h
@@ -16,7 +16,7 @@
 #include <map>
 #include <utility>
 
-class GrammarCompare {
+class GrammarCompare : public grammar::VisitableGrammarBase::const_same_visitor_type {
 	static bool testCompare(const grammar::LeftLG& a, const grammar::LeftLG& b);
 	static void printCompare(const grammar::LeftLG& a, const grammar::LeftLG& b);
 
@@ -60,6 +60,23 @@ class GrammarCompare {
 	template <class T> static void listCompare(const std::list<T> a, const std::list<T> b);
 	template <class T, class R> static void mapCompare(const std::map<T, R> a, const std::map<T, R> b);
 public:
+	void Visit(void*, const grammar::RightRG& first, const grammar::RightRG& second) const;
+	void Visit(void*, const grammar::LeftRG& first, const grammar::LeftRG& second) const;
+	void Visit(void*, const grammar::RightLG& first, const grammar::RightLG& second) const;
+	void Visit(void*, const grammar::LeftLG& first, const grammar::LeftLG& second) const;
+
+	void Visit(void*, const grammar::LG& first, const grammar::LG& second) const;
+	void Visit(void*, const grammar::CFG& first, const grammar::CFG& second) const;
+	void Visit(void*, const grammar::EpsilonFreeCFG& first, const grammar::EpsilonFreeCFG& second) const;
+	void Visit(void*, const grammar::CNF& first, const grammar::CNF& second) const;
+	void Visit(void*, const grammar::GNF& first, const grammar::GNF& second) const;
+
+	void Visit(void*, const grammar::CSG& first, const grammar::CSG& second) const;
+	void Visit(void*, const grammar::NonContractingGrammar& first, const grammar::NonContractingGrammar& second) const;
+
+	void Visit(void*, const grammar::ContextPreservingUnrestrictedGrammar& first, const grammar::ContextPreservingUnrestrictedGrammar& second) const;
+	void Visit(void*, const grammar::UnrestrictedGrammar& first, const grammar::UnrestrictedGrammar& second) const;
+
 	static int compare(const grammar::LeftLG& a, const grammar::LeftLG& b);
 	static int compare(const grammar::LeftRG& a, const grammar::LeftRG& b);
 	static int compare(const grammar::RightLG& a, const grammar::RightLG& b);
@@ -73,11 +90,10 @@ public:
 	static int compare(const grammar::NonContractingGrammar& a, const grammar::NonContractingGrammar& b);
 	static int compare(const grammar::ContextPreservingUnrestrictedGrammar& a, const grammar::ContextPreservingUnrestrictedGrammar& b);
 	static int compare(const grammar::UnrestrictedGrammar& a, const grammar::UnrestrictedGrammar& b);
-	
-	template<typename T>
-	static int dynamicCompare(const grammar::Grammar& a, const grammar::Grammar& b);
 
 	static int compare(const grammar::Grammar& a, const grammar::Grammar& b);
+
+	static const GrammarCompare GRAMMAR_COMPARE;
 };
 
 #endif /* GRAMMAR_COMPARE_H_ */
-- 
GitLab