Rename.h

Go to the documentation of this file.

 
/*
 * This file is part of Algorithms library toolkit.
 * Copyright (C) 2017 Jan Travnicek (jan.travnicek@fit.cvut.cz)
 
 * Algorithms library toolkit is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 
 * Algorithms library toolkit is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 
 * You should have received a copy of the GNU General Public License
 * along with Algorithms library toolkit.  If not, see <http://www.gnu.org/licenses/>.
 */
 
#pragma once
 
#include <ext/algorithm>
 
#include <alib/map>
#include <alib/vector>
 
#include <automaton/FSM/DFA.h>
#include <automaton/FSM/NFA.h>
#include <automaton/FSM/EpsilonNFA.h>
#include <automaton/TA/DFTA.h>
#include <automaton/TA/NFTA.h>
#include <automaton/TA/ArcFactoredNondeterministicZAutomaton.h>
#include <automaton/TA/ArcFactoredDeterministicZAutomaton.h>
#include <automaton/PDA/DPDA.h>
#include <automaton/PDA/NPDA.h>
#include <automaton/PDA/InputDrivenDPDA.h>
#include <automaton/PDA/RealTimeHeightDeterministicDPDA.h>
#include <automaton/PDA/SinglePopDPDA.h>
#include <automaton/PDA/VisiblyPushdownDPDA.h>
 
namespace automaton {
 
namespace simplify {
 
class Rename {
    template < class T >
    struct DFATra {
        using type = automaton::DFA < typename T::SymbolType, unsigned >;
    };
 
    template < class T >
    struct NFATra {
        using type = automaton::NFA < typename T::SymbolType, unsigned >;
    };
 
    template < class T >
    struct EpsilonNFATra {
        using type = automaton::EpsilonNFA < typename T::SymbolType, unsigned >;
    };
 
    template < class T >
    using RenamedAutomaton = typename ext::casional <
            ext::boolean < isDFA < T > >, DFATra < T >,
            ext::boolean < isNFA < T > >, NFATra < T >,
            ext::boolean < isEpsilonNFA < T > >, EpsilonNFATra < T >
        >::type::type;
 
    template < class T >
    struct DFTATra {
        using type = automaton::DFTA < typename T::SymbolType, unsigned >;
    };
 
    template < class T >
    struct NFTATra {
        using type = automaton::NFTA < typename T::SymbolType, unsigned >;
    };
 
    template < class T >
    using RenamedTreeAutomaton = typename ext::casional <
            ext::boolean < isDFTA < T > >, DFTATra < T >,
            ext::boolean < isNFTA < T > >, NFTATra < T >
        >::type::type;
 
public:
    template < class T >
    requires isDFA < T > || isNFA < T >
    static Rename::RenamedAutomaton < T > rename ( const T & fsm );
 
    template < class T >
    requires isDFTA < T > || isNFTA < T >
    static Rename::RenamedTreeAutomaton < T > rename ( const T & fta );
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::DPDA < InputSymbolType, unsigned, unsigned > rename ( const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda );
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::NPDA < InputSymbolType, unsigned, unsigned > rename ( const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda );
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::SinglePopDPDA < InputSymbolType, unsigned, unsigned > rename ( const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda );
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::InputDrivenDPDA < InputSymbolType, unsigned, unsigned > rename ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda );
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::VisiblyPushdownDPDA < InputSymbolType, unsigned, unsigned > rename ( const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda );
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, unsigned, unsigned > rename ( const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda );
 
    template < class InputSymbolType, class StateType >
    static automaton::ArcFactoredNondeterministicZAutomaton < InputSymbolType, unsigned > rename ( const automaton::ArcFactoredNondeterministicZAutomaton < InputSymbolType, StateType > & a );
 
