DotConverter.h

Go to the documentation of this file.

 
#pragma once
 
#include <ext/ostream>
#include <ext/sstream>
 
#include <ext/utility>
#include <ext/typeinfo>
 
#include <alib/set>
#include <alib/map>
#include <alib/list>
#include <alib/vector>
 
#include <exception/CommonException.h>
#include <string/String.h>
 
#include <automaton/FSM/NFA.h>
#include <automaton/FSM/EpsilonNFA.h>
#include <automaton/FSM/MultiInitialStateNFA.h>
#include <automaton/FSM/DFA.h>
#include <automaton/FSM/ExtendedNFA.h>
#include <automaton/FSM/CompactNFA.h>
#include <automaton/TA/NFTA.h>
#include <automaton/TA/EpsilonNFTA.h>
#include <automaton/TA/UnorderedNFTA.h>
#include <automaton/TA/ExtendedNFTA.h>
#include <automaton/TA/DFTA.h>
#include <automaton/TA/ArcFactoredNondeterministicZAutomaton.h>
#include <automaton/TA/NondeterministicZAutomaton.h>
#include <automaton/PDA/NPDA.h>
#include <automaton/PDA/SinglePopNPDA.h>
#include <automaton/PDA/InputDrivenDPDA.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>
#include <automaton/TM/OneTapeDTM.h>
 
#include "common/converterCommon.hpp"
 
#include <factory/StringDataFactory.hpp>
#include <string/string/LinearString.h>
#include <regexp/string/UnboundedRegExp.h>
 
#include "DotConverterTreePart.hxx"
#include "DotConverterRTEPart.hxx"
 
namespace convert {
 
class DotConverter {
    static constexpr const size_t CAPTION_LENGTH_LIMIT = 100;
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::DFA < SymbolType, StateType > & fsm, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::NFA < SymbolType, StateType > & fsm, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::MultiInitialStateNFA < SymbolType, StateType > & fsm, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::EpsilonNFA < SymbolType, StateType > & fsm, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::ExtendedNFA < SymbolType, StateType > & fsm, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::CompactNFA < SymbolType, StateType > & fsm, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::NFTA < SymbolType, StateType > & fta, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::EpsilonNFTA < SymbolType, StateType > & fta, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::UnorderedNFTA < SymbolType, StateType > & fta, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::ExtendedNFTA < SymbolType, StateType > & fta, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::DFTA < SymbolType, StateType > & fta, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::ArcFactoredNondeterministicZAutomaton < SymbolType, StateType > & afnza, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::NondeterministicZAutomaton < SymbolType, StateType > & nza, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::SinglePopNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::InputDrivenNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void transitions(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream & out);
 
    template < class SymbolType, class StateType >
    static void transitions(const automaton::OneTapeDTM < SymbolType, StateType > & tm, const ext::map < StateType, int > & states, ext::ostream & out);
public:
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::DFA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::NFA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::MultiInitialStateNFA < SymbolType, StateType >& a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::EpsilonNFA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::ExtendedNFA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::CompactNFA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::NFTA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::EpsilonNFTA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::UnorderedNFTA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::ExtendedNFTA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::DFTA < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::ArcFactoredNondeterministicZAutomaton < SymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::NondeterministicZAutomaton < SymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::SinglePopNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::InputDrivenNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a);
 
    template < class SymbolType, class StateType >
    static void convert(ext::ostream& out, const automaton::OneTapeDTM < SymbolType, StateType > & a);
 
    template < class SymbolType >
    static void convert(ext::ostream& out, const rte::FormalRTE < SymbolType > & e );
 
    template < class SymbolType >
    static void convert(ext::ostream& out, const tree::RankedTree < SymbolType > & e );
 
