From c6e7e327599f51f84c40e284b8b90938573be2b5 Mon Sep 17 00:00:00 2001
From: Jan Travnicek <Jan.Travnicek@fit.cvut.cz>
Date: Thu, 7 Jun 2018 08:08:20 +0200
Subject: [PATCH] template Rename algorithm

---
 alib2algo/src/automaton/simplify/Rename.cpp | 264 +-------------------
 alib2algo/src/automaton/simplify/Rename.h   | 262 ++++++++++++++++++-
 2 files changed, 260 insertions(+), 266 deletions(-)

diff --git a/alib2algo/src/automaton/simplify/Rename.cpp b/alib2algo/src/automaton/simplify/Rename.cpp
index db8b49b0fa..526eb6b901 100644
--- a/alib2algo/src/automaton/simplify/Rename.cpp
+++ b/alib2algo/src/automaton/simplify/Rename.cpp
@@ -6,270 +6,18 @@
  */
 
 #include "Rename.h"
-
-#include <alib/map>
-#include <alib/vector>
-#include <alib/algorithm>
-#include <sstream>
-#include <alib/iostream>
 #include <registration/AlgoRegistration.hpp>
 
 namespace automaton {
 
 namespace simplify {
 
-automaton::DFA<> Rename::rename(const automaton::DFA<>& fsm) {
-	int counter = 0;
-	ext::map<DefaultStateType, int > renamingData;
-
-	for(auto iter = fsm.getStates().begin(); iter != fsm.getStates().end(); iter++) {
-		renamingData.insert(std::make_pair(*iter, counter++));
-	}
-
-	automaton::DFA<> result(DefaultStateType(renamingData.find(fsm.getInitialState())->second));
-
-	result.setInputAlphabet(fsm.getInputAlphabet());
-
-	for(auto iter = fsm.getStates().begin(); iter != fsm.getStates().end(); iter++) {
-		result.addState(DefaultStateType(renamingData.find(*iter)->second));
-	}
-
-	for(auto iter = fsm.getFinalStates().begin(); iter != fsm.getFinalStates().end(); iter++) {
-		result.addFinalState(DefaultStateType(renamingData.find(*iter)->second));
-	}
-
-	for(auto iter = fsm.getTransitions().begin(); iter != fsm.getTransitions().end(); iter++) {
-		result.addTransition(DefaultStateType(renamingData.find(iter->first.first)->second), iter->first.second, DefaultStateType(renamingData.find(iter->second)->second));
-	}
-
-	return result;
-}
-
-auto RenameDFA = registration::AbstractRegister < Rename, automaton::DFA < >, const automaton::DFA < > & > ( Rename::rename );
-
-automaton::DPDA < > Rename::rename(const automaton::DPDA < > & pda) {
-	int counterState = 0;
-	ext::map<DefaultStateType, int > renamingDataState;
-	int counterSymbol = 0;
-	ext::map<DefaultSymbolType, int > renamingDataSymbol;
-
-	for(const DefaultStateType & state : pda.getStates())
-		renamingDataState.insert(std::make_pair(state, counterState++));
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		renamingDataSymbol.insert(std::make_pair(symbol, counterSymbol++));
-
-	automaton::DPDA < > result(DefaultStateType(renamingDataState.find(pda.getInitialState())->second), DefaultSymbolType(renamingDataSymbol.find(pda.getInitialSymbol())->second));
-
-	result.setInputAlphabet(pda.getInputAlphabet());
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		result.addPushdownStoreSymbol(DefaultSymbolType(renamingDataSymbol.find(symbol)->second));
-
-	for(const DefaultStateType & state : pda.getStates())
-		result.addState(DefaultStateType(renamingDataState.find(state)->second));
-
-	for(const DefaultStateType & state : pda.getFinalStates())
-		result.addFinalState(DefaultStateType(renamingDataState.find(state)->second));
-
-	for(const auto & transition : pda.getTransitions()) {
-		ext::vector<DefaultSymbolType> pop;
-		for(const auto& elem : std::get<2>(transition.first)) {
-			pop.push_back(DefaultSymbolType(renamingDataSymbol.find(elem)->second));
-		}
-		ext::vector<DefaultSymbolType> push;
-		for(const auto& elem : transition.second.second) {
-			push.push_back(DefaultSymbolType(renamingDataSymbol.find(elem)->second));
-		}
-		result.addTransition(DefaultStateType(renamingDataState.find(std::get<0>(transition.first))->second), std::get<1>(transition.first), pop, DefaultStateType(renamingDataState.find(transition.second.first)->second), push);
-	}
-
-	return result;
-}
-
-auto RenameDPDA = registration::AbstractRegister < Rename, automaton::DPDA < >, const automaton::DPDA < > & > ( Rename::rename );
-
-automaton::SinglePopDPDA < > Rename::rename(const automaton::SinglePopDPDA < > & pda) {
-	int counterState = 0;
-	ext::map<DefaultStateType, int > renamingDataState;
-	int counterSymbol = 0;
-	ext::map<DefaultSymbolType, int > renamingDataSymbol;
-
-	for(auto iter = pda.getStates().begin(); iter != pda.getStates().end(); iter++) {
-		renamingDataState.insert(std::make_pair(*iter, counterState++));
-	}
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		renamingDataSymbol.insert(std::make_pair(symbol, counterSymbol++));
-
-	automaton::SinglePopDPDA < > result(DefaultStateType(renamingDataState.find(pda.getInitialState())->second), DefaultSymbolType(renamingDataSymbol.find(pda.getInitialSymbol())->second));
-
-	result.setInputAlphabet(pda.getInputAlphabet());
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		result.addPushdownStoreSymbol(DefaultSymbolType(renamingDataSymbol.find(symbol)->second));
-
-	for(auto iter = pda.getStates().begin(); iter != pda.getStates().end(); iter++) {
-		result.addState(DefaultStateType(renamingDataState.find(*iter)->second));
-	}
-
-	for(auto iter = pda.getFinalStates().begin(); iter != pda.getFinalStates().end(); iter++) {
-		result.addFinalState(DefaultStateType(renamingDataState.find(*iter)->second));
-	}
-
-	for(auto iter = pda.getTransitions().begin(); iter != pda.getTransitions().end(); iter++) {
-		ext::vector<DefaultSymbolType> push;
-		for(const auto& elem : iter->second.second) {
-			push.push_back(DefaultSymbolType(renamingDataSymbol.find(elem)->second));
-		}
-		result.addTransition(DefaultStateType(renamingDataState.find(std::get<0>(iter->first))->second), std::get<1>(iter->first), DefaultSymbolType(renamingDataSymbol.find(std::get<2>(iter->first))->second), DefaultStateType(renamingDataState.find(iter->second.first)->second), push);
-	}
-
-	return result;
-}
-
-auto RenameSinglePopDPDA = registration::AbstractRegister < Rename, automaton::SinglePopDPDA < >, const automaton::SinglePopDPDA < > & > ( Rename::rename );
-
-automaton::InputDrivenDPDA < > Rename::rename(const automaton::InputDrivenDPDA < > & pda) {
-	int counter = 0;
-	ext::map<DefaultStateType, int > renamingData;
-	int counterSymbol = 0;
-	ext::map<DefaultSymbolType, int > renamingDataSymbol;
-
-	for(auto iter = pda.getStates().begin(); iter != pda.getStates().end(); iter++) {
-		renamingData.insert(std::make_pair(*iter, counter++));
-	}
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		renamingDataSymbol.insert(std::make_pair(symbol, counterSymbol++));
-
-	automaton::InputDrivenDPDA < > result(DefaultStateType(renamingData.find(pda.getInitialState())->second), DefaultSymbolType(renamingDataSymbol.find(pda.getInitialSymbol())->second));
-
-	result.setInputAlphabet(pda.getInputAlphabet());
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		result.addPushdownStoreSymbol(DefaultSymbolType(renamingDataSymbol.find(symbol)->second));
-
-	for(const std::pair<const DefaultSymbolType, std::pair<ext::vector<DefaultSymbolType>, ext::vector<DefaultSymbolType>>> operation : pda.getPushdownStoreOperations()) {
-		ext::vector<DefaultSymbolType> pop;
-		for(const auto& elem : operation.second.first) {
-			pop.push_back(DefaultSymbolType(renamingDataSymbol.find(elem)->second));
-		}
-		ext::vector<DefaultSymbolType> push;
-		for(const auto& elem : operation.second.second) {
-			push.push_back(DefaultSymbolType(renamingDataSymbol.find(elem)->second));
-		}
-		result.setPushdownStoreOperation(operation.first, pop, push);
-	}
-
-	for(auto iter = pda.getStates().begin(); iter != pda.getStates().end(); iter++) {
-		result.addState(DefaultStateType(renamingData.find(*iter)->second));
-	}
-
-	for(auto iter = pda.getFinalStates().begin(); iter != pda.getFinalStates().end(); iter++) {
-		result.addFinalState(DefaultStateType(renamingData.find(*iter)->second));
-	}
-
-	for(auto iter = pda.getTransitions().begin(); iter != pda.getTransitions().end(); iter++) {
-		result.addTransition(DefaultStateType(renamingData.find(iter->first.first)->second), iter->first.second, DefaultStateType(renamingData.find(iter->second)->second));
-	}
-
-	return result;
-}
-
-auto RenameInputDrivenDPDA = registration::AbstractRegister < Rename, automaton::InputDrivenDPDA < >, const automaton::InputDrivenDPDA < > & > ( Rename::rename );
-
-automaton::VisiblyPushdownDPDA < > Rename::rename(const automaton::VisiblyPushdownDPDA < > & pda) {
-	int counterState = 0;
-	ext::map<DefaultStateType, int > renamingDataState;
-	int counterSymbol = 0;
-	ext::map<DefaultSymbolType, int > renamingDataSymbol;
-
-	for(auto iter = pda.getStates().begin(); iter != pda.getStates().end(); iter++) {
-		renamingDataState.insert(std::make_pair(*iter, counterState++));
-	}
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		renamingDataSymbol.insert(std::make_pair(symbol, counterSymbol++));
-
-	automaton::VisiblyPushdownDPDA < > result(DefaultStateType(renamingDataState.find(pda.getInitialState())->second), DefaultSymbolType(renamingDataSymbol.find(pda.getBottomOfTheStackSymbol())->second));
-
-	result.setCallInputAlphabet(pda.getCallInputAlphabet());
-	result.setLocalInputAlphabet(pda.getLocalInputAlphabet());
-	result.setReturnInputAlphabet(pda.getReturnInputAlphabet());
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		result.addPushdownStoreSymbol(DefaultSymbolType(renamingDataSymbol.find(symbol)->second));
-
-	for(auto iter = pda.getStates().begin(); iter != pda.getStates().end(); iter++) {
-		result.addState(DefaultStateType(renamingDataState.find(*iter)->second));
-	}
-
-	for(auto iter = pda.getFinalStates().begin(); iter != pda.getFinalStates().end(); iter++) {
-		result.addFinalState(DefaultStateType(renamingDataState.find(*iter)->second));
-	}
-
-	for(auto iter = pda.getCallTransitions().begin(); iter != pda.getCallTransitions().end(); iter++) {
-		result.addCallTransition(DefaultStateType(renamingDataState.find(iter->first.first)->second), iter->first.second, DefaultStateType(renamingDataState.find(iter->second.first)->second), DefaultSymbolType(renamingDataSymbol.find(iter->second.second)->second));
-	}
-
-	for(auto iter = pda.getLocalTransitions().begin(); iter != pda.getLocalTransitions().end(); iter++) {
-		result.addLocalTransition(DefaultStateType(renamingDataState.find(iter->first.first)->second), iter->first.second, DefaultStateType(renamingDataState.find(iter->second)->second));
-	}
-
-	for(auto iter = pda.getReturnTransitions().begin(); iter != pda.getReturnTransitions().end(); iter++) {
-		result.addReturnTransition(DefaultStateType(renamingDataState.find(std::get<0>(iter->first))->second), std::get<1>(iter->first), DefaultSymbolType(renamingDataSymbol.find(std::get<2>(iter->first))->second), DefaultStateType(renamingDataState.find(iter->second)->second));
-	}
-
-	return result;
-}
-
-auto RenameVisiblyPushdownDPDA = registration::AbstractRegister < Rename, automaton::VisiblyPushdownDPDA < >, const automaton::VisiblyPushdownDPDA < > & > ( Rename::rename );
-
-automaton::RealTimeHeightDeterministicDPDA < > Rename::rename(const automaton::RealTimeHeightDeterministicDPDA < > & pda) {
-	int counterState = 0;
-	ext::map<DefaultStateType, int > renamingDataState;
-	int counterSymbol = 0;
-	ext::map<DefaultSymbolType, int > renamingDataSymbol;
-
-	for(auto iter = pda.getStates().begin(); iter != pda.getStates().end(); iter++) {
-		renamingDataState.insert(std::make_pair(*iter, counterState++));
-	}
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		renamingDataSymbol.insert(std::make_pair(symbol, counterSymbol++));
-
-	automaton::RealTimeHeightDeterministicDPDA < > result(DefaultStateType(renamingDataState.find(pda.getInitialState())->second), DefaultSymbolType(renamingDataSymbol.find(pda.getBottomOfTheStackSymbol())->second));
-
-	result.setInputAlphabet(pda.getInputAlphabet());
-
-	for(const DefaultSymbolType & symbol : pda.getPushdownStoreAlphabet())
-		result.addPushdownStoreSymbol(DefaultSymbolType(renamingDataSymbol.find(symbol)->second));
-
-	for(auto iter = pda.getStates().begin(); iter != pda.getStates().end(); iter++) {
-		result.addState(DefaultStateType(renamingDataState.find(*iter)->second));
-	}
-
-	for(auto iter = pda.getFinalStates().begin(); iter != pda.getFinalStates().end(); iter++) {
-		result.addFinalState(DefaultStateType(renamingDataState.find(*iter)->second));
-	}
-
-	for(auto iter = pda.getCallTransitions().begin(); iter != pda.getCallTransitions().end(); iter++) {
-		result.addCallTransition(DefaultStateType(renamingDataState.find(iter->first.first)->second), iter->first.second, DefaultStateType(renamingDataState.find(iter->second.first)->second), DefaultSymbolType(renamingDataSymbol.find(iter->second.second)->second));
-	}
-
-	for(auto iter = pda.getLocalTransitions().begin(); iter != pda.getLocalTransitions().end(); iter++) {
-		result.addLocalTransition(DefaultStateType(renamingDataState.find(iter->first.first)->second), iter->first.second, DefaultStateType(renamingDataState.find(iter->second)->second));
-	}
-
-	for(auto iter = pda.getReturnTransitions().begin(); iter != pda.getReturnTransitions().end(); iter++) {
-		result.addReturnTransition(DefaultStateType(renamingDataState.find(std::get<0>(iter->first))->second), std::get<1>(iter->first), DefaultSymbolType(renamingDataSymbol.find(std::get<2>(iter->first))->second), DefaultStateType(renamingDataState.find(iter->second)->second));
-	}
-
-	return result;
-}
-
-auto RenameRealTimeHeightDeterministicDPDA = registration::AbstractRegister < Rename, automaton::RealTimeHeightDeterministicDPDA < >, const automaton::RealTimeHeightDeterministicDPDA < > & > ( Rename::rename );
+auto RenameDFA = registration::AbstractRegister < Rename, automaton::DFA < DefaultSymbolType, unsigned >, const automaton::DFA < > & > ( Rename::rename );
+auto RenameDPDA = registration::AbstractRegister < Rename, automaton::DPDA < DefaultSymbolType, DefaultEpsilonType, unsigned, unsigned >, const automaton::DPDA < > & > ( Rename::rename );
+auto RenameSinglePopDPDA = registration::AbstractRegister < Rename, automaton::SinglePopDPDA < DefaultSymbolType, DefaultEpsilonType, unsigned, unsigned >, const automaton::SinglePopDPDA < > & > ( Rename::rename );
+auto RenameInputDrivenDPDA = registration::AbstractRegister < Rename, automaton::InputDrivenDPDA < DefaultSymbolType, unsigned, unsigned >, const automaton::InputDrivenDPDA < > & > ( Rename::rename );
+auto RenameVisiblyPushdownDPDA = registration::AbstractRegister < Rename, automaton::VisiblyPushdownDPDA < DefaultSymbolType, unsigned, unsigned >, const automaton::VisiblyPushdownDPDA < > & > ( Rename::rename );
+auto RenameRealTimeHeightDeterministicDPDA = registration::AbstractRegister < Rename, automaton::RealTimeHeightDeterministicDPDA < DefaultSymbolType, DefaultEpsilonType, unsigned, unsigned >, const automaton::RealTimeHeightDeterministicDPDA < > & > ( Rename::rename );
 
 } /* namespace simplify */
 
diff --git a/alib2algo/src/automaton/simplify/Rename.h b/alib2algo/src/automaton/simplify/Rename.h
index 9d0c4e1d36..f93086b4c5 100644
--- a/alib2algo/src/automaton/simplify/Rename.h
+++ b/alib2algo/src/automaton/simplify/Rename.h
@@ -8,12 +8,18 @@
 #ifndef RENAME_H_
 #define RENAME_H_
 
+#include <alib/algorithm>
+#include <alib/iostream>
+#include <alib/map>
+#include <alib/vector>
+#include <sstream>
+
 #include <automaton/FSM/DFA.h>
 #include <automaton/PDA/DPDA.h>
-#include <automaton/PDA/SinglePopDPDA.h>
 #include <automaton/PDA/InputDrivenDPDA.h>
-#include <automaton/PDA/VisiblyPushdownDPDA.h>
 #include <automaton/PDA/RealTimeHeightDeterministicDPDA.h>
+#include <automaton/PDA/SinglePopDPDA.h>
+#include <automaton/PDA/VisiblyPushdownDPDA.h>
 
 namespace automaton {
 
@@ -21,14 +27,254 @@ namespace simplify {
 
 class Rename {
 public:
-	static automaton::DFA<> rename(const automaton::DFA<>& dfa);
-	static automaton::DPDA < > rename(const automaton::DPDA < > & pda);
-	static automaton::SinglePopDPDA < > rename(const automaton::SinglePopDPDA < > & pda);
-	static automaton::InputDrivenDPDA < > rename(const automaton::InputDrivenDPDA < > & pda);
-	static automaton::VisiblyPushdownDPDA < > rename(const automaton::VisiblyPushdownDPDA < > & pda);
-	static automaton::RealTimeHeightDeterministicDPDA < > rename(const automaton::RealTimeHeightDeterministicDPDA < > & pda);
+	template < class SymbolType, class StateType >
+	static automaton::DFA < SymbolType, unsigned > rename ( const automaton::DFA < SymbolType, StateType > & dfa );
+
+	template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
+	static automaton::DPDA < InputSymbolType, EpsilonType, unsigned, unsigned > rename ( const automaton::DPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & pda );
+
+	template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
+	static automaton::SinglePopDPDA < InputSymbolType, EpsilonType, unsigned, unsigned > rename ( const automaton::SinglePopDPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & pda );
+
+	template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
+	static automaton::InputDrivenDPDA < InputSymbolType, unsigned, unsigned > rename ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda );
+
+	template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
+	static automaton::VisiblyPushdownDPDA < InputSymbolType, unsigned, unsigned > rename ( const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda );
+
+	template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
+	static automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, EpsilonType, unsigned, unsigned > rename ( const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & pda );
 };
 
+template < class SymbolType, class StateType >
+automaton::DFA < SymbolType, unsigned > Rename::rename ( const automaton::DFA < SymbolType, StateType > & fsm ) {
+	unsigned counter = 0;
+	ext::map < StateType, unsigned > renamingData;
+
+	for ( const StateType & state : fsm.getStates ( ) )
+		renamingData.insert ( std::make_pair ( state, counter++ ) );
+
+	automaton::DFA < SymbolType, unsigned > result ( renamingData.at ( fsm.getInitialState ( ) ) );
+
+	result.setInputAlphabet ( fsm.getInputAlphabet ( ) );
+
+	for ( const StateType & state : fsm.getStates ( ) )
+		result.addState ( renamingData.at ( state ) );
+
+	for ( const StateType & state : fsm.getFinalStates ( ) )
+		result.addFinalState ( renamingData.at ( state ) );
+
+	for ( const auto & transition : fsm.getTransitions ( ) )
+		result.addTransition ( renamingData.at ( transition.first.first ), transition.first.second, renamingData.at ( transition.second ) );
+
+	return result;
+}
+
+template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
+automaton::DPDA < InputSymbolType, EpsilonType, unsigned, unsigned > Rename::rename ( const automaton::DPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & pda ) {
+	unsigned counterState = 0;
+	ext::map < StateType, unsigned > renamingDataState;
+	unsigned counterSymbol = 0;
+	ext::map < InputSymbolType, unsigned > renamingDataSymbol;
+
+	for ( const StateType & state : pda.getStates ( ) )
+		renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
+
+	automaton::DPDA < InputSymbolType, EpsilonType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getInitialSymbol ( ) ) );
+
+	result.setInputAlphabet ( pda.getInputAlphabet ( ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
+
+	for ( const StateType & state : pda.getStates ( ) )
+		result.addState ( renamingDataState.at ( state ) );
+
+	for ( const StateType & state : pda.getFinalStates ( ) )
+		result.addFinalState ( renamingDataState.at ( state ) );
+
+	for ( const auto & transition : pda.getTransitions ( ) ) {
+		ext::vector < unsigned > pop;
+
+		for ( const InputSymbolType & symbol : std::get < 2 > ( transition.first ) )
+			pop.push_back ( renamingDataSymbol.at ( symbol ) );
+
+		ext::vector < unsigned > push;
+
+		for ( const InputSymbolType & symbol : transition.second.second )
+			push.push_back ( renamingDataSymbol.at ( symbol ) );
+
+		result.addTransition ( renamingDataState.at ( std::get < 0 > ( transition.first ) ), std::get < 1 > ( transition.first ), pop, renamingDataState.at ( transition.second.first ), push );
+	}
+
+	return result;
+}
+
+template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
+automaton::SinglePopDPDA < InputSymbolType, EpsilonType, unsigned, unsigned > Rename::rename ( const automaton::SinglePopDPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & pda ) {
+	int counterState = 0;
+	ext::map < StateType, unsigned > renamingDataState;
+	int counterSymbol = 0;
+	ext::map < InputSymbolType, unsigned > renamingDataSymbol;
+
+	for ( const StateType & state : pda.getStates ( ) )
+		renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
+
+	automaton::SinglePopDPDA < InputSymbolType, EpsilonType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getInitialSymbol ( ) ) );
+
+	result.setInputAlphabet ( pda.getInputAlphabet ( ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
+
+	for ( const StateType & state : pda.getStates ( ) )
+		result.addState ( renamingDataState.at ( state ) );
+
+	for ( const StateType & state : pda.getFinalStates ( ) )
+		result.addFinalState ( renamingDataState.at ( state ) );
+
+	for ( const auto & transition : pda.getTransitions ( ) ) {
+		ext::vector < unsigned > push;
+
+		for ( const PushdownStoreSymbolType & symbol : transition.second.second )
+			push.push_back ( renamingDataSymbol.at ( symbol ) );
+
+		result.addTransition ( renamingDataState.at ( std::get < 0 > ( transition.first ) ), std::get < 1 > ( transition.first ), renamingDataSymbol.at ( std::get < 2 > ( transition.first ) ), renamingDataState.at ( transition.second.first ), push );
+	}
+
+	return result;
+}
+
+template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
+automaton::InputDrivenDPDA < InputSymbolType, unsigned, unsigned > Rename::rename ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
+	int counterState = 0;
+	ext::map < StateType, unsigned > renamingDataState;
+	int counterSymbol = 0;
+	ext::map < InputSymbolType, unsigned > renamingDataSymbol;
+
+	for ( const StateType & state : pda.getStates ( ) )
+		renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
+
+	automaton::InputDrivenDPDA < InputSymbolType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getInitialSymbol ( ) ) );
+
+	result.setInputAlphabet ( pda.getInputAlphabet ( ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
+
+	for ( const std::pair < const InputSymbolType, std::pair < ext::vector < PushdownStoreSymbolType >, ext::vector < PushdownStoreSymbolType > > > operation : pda.getPushdownStoreOperations ( ) ) {
+		ext::vector < unsigned > pop;
+
+		for ( const PushdownStoreSymbolType & symbol : operation.second.first )
+			pop.push_back ( renamingDataSymbol.at ( symbol ) );
+
+		ext::vector < unsigned > push;
+
+		for ( const PushdownStoreSymbolType & symbol : operation.second.second )
+			push.push_back ( renamingDataSymbol.at ( symbol ) );
+
+		result.setPushdownStoreOperation ( operation.first, pop, push );
+	}
+
+	for ( const StateType & state : pda.getStates ( ) )
+		result.addState ( renamingDataState.at ( state ) );
+
+	for ( const StateType & state : pda.getFinalStates ( ) )
+		result.addFinalState ( renamingDataState.at ( state ) );
+
+	for ( const auto & transition : pda.getTransitions ( ) )
+		result.addTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second ) );
+
+	return result;
+}
+
+template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
+automaton::VisiblyPushdownDPDA < InputSymbolType, unsigned, unsigned > Rename::rename ( const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
+	int counterState = 0;
+	ext::map < StateType, unsigned > renamingDataState;
+	int counterSymbol = 0;
+	ext::map < InputSymbolType, unsigned > renamingDataSymbol;
+
+	for ( const StateType & state : pda.getStates ( ) )
+		renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
+
+	automaton::VisiblyPushdownDPDA < InputSymbolType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getBottomOfTheStackSymbol ( ) ) );
+
+	result.setCallInputAlphabet ( pda.getCallInputAlphabet ( ) );
+	result.setLocalInputAlphabet ( pda.getLocalInputAlphabet ( ) );
+	result.setReturnInputAlphabet ( pda.getReturnInputAlphabet ( ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
+
+	for ( const StateType & state : pda.getStates ( ) )
+		result.addState ( renamingDataState.at ( state ) );
+
+	for ( const StateType & state : pda.getFinalStates ( ) )
+		result.addFinalState ( renamingDataState.at ( state ) );
+
+	for ( const auto & transition : pda.getCallTransitions ( ) )
+		result.addCallTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second.first ), renamingDataSymbol.at ( transition.second.second ) );
+
+	for ( const auto & transition : pda.getLocalTransitions ( ) )
+		result.addLocalTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second ) );
+
+	for ( const auto & transition : pda.getReturnTransitions ( ) )
+		result.addReturnTransition ( renamingDataState.at ( std::get < 0 > ( transition.first ) ), std::get < 1 > ( transition.first ), renamingDataSymbol.at ( std::get < 2 > ( transition.first ) ), renamingDataState.at ( transition.second ) );
+
+	return result;
+}
+
+template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
+automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, EpsilonType, unsigned, unsigned > Rename::rename ( const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & pda ) {
+	int counterState = 0;
+	ext::map < StateType, unsigned > renamingDataState;
+	int counterSymbol = 0;
+	ext::map < InputSymbolType, unsigned > renamingDataSymbol;
+
+	for ( const StateType & state : pda.getStates ( ) )
+		renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
+
+	automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, EpsilonType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getBottomOfTheStackSymbol ( ) ) );
+
+	result.setInputAlphabet ( pda.getInputAlphabet ( ) );
+
+	for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
+		result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
+
+	for ( const StateType & state : pda.getStates ( ) )
+		result.addState ( renamingDataState.at ( state ) );
+
+	for ( const StateType & state : pda.getFinalStates ( ) )
+		result.addFinalState ( renamingDataState.at ( state ) );
+
+	for ( const auto & transition : pda.getCallTransitions ( ) )
+		result.addCallTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second.first ), renamingDataSymbol.at ( transition.second.second ) );
+
+	for ( const auto & transition : pda.getLocalTransitions ( ) )
+		result.addLocalTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second ) );
+
+	for ( const auto & transition : pda.getReturnTransitions ( ) )
+		result.addReturnTransition ( renamingDataState.at ( std::get < 0 > ( transition.first ) ), std::get < 1 > ( transition.first ), renamingDataSymbol.at ( std::get < 2 > ( transition.first ) ), renamingDataState.at ( transition.second ) );
+
+	return result;
+}
+
 } /* namespace simplify */
 
 } /* namespace automaton */
-- 
GitLab