    template < class InputSymbolType, class StateType >
    static automaton::ArcFactoredDeterministicZAutomaton < InputSymbolType, unsigned > rename ( const automaton::ArcFactoredDeterministicZAutomaton < InputSymbolType, StateType > & a );
};
 
template < class T >
requires isDFA < T > || isNFA < T >
Rename::RenamedAutomaton < T > Rename::rename ( const T & fsm ) {
    using StateType = typename T::StateType;
 
    unsigned counter = 0;
    ext::map < StateType, unsigned > renamingData;
 
    for ( const StateType & state : fsm.getStates ( ) )
        renamingData.insert ( std::make_pair ( state, counter++ ) );
 
    Rename::RenamedAutomaton < T > result ( renamingData.at ( fsm.getInitialState ( ) ) );
 
    result.setInputAlphabet ( fsm.getInputAlphabet ( ) );
 
    for ( const StateType & state : fsm.getStates ( ) )
        result.addState ( renamingData.at ( state ) );
 
    for ( const StateType & state : fsm.getFinalStates ( ) )
        result.addFinalState ( renamingData.at ( state ) );
 
    for ( const auto & transition : fsm.getTransitions ( ) )
        result.addTransition ( renamingData.at ( transition.first.first ), transition.first.second, renamingData.at ( transition.second ) );
 
    return result;
}
 
template < class T >
requires isDFTA < T > || isNFTA < T >
Rename::RenamedTreeAutomaton < T > Rename::rename ( const T & fta ) {
    using StateType = typename T::StateType;
 
    unsigned counter = 0;
    ext::map < StateType, unsigned > renamingData;
 
    for ( const StateType & state : fta.getStates ( ) )
        renamingData.insert ( std::make_pair ( state, counter++ ) );
 
    Rename::RenamedTreeAutomaton < T > result;
 
    result.setInputAlphabet ( fta.getInputAlphabet ( ) );
 
    for ( const StateType & state : fta.getStates ( ) )
        result.addState ( renamingData.at ( state ) );
 
    for ( const StateType & state : fta.getFinalStates ( ) )
        result.addFinalState ( renamingData.at ( state ) );
 
    for ( const auto & transition : fta.getTransitions ( ) ) {
        ext::vector < unsigned > sourceStates;
 
        for ( const StateType & source : transition.first.second )
            sourceStates.push_back ( renamingData.at ( source ) );
 
        result.addTransition ( transition.first.first, sourceStates, renamingData.at ( transition.second ) );
    }
 
    return result;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::DPDA < InputSymbolType, unsigned, unsigned > Rename::rename ( const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    unsigned counterState = 0;
    ext::map < StateType, unsigned > renamingDataState;
    unsigned counterSymbol = 0;
    ext::map < InputSymbolType, unsigned > renamingDataSymbol;
 
    for ( const StateType & state : pda.getStates ( ) )
        renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
 
    automaton::DPDA < InputSymbolType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getInitialSymbol ( ) ) );
 
