AutomatonDiff.h

Go to the documentation of this file.

 
#pragma once
 
#include <ostream>
 
#include <ext/iostream>
#include <ext/utility>
 
#include <compare/DiffAux.h>
#include <compare/AutomatonCompare.h>
 
#include <alib/set>
#include <alib/list>
#include <alib/map>
#include <alib/vector>
 
#include "automaton/FSM/DFA.h"
#include "automaton/FSM/NFA.h"
#include "automaton/FSM/MultiInitialStateNFA.h"
#include "automaton/FSM/EpsilonNFA.h"
#include "automaton/FSM/ExtendedNFA.h"
#include "automaton/FSM/CompactDFA.h"
#include "automaton/FSM/CompactNFA.h"
#include "automaton/TA/DFTA.h"
#include "automaton/TA/NFTA.h"
#include "automaton/PDA/NPDA.h"
#include "automaton/PDA/DPDA.h"
#include "automaton/PDA/InputDrivenNPDA.h"
#include "automaton/PDA/InputDrivenDPDA.h"
#include "automaton/PDA/VisiblyPushdownNPDA.h"
#include "automaton/PDA/VisiblyPushdownDPDA.h"
#include "automaton/PDA/RealTimeHeightDeterministicNPDA.h"
#include "automaton/PDA/RealTimeHeightDeterministicDPDA.h"
#include "automaton/PDA/SinglePopNPDA.h"
#include "automaton/PDA/SinglePopDPDA.h"
#include "automaton/TM/OneTapeDTM.h"
 
namespace compare {
 
class AutomatonDiff {
private:
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::DFA < SymbolType, StateType > & a, const automaton::DFA < SymbolType, StateType > & b, ext::ostream & out );
 
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::NFA < SymbolType, StateType > & a, const automaton::NFA < SymbolType, StateType > & b, ext::ostream & out );
 
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::MultiInitialStateNFA < SymbolType, StateType > & a, const automaton::MultiInitialStateNFA < SymbolType, StateType > & b, ext::ostream & out );
 
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::EpsilonNFA < SymbolType, StateType > & a, const automaton::EpsilonNFA < SymbolType, StateType > & b, ext::ostream & out );
 
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::ExtendedNFA < SymbolType, StateType > & a, const automaton::ExtendedNFA < SymbolType, StateType > & b, ext::ostream & out );
 
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::CompactDFA < SymbolType, StateType > & a, const automaton::CompactDFA < SymbolType, StateType > & b, ext::ostream & out );
 
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::CompactNFA < SymbolType, StateType > & a, const automaton::CompactNFA < SymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::DFTA < SymbolType, StateType > & a, const automaton::DFTA < SymbolType, StateType > & b, ext::ostream & out );
 
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::NFTA < SymbolType, StateType > & a, const automaton::NFTA < SymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::InputDrivenNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::InputDrivenNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
    static void printDiff(const automaton::SinglePopNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::SinglePopNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out );
 
    template<class SymbolType, class StateType>
    static void printDiff(const automaton::OneTapeDTM < SymbolType, StateType > & a, const automaton::OneTapeDTM < SymbolType, StateType > & b, ext::ostream & out );