    template < class T >
    static std::string convert ( const T & automaton ) {
        ext::ostringstream ss;
        convert ( ss, automaton );
        return ss.str ( );
    }
};
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::EpsilonNFA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::MultiInitialStateNFA < SymbolType, StateType >& a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    for (const StateType& state : a.getInitialStates()) {
        out << "0 -> " << states.find(state)->second << ";\n";
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::NFA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::DFA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::ExtendedNFA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::CompactNFA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::NFTA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::EpsilonNFTA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::UnorderedNFTA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::ExtendedNFTA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=TD;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; State" << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; State" << state.second << ";\n";
        }
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::DFTA < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::ArcFactoredNondeterministicZAutomaton < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::NondeterministicZAutomaton < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::InputDrivenNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    for (const StateType& state : a.getInitialStates()) {
        out << "0 -> " << states.find(state)->second << ";\n";
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    for (const StateType& state : a.getInitialStates()) {
        out << "0 -> " << states.find(state)->second << ";\n";
    }
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::SinglePopNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::convert(ext::ostream& out, const automaton::OneTapeDTM < SymbolType, StateType > & a) {
    out << "digraph automaton {\n";
    out << "rankdir=LR;\n";
    int cnt = 1;
 
    //Map states to indices
    ext::map<StateType, int> states;
    for (const StateType& state : a.getStates()) {
        states.insert(std::make_pair(state, cnt++));
    }
 
    //Print final states
    for (const StateType& state : a.getFinalStates()) {
        out << "node [shape = doublecircle, label=\"" << replace ( factory::StringDataFactory::toString ( state ), "\"", "\\\"" ) << "\"]; " << states.find(state)->second << ";\n";
    }
 
    //Print nonfinal states
    for (const auto& state : states) {
        if (!a.getFinalStates().count(state.first)) {
            out << "node [shape = circle, label=\"" << replace ( factory::StringDataFactory::toString ( state.first ), "\"", "\\\"" ) << "\" ]; " << state.second << ";\n";
        }
    }
 
    //Mark initial states
    out << "node [shape = plaintext, label=\"start\"]; 0; \n";
    out << "0 -> " << states.find(a.getInitialState())->second << ";\n";
 
    transitions(a, states, out);
    out << "}";
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::EpsilonNFA < SymbolType, StateType > & fsm, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fsm.getTransitions()) {
        std::string symbol;
        if (transition.first.second.is_epsilon()) {
            symbol = "&epsilon;";
        } else {
            symbol = replace ( factory::StringDataFactory::toString ( std::get<1>(transition.first ).getSymbol()), "\"", "\\\"" );
        }
 
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class SymbolType >
void DotConverter::convert(ext::ostream& out, const rte::FormalRTE < SymbolType > & e ) {
    out << "digraph rte {\n";
    DotConverterRTE::convertInternal ( out, e );
    out << '\n' << "}" << std::endl;
}
 
template < class SymbolType >
void DotConverter::convert(ext::ostream& out, const tree::RankedTree < SymbolType > & e ) {
    out << "digraph tree {\n";
    DotConverterTree::convertInternal ( out, e );
    out << '\n' << "}" << std::endl;
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::MultiInitialStateNFA < SymbolType, StateType >& fsm, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fsm.getTransitions()) {
        std::string symbol = replace ( factory::StringDataFactory::toString ( transition.first.second ), "\"", "\\\"" );
 
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair< const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::NFA < SymbolType, StateType > & fsm, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fsm.getTransitions()) {
        std::string symbol = replace ( factory::StringDataFactory::toString ( transition.first.second ), "\"", "\\\"" );
 
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::DFA < SymbolType, StateType > & fsm, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fsm.getTransitions()) {
        std::string symbol = replace ( factory::StringDataFactory::toString ( transition.first.second ), "\"", "\\\"" );
 
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::ExtendedNFA < SymbolType, StateType > & fsm, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fsm.getTransitions()) {
        std::string symbol = replace ( factory::StringDataFactory::toString ( transition.first.second ), "\"", "\\\"" );
 
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find ( transition.second )->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::CompactNFA < SymbolType, StateType > & fsm, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fsm.getTransitions()) {
        std::string symbol = replace ( factory::StringDataFactory::toString ( string::stringFrom ( transition.first.second ) ), "\"", "\\\"" );
 
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::ExtendedNFTA < SymbolType, StateType > & fta, const ext::map<StateType, int>& states, ext::ostream& out) {
    //print the map
    unsigned auxNodeCnt = 1;
    for (const auto & transition : fta.getTransitions ( ) ) {
        // print subgraph with the rte
        out << '\n';
        out << "subgraph cluster_rte_" << auxNodeCnt << "{" << '\n';
        out << "label=\"rte_" << auxNodeCnt << "\"\n";
        out << "color = blue;\n";
        convert::DotConverterRTE::convertInternal ( out, rte::FormalRTE < ext::variant < SymbolType, StateType > > ( transition.first.first ), "x" + ext::to_string ( auxNodeCnt ) + "x" );
        out << "}\n" << std::endl;
 
        out << "node [shape = point, label=\"\"]; Aux" << auxNodeCnt << ";\n";
        unsigned j = 1;
        for(const auto & state : transition.first.second) // from source states to connecting node
            out << "State" << states.at ( state ) << " -> " << "Aux" << auxNodeCnt << "[label=\"" << j++ << "\"];\n";
        for ( const auto & target : transition.second ) // from connecting node to target nodes
            out << "Aux" << auxNodeCnt << " -> State" << states.at ( target ) << "[label=\"" << "rte_" << auxNodeCnt << "\"];\n";
 
        auxNodeCnt++;
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::NFTA < SymbolType, StateType > & fta, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, ext::vector<int>>, std::string> transitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fta.getTransitions()) {
        std::string symbol = replace ( factory::StringDataFactory::toString ( transition.first.first.getSymbol( )), "\"", "\\\"" );
        symbol += ext::to_string(transition.first.first.getRank());
 
        std::pair<int, ext::vector<int>> key(states.find(transition.second)->second, {});
        for(const StateType& state : transition.first.second) {
            key.second.push_back(states.find(state)->second);
        }
        ext::map<std::pair<int, ext::vector<int>>, std::string>::iterator mapit = transitions.find(key);
 
        if (mapit == transitions.end()) {
            transitions.insert(std::make_pair(key, symbol));
        } else {
            mapit->second += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //Print auxilary dots
    for (unsigned i = 1; i <= transitions.size(); i++) {
        out << "node [shape = point, label=\"\"]; " << states.size() + i << ";\n";
    }
 
    //print the map
    unsigned i = states.size() + 1;
    for (std::pair<const std::pair<int, ext::vector<int>>, std::string>& transition : transitions) {
        out << i << " -> " << transition.first.first;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
        unsigned j = 0;
        for(int from : transition.first.second) {
            out << from << " -> " << i;
            out << "[label=\"" << j << "\"]\n";
            j++;
        }
        i++;
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::EpsilonNFTA < SymbolType, StateType > & fta, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, ext::vector<int>>, std::string> transitions;
    ext::multimap<int, int> epsilonTransitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fta.getTransitions()) {
        if ( transition.first.template is < StateType > ( ) ) {
            const StateType & source = transition.first.template get < StateType > ( );
            epsilonTransitions.insert ( states.find ( source )->second, states.find ( transition.second )->second );
        } else {
            const ext::pair < common::ranked_symbol < SymbolType >, ext::vector < StateType > > & source = transition.first.template get < ext::pair < common::ranked_symbol < SymbolType >, ext::vector < StateType > > > ( );
            std::string symbol = replace ( factory::StringDataFactory::toString ( source.first.getSymbol( )), "\"", "\\\"" );
            symbol += ext::to_string(source.first.getRank());
 
            std::pair<int, ext::vector<int>> key(states.find(transition.second)->second, {});
            for(const StateType& state : source.second) {
                key.second.push_back(states.find(state)->second);
            }
            ext::map<std::pair<int, ext::vector<int>>, std::string>::iterator mapit = transitions.find(key);
 
            if (mapit == transitions.end()) {
                transitions.insert(std::make_pair(key, symbol));
            } else {
                mapit->second += ",";
 
                size_t pos = mapit->second.find_last_of("\n");
                if(pos == std::string::npos) pos = 0;
                if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
                else mapit->second += " ";
 
                mapit->second += symbol;
            }
        }
    }
 
    //Print auxilary dots
    for (unsigned i = 1; i <= transitions.size(); i++) {
        out << "node [shape = point, label=\"\"]; " << states.size() + i << ";\n";
    }
 
    //print the map
    unsigned i = states.size() + 1;
    for (std::pair<const std::pair<int, ext::vector<int>>, std::string>& transition : transitions) {
        out << i << " -> " << transition.first.first;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
        unsigned j = 0;
        for(int from : transition.first.second) {
            out << from << " -> " << i;
            out << "[label=\"" << j << "\"]\n";
            j++;
        }
        i++;
    }
 
    for ( const std::pair < const int, int > epsilonTransition : epsilonTransitions ) {
        out << epsilonTransition.first << " -> " << epsilonTransition.second;
        out << "[label=\"&epsilon;\"]\n";
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::UnorderedNFTA < SymbolType, StateType > & fta, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, ext::vector<int>>, std::string> transitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fta.getTransitions()) {
        std::string symbol = replace ( factory::StringDataFactory::toString ( transition.first.first.getSymbol( )), "\"", "\\\"" );
        symbol += ext::to_string(transition.first.first.getRank());
 
        std::pair<int, ext::vector<int>> key(states.find(transition.second)->second, {});
        for(const StateType& state : transition.first.second) {
            key.second.push_back(states.find(state)->second);
        }
        ext::map<std::pair<int, ext::vector<int>>, std::string>::iterator mapit = transitions.find(key);
 
        if (mapit == transitions.end()) {
            transitions.insert(std::make_pair(key, symbol));
        } else {
            mapit->second += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //Print auxilary dots
    for (unsigned i = 1; i <= transitions.size(); i++) {
        out << "node [shape = point, label=\"\"]; " << states.size() + i << ";\n";
    }
 
    //print the map
    unsigned i = states.size() + 1;
    for (std::pair<const std::pair<int, ext::vector<int>>, std::string>& transition : transitions) {
        out << i << " -> " << transition.first.first;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
        unsigned j = 0;
        for(int from : transition.first.second) {
            out << from << " -> " << i << "\n";
            j++;
        }
        i++;
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::DFTA < SymbolType, StateType > & fta, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, ext::vector<int>>, std::string> transitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : fta.getTransitions()) {
        std::string symbol = replace ( factory::StringDataFactory::toString ( transition.first.first.getSymbol( )), "\"", "\\\"" );
        symbol += ext::to_string(transition.first.first.getRank());
 
        std::pair<int, ext::vector<int>> key(states.find(transition.second)->second, {});
        for(const StateType& state : transition.first.second) {
            key.second.push_back(states.find(state)->second);
        }
        ext::map<std::pair<int, ext::vector<int>>, std::string>::iterator mapit = transitions.find(key);
 
        if (mapit == transitions.end()) {
            transitions.insert(std::make_pair(key, symbol));
        } else {
            mapit->second += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //Print auxilary dots
    for (unsigned i = 1; i <= transitions.size(); i++) {
        out << "node [shape = point, label=\"\"]; " << states.size() + i << ";\n";
    }
 
    //print the map
    unsigned i = states.size() + 1;
    for (std::pair<const std::pair<int, ext::vector<int>>, std::string>& transition : transitions) {
        out << i << " -> " << transition.first.first;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
        unsigned j = 0;
        for(int from : transition.first.second) {
            out << from << " -> " << i;
            out << "[label=\"" << j << "\"]\n";
            j++;
        }
        i++;
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::ArcFactoredNondeterministicZAutomaton < SymbolType, StateType > & afnza, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::set < std::tuple<int, int, int> > stateTransitions;
 
    //put transitions from automaton to "transitions"
    for (const auto& transition : afnza.getTransitions()) {
        if ( transition.first.template is < ext::pair < StateType, StateType > > ( ) ) {
            const ext::pair < StateType, StateType > & trans = transition.first.template get < ext::pair < StateType, StateType > > ( );
 
            std::tuple < int, int, int > key ( states.find ( trans.first )->second, states.find ( trans.second )->second, states.find ( transition.second )->second );
            stateTransitions.insert ( std::move ( key ) );
        }
    }
 
    ext::map < int, std::string > symbolTransitions;
 
    for (const auto& transition : afnza.getTransitions()) {
        if ( transition.first.template is < SymbolType > ( ) ) {
            int key = states.find ( transition.second )->second;
 
            const SymbolType & trans = transition.first.template get < SymbolType > ( );
            std::string symbol = replace ( factory::StringDataFactory::toString ( trans ), "\"", "\\\"" );
 
            ext::map < int, std::string >::iterator mapit = symbolTransitions.find ( key );
 
            if (mapit == symbolTransitions.end()) {
                symbolTransitions.insert(std::make_pair(key, symbol));
            } else {
                mapit->second += ",";
 
                size_t pos = mapit->second.find_last_of("\n");
                if(pos == std::string::npos) pos = 0;
                if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
                else mapit->second += " ";
 
                mapit->second += symbol;
            }
        }
    }
 
    //Print auxilary dots, symbols
    for (unsigned i = 1; i <= symbolTransitions.size(); i++) {
        out << "node [shape = point, label=\"\"]; " << states.size ( ) + i << ";\n";
    }
 
    //print the symbol map
    {
        unsigned i = states.size ( ) + 1;
        for ( std::pair < const int, std::string > & transition : symbolTransitions ) {
            out << i << " -> " << transition.first;
            replaceInplace(transition.second, "\n", "\\n");
            out << "[label=\"" << transition.second << "\"]\n";
            i++;
        }
    }
 
    //Print auxilary dots, state transitions
    for (unsigned i = 1; i <= stateTransitions.size(); i++) {
        out << "node [shape = point, label=\"\"]; " << states.size ( ) + symbolTransitions.size ( ) + i << ";\n";
    }
 
    //print the map
    {
        unsigned i = states.size ( ) + symbolTransitions.size ( ) + 1;
        for ( const std::tuple < int, int, int > & transition : stateTransitions ) {
            out << i << " -> " << std::get < 2 > ( transition ) << "\n";
            out << std::get < 0 > ( transition ) << " -> " << i;
            out << "[label=\"" << 0 << "\"]\n";
            out << std::get < 1 > ( transition ) << " -> " << i;
            out << "[label=\"" << 1 << "\"]\n";
            i++;
        }
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::NondeterministicZAutomaton < SymbolType, StateType > & nza, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::set < std::tuple < std::variant < int, std::string >, std::vector < std::variant < int, std::string > >, int > > transitions;
 
    auto transform = [ & ] ( const ext::variant < SymbolType, StateType > & param ) -> std::variant < int, std::string > {
        if ( nza.getInputAlphabet ( ).contains ( param ) ) {
            return replace ( factory::StringDataFactory::toString ( param.template get < SymbolType > ( ) ), "\"", "\\\"" );
        } else {
            return states.find ( param.template get < StateType > ( ) )->second;
        }
    };
 
    //put transitions from automaton to "transitions"
    for ( const std::pair < const ext::pair < ext::variant < SymbolType, StateType >, ext::vector < ext::variant < SymbolType, StateType > > >, StateType > & transition : nza.getTransitions ( ) ) {
        std::variant < int, std::string > sourcesFirst = transform ( transition.first.first );
        std::vector < std::variant < int, std::string > > sourcesSecond;
        for ( const ext::variant < SymbolType, StateType > & from : transition.first.second ) {
            sourcesSecond.push_back ( transform ( from ) );
        }
        int destination = states.find ( transition.second )->second;
 
        transitions.insert ( std::make_tuple ( sourcesFirst, sourcesSecond, destination ) );
    }
 
    // transition structs
    {
        out << "node[shape=record];\n";
        unsigned i = states.size ( ) + 1;
        for ( const std::tuple < std::variant < int, std::string >, std::vector < std::variant < int, std::string > >, int > & transition : transitions ) {
            const auto & firstSource = std::get < 0 > ( transition );
            out << "struct" << i<< "[ label =\"<head> " << ( std::holds_alternative < std::string > ( firstSource ) ? std::get < std::string > ( firstSource ) : "" );
            const auto & secondSource = std::get < 1 > ( transition );
            if ( ! secondSource.empty ( ) ) {
                out << "|{";
                for ( unsigned j = 0; j < secondSource.size ( ); ++ j ) {
                    if ( j != 0 ) {
                        out << "|";
                    }
                    out << "<" << j << "> " << ( std::holds_alternative < std::string > ( firstSource ) ? std::get < std::string > ( firstSource ) : "" );
                }
                out << "}";
            }
            out << "\"];\n";
            i++;
        }
    }
 
    //print the symbol map
    {
        unsigned i = states.size ( ) + 1;
        for ( const std::tuple < std::variant < int, std::string >, std::vector < std::variant < int, std::string > >, int > & transition : transitions ) {
            out << "struct" << i << ":head:e -> " << std::get < 2 > ( transition ) << "\n";
            const auto & firstSource = std::get < 0 > ( transition );
            if ( std::holds_alternative < int > ( firstSource ) ) {
                out << std::get < int > ( firstSource ) << " -> struct" << i << ":head:w\n";
            }
            const auto & secondSource = std::get < 1 > ( transition );
            for ( unsigned j = 0; j < secondSource.size ( ); ++ j ) {
                if ( std::holds_alternative < int > ( secondSource [ j ] ) ) {
                    out << std::get < int > ( secondSource [ j ] ) << " -> struct" << i << ":" << j << "\n";
                }
            }
            i++;
        }
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map < StateType, int > & states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    for (const auto& transition : pda.getTransitions()) {
        std::string symbol;
 
        //input symbol
        if (std::get<1>(transition.first).is_epsilon ( ) ) {
            symbol = "&epsilon;";
        } else {
            symbol = replace ( factory::StringDataFactory::toString ( std::get<1>(transition.first ).getSymbol()), "\"", "\\\"" );
        }
 
        symbol += " |";
 
        //Pop part
        if (std::get<2>(transition.first).empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : std::get<2>(transition.first)) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        symbol += " ->";
 
        //Push part
        if (transition.second.second.empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : transition.second.second) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        //Insert into map
        std::pair<int, int> key(states.find(std::get<0>(transition.first))->second, states.find(transition.second.first)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    for (const auto& transition : pda.getTransitions()) {
        std::string symbol;
 
        //input symbol
        if (std::get<1>(transition.first).is_epsilon ( )) {
            symbol = "&epsilon;";
        } else {
            symbol = replace ( factory::StringDataFactory::toString ( std::get<1>(transition.first ).getSymbol ( )), "\"", "\\\"" );
        }
 
        symbol += " |";
 
        //Pop part
        symbol += " " + replace ( factory::StringDataFactory::toString ( std::get<2>(transition.first )), "\"", "\\\"" );
 
        symbol += " ->";
 
        //Push part
        if (transition.second.second.empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : transition.second.second) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        //Insert into map
        std::pair<int, int> key(states.find(std::get<0>(transition.first))->second, states.find(transition.second.first)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    const auto& symbolToPDSOperation = pda.getPushdownStoreOperations();
    for (const auto& transition : pda.getTransitions()) {
        const auto& pop = symbolToPDSOperation.find(transition.first.second)->second.first;
        const auto& push = symbolToPDSOperation.find(transition.first.second)->second.second;
 
        std::string symbol;
 
        //input symbol
        symbol = replace ( factory::StringDataFactory::toString ( transition.first.second ), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        if (pop.empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : pop) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        symbol += " ->";
 
        const auto& to = transition.second;
        //Push part
        if (push.empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : push) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        //Insert into map
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(to)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::InputDrivenNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    const auto& symbolToPDSOperation = pda.getPushdownStoreOperations();
    for (const auto& transition : pda.getTransitions()) {
        const auto& pop = symbolToPDSOperation.find(transition.first.second)->second.first;
        const auto& push = symbolToPDSOperation.find(transition.first.second)->second.second;
 
        std::string symbol;
 
        //input symbol
        symbol = replace ( factory::StringDataFactory::toString ( transition.first.second ), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        if (pop.empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : pop) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        symbol += " ->";
 
        //Push part
        if (push.empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : push) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        //Insert into map
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find( transition.second )->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    for (const auto& transition : pda.getCallTransitions()) {
        std::string symbol;
 
        //input symbol
        symbol = replace ( factory::StringDataFactory::toString ( transition.first.second ), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        symbol += " &epsilon;";
        symbol += " ->";
 
        symbol += " " + replace ( factory::StringDataFactory::toString ( transition.second.second ), "\"", "\\\"" );
 
        //Insert into map
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second.first)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    for (const auto& transition : pda.getReturnTransitions()) {
        std::string symbol;
 
        //input symbol
        symbol = replace ( factory::StringDataFactory::toString ( std::get<1>(transition.first )), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        symbol += " " + replace ( factory::StringDataFactory::toString ( 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);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    for (const auto& transition : pda.getLocalTransitions()) {
        std::string symbol;
 
        //input symbol
        symbol = replace ( factory::StringDataFactory::toString ( 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);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    for (const auto& transition : pda.getCallTransitions()) {
        std::string symbol;
 
        //input symbol
        symbol = replace ( factory::StringDataFactory::toString ( transition.first.second ), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        symbol += " &epsilon;";
        symbol += " ->";
 
        symbol += " " + replace ( factory::StringDataFactory::toString ( transition.second.second ), "\"", "\\\"" );
 
        //Insert into map
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second.first)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    for (const auto& transition : pda.getReturnTransitions()) {
        std::string symbol;
 
        //input symbol
        symbol = replace ( factory::StringDataFactory::toString ( std::get<1>(transition.first )), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        symbol += " " + replace ( factory::StringDataFactory::toString ( 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);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    for (const auto& transition : pda.getLocalTransitions()) {
        std::string symbol;
 
        //input symbol
        symbol = replace ( factory::StringDataFactory::toString ( 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);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    for (const auto& transition : pda.getCallTransitions()) {
        std::string symbol;
 
        //input symbol
        if(transition.first.second.is_epsilon ( ) )
            symbol = "&epsilon";
        else
            symbol = replace ( factory::StringDataFactory::toString ( transition.first.second.getSymbol ( ) ), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        symbol += " &epsilon;";
        symbol += " ->";
 
        symbol += " " + replace ( factory::StringDataFactory::toString ( transition.second.second ), "\"", "\\\"" );
 
        //Insert into map
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second.first)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    for (const auto& transition : pda.getReturnTransitions()) {
        std::string symbol;
 
        //input symbol
        if(std::get<1>(transition.first).is_epsilon ( ) )
            symbol = "&epsilon";
        else
            symbol = replace ( factory::StringDataFactory::toString ( std::get<1>(transition.first ).getSymbol ( ) ), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        symbol += " " + replace ( factory::StringDataFactory::toString ( 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);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    for (const auto& transition : pda.getLocalTransitions()) {
        std::string symbol;
 
        //input symbol
        if(transition.first.second.is_epsilon ( ) )
            symbol = "&epsilon";
        else
            symbol = replace ( factory::StringDataFactory::toString ( transition.first.second.getSymbol ( ) ), "\"", "\\\"" );
 
        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);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    for (const auto& transition : pda.getCallTransitions()) {
        std::string symbol;
 
        //input symbol
        if(transition.first.second.is_epsilon ( ) )
            symbol = "&epsilon";
        else
            symbol = replace ( factory::StringDataFactory::toString ( transition.first.second.getSymbol ( ) ), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        symbol += " &epsilon;";
        symbol += " ->";
 
        symbol += " " + replace ( factory::StringDataFactory::toString ( transition.second.second ), "\"", "\\\"" );
 
        //Insert into map
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(transition.second.first)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    for (const auto& transition : pda.getReturnTransitions()) {
        std::string symbol;
 
        //input symbol
        if(std::get<1>(transition.first).is_epsilon ( ) )
            symbol = "&epsilon;";
        else
            symbol = replace ( factory::StringDataFactory::toString ( std::get<1>(transition.first ).getSymbol ( ) ), "\"", "\\\"" );
 
        symbol += " |";
 
        //Pop part
        symbol += " " + replace ( factory::StringDataFactory::toString ( 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);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    for (const auto& transition : pda.getLocalTransitions()) {
        std::string symbol;
 
        //input symbol
        if(transition.first.second.is_epsilon ( ) )
            symbol = "&epsilon;";
        else
            symbol = replace ( factory::StringDataFactory::toString ( transition.first.second.getSymbol ( ) ), "\"", "\\\"" );
 
        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);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    for (const auto& transition : pda.getTransitions()) {
        std::string symbol;
 
        //input symbol
        if (std::get<1>(transition.first).is_epsilon ( ) ) {
            symbol = "&epsilon;";
        } else {
            symbol = replace ( factory::StringDataFactory::toString ( std::get<1>(transition.first ).getSymbol ( ) ), "\"", "\\\"" );
        }
 
        symbol += " |";
 
        //Pop part
        if (std::get<2>(transition.first).empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : std::get<2>(transition.first)) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        symbol += " ->";
 
        //Push part
        if (transition.second.second.empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : transition.second.second) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        //Insert into map
        std::pair<int, int> key(states.find(std::get<0>(transition.first))->second, states.find(transition.second.first)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void DotConverter::transitions(const automaton::SinglePopNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda, const ext::map<StateType, int>& states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
 
    for (const auto& transition : pda.getTransitions()) {
        std::string symbol;
 
        //input symbol
        if (std::get<1>(transition.first).is_epsilon ( )) {
            symbol = "&epsilon;";
        } else {
            symbol = replace ( factory::StringDataFactory::toString ( std::get<1>(transition.first ).getSymbol ( )), "\"", "\\\"" );
        }
 
        symbol += " |";
 
        //Pop part
        symbol += " " + replace ( factory::StringDataFactory::toString ( std::get<2>(transition.first )), "\"", "\\\"" );
 
        symbol += " ->";
 
        //Push part
        if (transition.second.second.empty ( )) {
            symbol += " &epsilon;";
        } else {
            for ( const PushdownStoreSymbolType & symb : transition.second.second) {
                symbol += " " + replace ( factory::StringDataFactory::toString ( symb ), "\"", "\\\"" );
            }
 
        }
 
        //Insert into map
        std::pair<int, int> key(states.find(std::get<0>(transition.first))->second, states.find(transition.second.first)->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
template < class SymbolType, class StateType >
void DotConverter::transitions(const automaton::OneTapeDTM < SymbolType, StateType > & tm, const ext::map < StateType, int > & states, ext::ostream& out) {
    ext::map<std::pair<int, int>, std::string> transitions;
    for (const auto& transition : tm.getTransitions()) {
        std::string symbol;
 
        //input symbol
        symbol = "(";
        symbol += replace ( factory::StringDataFactory::toString ( transition.first.second ), "\"", "\\\"" );
        symbol += ", ";
        symbol += replace ( factory::StringDataFactory::toString ( std::get<1>(transition.second )), "\"", "\\\"" );
        symbol += " ";
        switch(std::get<2>(transition.second)) {
        case automaton::Shift::LEFT:
            symbol += "&larr;";
            break;
        case automaton::Shift::RIGHT:
            symbol += "&rarr;";
            break;
        case automaton::Shift::NONE:
            symbol += "&times;";
            break;
        default:
            throw exception::CommonException("Unexpected shift direction");
        }
 
        //Insert into map
        std::pair<int, int> key(states.find(transition.first.first)->second, states.find(std::get<0>(transition.second))->second);
        ext::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 += ",";
 
            size_t pos = mapit->second.find_last_of("\n");
            if(pos == std::string::npos) pos = 0;
            if(mapit->second.size() - pos > CAPTION_LENGTH_LIMIT) mapit->second += "\n";
            else mapit->second += " ";
 
            mapit->second += symbol;
        }
    }
 
    //print the map
    for (std::pair<const std::pair<int, int>, std::string>& transition : transitions) {
        out << transition.first.first << " -> " << transition.first.second;
        replaceInplace(transition.second, "\n", "\\n");
        out << "[label=\"" << transition.second << "\"]\n";
    }
}
 
} /* namespace convert */