    result.setInputAlphabet ( pda.getInputAlphabet ( ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
 
    for ( const StateType & state : pda.getStates ( ) )
        result.addState ( renamingDataState.at ( state ) );
 
    for ( const StateType & state : pda.getFinalStates ( ) )
        result.addFinalState ( renamingDataState.at ( state ) );
 
    for ( const auto & transition : pda.getTransitions ( ) ) {
        ext::vector < unsigned > pop;
 
        for ( const InputSymbolType & symbol : std::get < 2 > ( transition.first ) )
            pop.push_back ( renamingDataSymbol.at ( symbol ) );
 
        ext::vector < unsigned > push;
 
        for ( const InputSymbolType & symbol : transition.second.second )
            push.push_back ( renamingDataSymbol.at ( symbol ) );
 
        result.addTransition ( renamingDataState.at ( std::get < 0 > ( transition.first ) ), std::get < 1 > ( transition.first ), pop, renamingDataState.at ( transition.second.first ), push );
    }
 
    return result;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::NPDA < InputSymbolType, unsigned, unsigned > Rename::rename ( const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    unsigned counterState = 0;
    ext::map < StateType, unsigned > renamingDataState;
    unsigned counterSymbol = 0;
    ext::map < InputSymbolType, unsigned > renamingDataSymbol;
 
    for ( const StateType & state : pda.getStates ( ) )
        renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
 
    automaton::NPDA < InputSymbolType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getInitialSymbol ( ) ) );
 
    result.setInputAlphabet ( pda.getInputAlphabet ( ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
 
    for ( const StateType & state : pda.getStates ( ) )
        result.addState ( renamingDataState.at ( state ) );
 
    for ( const StateType & state : pda.getFinalStates ( ) )
        result.addFinalState ( renamingDataState.at ( state ) );
 
    for ( const auto & transition : pda.getTransitions ( ) ) {
        ext::vector < unsigned > pop;
        for ( const InputSymbolType & symbol : std::get < 2 > ( transition.first ) )
            pop.push_back ( renamingDataSymbol.at ( symbol ) );
 
        ext::vector < unsigned > push;
        for ( const InputSymbolType & symbol : transition.second.second )
            push.push_back ( renamingDataSymbol.at ( symbol ) );
 
        result.addTransition ( renamingDataState.at ( std::get < 0 > ( transition.first ) ), std::get < 1 > ( transition.first ), pop, renamingDataState.at ( transition.second.first ), push );
    }
 
    return result;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::SinglePopDPDA < InputSymbolType, unsigned, unsigned > Rename::rename ( const automaton::SinglePopDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    int counterState = 0;
    ext::map < StateType, unsigned > renamingDataState;
    int counterSymbol = 0;
    ext::map < InputSymbolType, unsigned > renamingDataSymbol;
 
    for ( const StateType & state : pda.getStates ( ) )
        renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
 
    automaton::SinglePopDPDA < InputSymbolType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getInitialSymbol ( ) ) );
 
    result.setInputAlphabet ( pda.getInputAlphabet ( ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
 
    for ( const StateType & state : pda.getStates ( ) )
        result.addState ( renamingDataState.at ( state ) );
 
    for ( const StateType & state : pda.getFinalStates ( ) )
        result.addFinalState ( renamingDataState.at ( state ) );
 
    for ( const auto & transition : pda.getTransitions ( ) ) {
        ext::vector < unsigned > push;
 
        for ( const PushdownStoreSymbolType & symbol : transition.second.second )
            push.push_back ( renamingDataSymbol.at ( symbol ) );
 
        result.addTransition ( renamingDataState.at ( std::get < 0 > ( transition.first ) ), std::get < 1 > ( transition.first ), renamingDataSymbol.at ( std::get < 2 > ( transition.first ) ), renamingDataState.at ( transition.second.first ), push );
    }
 
    return result;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::InputDrivenDPDA < InputSymbolType, unsigned, unsigned > Rename::rename ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    int counterState = 0;
    ext::map < StateType, unsigned > renamingDataState;
    int counterSymbol = 0;
    ext::map < InputSymbolType, unsigned > renamingDataSymbol;
 
    for ( const StateType & state : pda.getStates ( ) )
        renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
 
    automaton::InputDrivenDPDA < InputSymbolType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getInitialSymbol ( ) ) );
 
    result.setInputAlphabet ( pda.getInputAlphabet ( ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
 
    for ( const std::pair < const InputSymbolType, ext::pair < ext::vector < PushdownStoreSymbolType >, ext::vector < PushdownStoreSymbolType > > > & operation : pda.getPushdownStoreOperations ( ) ) {
        ext::vector < unsigned > pop;
 
        for ( const PushdownStoreSymbolType & symbol : operation.second.first )
            pop.push_back ( renamingDataSymbol.at ( symbol ) );
 
        ext::vector < unsigned > push;
 
        for ( const PushdownStoreSymbolType & symbol : operation.second.second )
            push.push_back ( renamingDataSymbol.at ( symbol ) );
 
        result.setPushdownStoreOperation ( operation.first, pop, push );
    }
 
    for ( const StateType & state : pda.getStates ( ) )
        result.addState ( renamingDataState.at ( state ) );
 
    for ( const StateType & state : pda.getFinalStates ( ) )
        result.addFinalState ( renamingDataState.at ( state ) );
 
    for ( const auto & transition : pda.getTransitions ( ) )
        result.addTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second ) );
 
    return result;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::VisiblyPushdownDPDA < InputSymbolType, unsigned, unsigned > Rename::rename ( const automaton::VisiblyPushdownDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    int counterState = 0;
    ext::map < StateType, unsigned > renamingDataState;
    int counterSymbol = 0;
    ext::map < InputSymbolType, unsigned > renamingDataSymbol;
 
    for ( const StateType & state : pda.getStates ( ) )
        renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
 
    automaton::VisiblyPushdownDPDA < InputSymbolType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getBottomOfTheStackSymbol ( ) ) );
 
    result.setCallInputAlphabet ( pda.getCallInputAlphabet ( ) );
    result.setLocalInputAlphabet ( pda.getLocalInputAlphabet ( ) );
    result.setReturnInputAlphabet ( pda.getReturnInputAlphabet ( ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
 
    for ( const StateType & state : pda.getStates ( ) )
        result.addState ( renamingDataState.at ( state ) );
 
    for ( const StateType & state : pda.getFinalStates ( ) )
        result.addFinalState ( renamingDataState.at ( state ) );
 
    for ( const auto & transition : pda.getCallTransitions ( ) )
        result.addCallTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second.first ), renamingDataSymbol.at ( transition.second.second ) );
 
    for ( const auto & transition : pda.getLocalTransitions ( ) )
        result.addLocalTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second ) );
 
    for ( const auto & transition : pda.getReturnTransitions ( ) )
        result.addReturnTransition ( renamingDataState.at ( std::get < 0 > ( transition.first ) ), std::get < 1 > ( transition.first ), renamingDataSymbol.at ( std::get < 2 > ( transition.first ) ), renamingDataState.at ( transition.second ) );
 
    return result;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, unsigned, unsigned > Rename::rename ( const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    int counterState = 0;
    ext::map < StateType, unsigned > renamingDataState;
    int counterSymbol = 0;
    ext::map < InputSymbolType, unsigned > renamingDataSymbol;
 
    for ( const StateType & state : pda.getStates ( ) )
        renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        renamingDataSymbol.insert ( std::make_pair ( symbol, counterSymbol++ ) );
 
    automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, unsigned, unsigned > result ( renamingDataState.at ( pda.getInitialState ( ) ), renamingDataSymbol.at ( pda.getBottomOfTheStackSymbol ( ) ) );
 
    result.setInputAlphabet ( pda.getInputAlphabet ( ) );
 
    for ( const InputSymbolType & symbol : pda.getPushdownStoreAlphabet ( ) )
        result.addPushdownStoreSymbol ( renamingDataSymbol.at ( symbol ) );
 
    for ( const StateType & state : pda.getStates ( ) )
        result.addState ( renamingDataState.at ( state ) );
 
    for ( const StateType & state : pda.getFinalStates ( ) )
        result.addFinalState ( renamingDataState.at ( state ) );
 
    for ( const auto & transition : pda.getCallTransitions ( ) )
        result.addCallTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second.first ), renamingDataSymbol.at ( transition.second.second ) );
 
    for ( const auto & transition : pda.getLocalTransitions ( ) )
        result.addLocalTransition ( renamingDataState.at ( transition.first.first ), transition.first.second, renamingDataState.at ( transition.second ) );
 
    for ( const auto & transition : pda.getReturnTransitions ( ) )
        result.addReturnTransition ( renamingDataState.at ( std::get < 0 > ( transition.first ) ), std::get < 1 > ( transition.first ), renamingDataSymbol.at ( std::get < 2 > ( transition.first ) ), renamingDataState.at ( transition.second ) );
 
    return result;
}
 