public:
    template<class T>
    static void diff(const T & a, const T & b, ext::ostream & out );
 
    template < class T >
    static std::string diff ( const T & a, const T & b );
};
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::DFA < SymbolType, StateType > & a, const automaton::DFA < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::MultiInitialStateNFA < SymbolType, StateType > & a, const automaton::MultiInitialStateNFA < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialStates() != b.getInitialStates()) {
        out << "InitialStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getInitialStates(), b.getInitialStates());
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::NFA < SymbolType, StateType > & a, const automaton::NFA < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::EpsilonNFA < SymbolType, StateType > & a, const automaton::EpsilonNFA < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::CompactDFA < SymbolType, StateType > & a, const automaton::CompactDFA < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::ExtendedNFA < SymbolType, StateType > & a, const automaton::ExtendedNFA < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::CompactNFA < SymbolType, StateType > & a, const automaton::CompactNFA < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::DFTA < SymbolType, StateType > & a, const automaton::DFTA < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::NFTA < SymbolType, StateType > & a, const automaton::NFTA < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getInitialSymbol() != b.getInitialSymbol()) {
        out << "InitialSymbol" << std::endl;
 
        out << "< " << a.getInitialSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getInitialSymbol() != b.getInitialSymbol()) {
        out << "InitialSymbol" << std::endl;
 
        out << "< " << a.getInitialSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getInitialSymbol() != b.getInitialSymbol()) {
        out << "InitialSymbol" << std::endl;
 
        out << "< " << a.getInitialSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getPushdownStoreOperations() != b.getPushdownStoreOperations()) {
        out << "PushdownStoreOperations" << std::endl;
 
        DiffAux::mapDiff ( out, a.getPushdownStoreOperations(), b.getPushdownStoreOperations());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::InputDrivenNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::InputDrivenNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getInitialSymbol() != b.getInitialSymbol()) {
        out << "InitialSymbol" << std::endl;
 
        out << "< " << a.getInitialSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getPushdownStoreOperations() != b.getPushdownStoreOperations()) {
        out << "PushdownStoreOperations" << std::endl;
 
        DiffAux::mapDiff ( out, a.getPushdownStoreOperations(), b.getPushdownStoreOperations());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getCallInputAlphabet() != b.getCallInputAlphabet()) {
        out << "CallInputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getCallInputAlphabet(), b.getCallInputAlphabet());
    }
 
    if(a.getReturnInputAlphabet() != b.getReturnInputAlphabet()) {
        out << "ReturnInputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getReturnInputAlphabet(), b.getReturnInputAlphabet());
    }
 
    if(a.getLocalInputAlphabet() != b.getLocalInputAlphabet()) {
        out << "LocalInputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getLocalInputAlphabet(), b.getLocalInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getBottomOfTheStackSymbol() != b.getBottomOfTheStackSymbol()) {
        out << "BottomOfTheStackSymbol" << std::endl;
 
        out << "< " << a.getBottomOfTheStackSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getBottomOfTheStackSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getCallTransitions() != b.getCallTransitions()) {
        out << "CallTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getCallTransitions(), b.getCallTransitions());
    }
 
    if(a.getReturnTransitions() != b.getReturnTransitions()) {
        out << "ReturnTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getReturnTransitions(), b.getReturnTransitions());
    }
 
    if(a.getLocalTransitions() != b.getLocalTransitions()) {
        out << "LocalTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getLocalTransitions(), b.getLocalTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialStates() != b.getInitialStates()) {
        out << "Initial states" << std::endl;
 
        DiffAux::setDiff ( out, a.getInitialStates(), b.getInitialStates());
    }
 
    if(a.getCallInputAlphabet() != b.getCallInputAlphabet()) {
        out << "CallInputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getCallInputAlphabet(), b.getCallInputAlphabet());
    }
 
    if(a.getReturnInputAlphabet() != b.getReturnInputAlphabet()) {
        out << "ReturnInputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getReturnInputAlphabet(), b.getReturnInputAlphabet());
    }
 
    if(a.getLocalInputAlphabet() != b.getLocalInputAlphabet()) {
        out << "LocalInputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getLocalInputAlphabet(), b.getLocalInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getBottomOfTheStackSymbol() != b.getBottomOfTheStackSymbol()) {
        out << "BottomOfTheStackSymbol" << std::endl;
 
        out << "< " << a.getBottomOfTheStackSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getBottomOfTheStackSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getCallTransitions() != b.getCallTransitions()) {
        out << "CallTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getCallTransitions(), b.getCallTransitions());
    }
 
    if(a.getReturnTransitions() != b.getReturnTransitions()) {
        out << "ReturnTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getReturnTransitions(), b.getReturnTransitions());
    }
 
    if(a.getLocalTransitions() != b.getLocalTransitions()) {
        out << "LocalTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getLocalTransitions(), b.getLocalTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getBottomOfTheStackSymbol() != b.getBottomOfTheStackSymbol()) {
        out << "BottomOfTheStackSymbol" << std::endl;
 
        out << "< " << a.getBottomOfTheStackSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getBottomOfTheStackSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getCallTransitions() != b.getCallTransitions()) {
        out << "CallTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getCallTransitions(), b.getCallTransitions());
    }
 
    if(a.getReturnTransitions() != b.getReturnTransitions()) {
        out << "ReturnTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getReturnTransitions(), b.getReturnTransitions());
    }
 
    if(a.getLocalTransitions() != b.getLocalTransitions()) {
        out << "LocalTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getLocalTransitions(), b.getLocalTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialStates() != b.getInitialStates()) {
        out << "Initial states" << std::endl;
 
        DiffAux::setDiff ( out, a.getInitialStates(), b.getInitialStates());
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getBottomOfTheStackSymbol() != b.getBottomOfTheStackSymbol()) {
        out << "BottomOfTheStackSymbol" << std::endl;
 
        out << "< " << a.getBottomOfTheStackSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getBottomOfTheStackSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getCallTransitions() != b.getCallTransitions()) {
        out << "CallTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getCallTransitions(), b.getCallTransitions());
    }
 
    if(a.getReturnTransitions() != b.getReturnTransitions()) {
        out << "ReturnTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getReturnTransitions(), b.getReturnTransitions());
    }
 
    if(a.getLocalTransitions() != b.getLocalTransitions()) {
        out << "LocalTransitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getLocalTransitions(), b.getLocalTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getInitialSymbol() != b.getInitialSymbol()) {
        out << "InitialSymbol" << std::endl;
 
        out << "< " << a.getInitialSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class InputSymbolType, class PushdownStoreSymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::SinglePopNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & a, const automaton::SinglePopNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getPushdownStoreAlphabet() != b.getPushdownStoreAlphabet()) {
        out << "StackAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getPushdownStoreAlphabet(), b.getPushdownStoreAlphabet());
    }
 
    if(a.getInitialSymbol() != b.getInitialSymbol()) {
        out << "InitialSymbol" << std::endl;
 
        out << "< " << a.getInitialSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialSymbol() << std::endl;
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template<class SymbolType, class StateType>
void AutomatonDiff::printDiff(const automaton::OneTapeDTM < SymbolType, StateType > & a, const automaton::OneTapeDTM < SymbolType, StateType > & b, ext::ostream & out ) {
    out << "AutomataComparer" << std::endl;
 
    if(a.getBlankSymbol() != b.getBlankSymbol()) {
        out << "Blank symbol" << std::endl;
 
        out << "< " << a.getBlankSymbol() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getBlankSymbol() << std::endl;
    }
 
    if(a.getFinalStates() != b.getFinalStates()){
        out << "FinalStates" << std::endl;
 
        DiffAux::setDiff ( out, a.getFinalStates(), b.getFinalStates());
    }
 
    if(a.getInitialState() != b.getInitialState()) {
        out << "Initial state" << std::endl;
 
        out << "< " << a.getInitialState() << std::endl;
        out << "---" << std::endl;
        out << "> " << b.getInitialState() << std::endl;
    }
 
    if(a.getInputAlphabet() != b.getInputAlphabet()) {
        out << "InputAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getInputAlphabet(), b.getInputAlphabet());
    }
 
    if(a.getStates() != b.getStates()) {
        out << "States" << std::endl;
 
        DiffAux::setDiff ( out, a.getStates(), b.getStates());
    }
 
    if(a.getTapeAlphabet() != b.getTapeAlphabet()) {
        out << "TapeAlphabet" << std::endl;
 
        DiffAux::setDiff ( out, a.getTapeAlphabet(), b.getTapeAlphabet());
    }
 
    if(a.getTransitions() != b.getTransitions()) {
        out << "Transitions" << std::endl;
 
        DiffAux::mapDiff ( out, a.getTransitions(), b.getTransitions());
    }
}
 
template < class T>
void AutomatonDiff::diff(const T & a, const T & b, ext::ostream & out) {
    if(!AutomatonCompare::compare(a, b)) {
        AutomatonDiff::printDiff(a, b, out);
    }
}
 
template < class T >
std::string AutomatonDiff::diff ( const T & a, const T & b ) {
    ext::ostringstream ss;
    diff ( a, b, ss );
    return ss.str ( );
}
 
} /* namespace compare */