template < class SymbolType, class StateType >
automaton::ArcFactoredNondeterministicZAutomaton < SymbolType, unsigned > Rename::rename ( const automaton::ArcFactoredNondeterministicZAutomaton < SymbolType, StateType > & a ) {
    int counterState = 0;
    ext::map < StateType, unsigned > renamingDataState;
 
    for ( const StateType & state : a.getStates ( ) )
        renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
 
    automaton::ArcFactoredNondeterministicZAutomaton < SymbolType, unsigned > result;
 
    result.setInputAlphabet ( a.getInputAlphabet ( ) );
 
    for ( const StateType & state : a.getStates ( ) )
        result.addState ( renamingDataState.at ( state ) );
 
    for ( const StateType & state : a.getFinalStates ( ) )
        result.addFinalState ( renamingDataState.at ( state ) );
 
    for ( const std::pair < const ext::variant < SymbolType, ext::pair < StateType, StateType > >, StateType > & transition : a.getTransitions ( ) ) {
        if ( transition.first.template is < SymbolType > ( ) ) {
            result.addTransition ( transition.first.template get < SymbolType > ( ), renamingDataState.at ( transition.second ) );
        } else {
            auto source = transition.first.template get < ext::pair < StateType, StateType > > ( );
            result.addTransition ( ext::make_pair ( renamingDataState.at ( source.first ), renamingDataState.at ( source.second ) ), renamingDataState.at ( transition.second ) );
        }
    }
 
    return result;
}
 
template < class SymbolType, class StateType >
automaton::ArcFactoredDeterministicZAutomaton < SymbolType, unsigned > Rename::rename ( const automaton::ArcFactoredDeterministicZAutomaton < SymbolType, StateType > & a ) {
    int counterState = 0;
    ext::map < StateType, unsigned > renamingDataState;
 
    for ( const StateType & state : a.getStates ( ) )
        renamingDataState.insert ( std::make_pair ( state, counterState++ ) );
 
    automaton::ArcFactoredDeterministicZAutomaton < SymbolType, unsigned > result;
 
    result.setInputAlphabet ( a.getInputAlphabet ( ) );
 
    for ( const StateType & state : a.getStates ( ) )
        result.addState ( renamingDataState.at ( state ) );
 
    for ( const StateType & state : a.getFinalStates ( ) )
        result.addFinalState ( renamingDataState.at ( state ) );
 
    for ( const std::pair < const ext::variant < SymbolType, ext::pair < StateType, StateType > >, StateType > & transition : a.getTransitions ( ) ) {
        if ( transition.first.template is < SymbolType > ( ) ) {
            result.addTransition ( transition.first.template get < SymbolType > ( ), renamingDataState.at ( transition.second ) );
        } else {
            auto source = transition.first.template get < ext::pair < StateType, StateType > > ( );
            result.addTransition ( ext::make_pair ( renamingDataState.at ( source.first ), renamingDataState.at ( source.second ) ), renamingDataState.at ( transition.second ) );
        }
    }
 
    return result;
}
 
} /* namespace simplify */
 
} /* namespace automaton */