PDAToRHPDA.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 <automaton/PDA/RealTimeHeightDeterministicNPDA.h>
#include <automaton/PDA/RealTimeHeightDeterministicDPDA.h>
#include <automaton/PDA/NPDA.h>
#include <automaton/PDA/DPDA.h>
 
#include <alphabet/BottomOfTheStackSymbol.h>
 
#include <alib/set>
#include <label/InitialStateLabel.h>
#include <common/createUnique.hpp>
 
namespace automaton {
 
namespace transform {
 
class PDAToRHPDA {
public:
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > convert ( const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, ext::variant < StateType, std::string > > convert ( const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > convert ( const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda);
 
    template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
    static automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, ext::variant < StateType, std::string > > convert ( const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda);
};
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > PDAToRHPDA::convert ( const automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    return pda;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > PDAToRHPDA::convert ( const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    return pda;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, ext::variant < StateType, std::string > > PDAToRHPDA::convert ( const automaton::DPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    ext::variant < StateType, std::string > q0 = common::createUnique ( label::InitialStateLabel::instance < StateType > ( ), pda.getStates ( ) );
 
    RealTimeHeightDeterministicDPDA < InputSymbolType, PushdownStoreSymbolType, ext::variant < StateType, std::string > > res ( q0, alphabet::BottomOfTheStackSymbol::instance < InputSymbolType > ( ) );
 
    res.setInputAlphabet ( pda.getInputAlphabet ( ) );
 
    for ( const auto & state : pda.getStates ( ) )
        res.addState ( state );
    for ( const auto & state : pda.getFinalStates ( ) )
        res.addFinalState ( state );
 
    ext::set < InputSymbolType > pushdownStoreAlphabet = pda.getPushdownStoreAlphabet ( );
    pushdownStoreAlphabet.insert ( alphabet::BottomOfTheStackSymbol::instance < InputSymbolType > ( ) );
    res.setPushdownStoreAlphabet ( pushdownStoreAlphabet );
 
    res.addCallTransition ( q0, pda.getInitialState ( ), pda.getInitialSymbol ( ) );
 
    std::string us ( "us" );
    int i = 0;
 
    for ( const auto & transition : pda.getTransitions ( ) ) {
        const auto & to = transition.second;
 
        if ( ( std::get < 2 > ( transition.first ).empty ( ) ) && ( to.second.empty ( ) ) ) {
            res.addLocalTransition ( std::get < 0 > ( transition.first ), std::get < 1 > ( transition.first ), to.first );
        } else if ( ( std::get < 2 > ( transition.first ).size ( ) == 1 ) && ( to.second.empty ( ) ) ) {
            res.addReturnTransition ( std::get < 0 > ( transition.first ), std::get < 1 > ( transition.first ), std::get < 2 > ( transition.first )[0], to.first );
        } else if ( ( std::get < 2 > ( transition.first ).empty ( ) ) && ( to.second.size ( ) == 1 ) ) {
            res.addCallTransition ( std::get < 0 > ( transition.first ), std::get < 1 > ( transition.first ), to.first, to.second[0] );
        } else {
            int popPushIndex = 0;
            int popPushSymbols = std::get < 2 > ( transition.first ).size ( ) + to.second.size ( );
 
            ext::variant < StateType, std::string > lastUS = common::createUnique ( us + ext::to_string ( i ), res.getStates ( ) );
            for ( const InputSymbolType & pop :std::get < 2 > ( transition.first ) ) {
                ext::variant < StateType, std::string > fromState = ( popPushIndex == 0 ) ? ext::variant < StateType, std::string > ( std::get < 0 > ( transition.first ) ) : ext::variant < StateType, std::string > ( lastUS );
 
                if ( popPushIndex != 0 ) lastUS = common::createUnique ( us + ext::to_string ( ++i ), res.getStates ( ) );
 
                ext::variant < StateType, std::string > toState = ( popPushIndex == popPushSymbols - 1 ) ? ext::variant < StateType, std::string > ( to.first ) : ext::variant < StateType, std::string > ( lastUS );
 
                res.addState ( fromState );
                res.addState ( toState );
 
                if ( popPushIndex == 0 )
                    res.addReturnTransition ( fromState, std::get < 1 > ( transition.first ), pop, toState );
                else
                    res.addReturnTransition ( fromState, pop, toState );
 
                popPushIndex++;
            }
            for ( const InputSymbolType & push : ext::make_reverse ( to.second ) ) {
                ext::variant < StateType, std::string > fromState = ( popPushIndex == 0 ) ? ext::variant < StateType, std::string > ( std::get < 0 > ( transition.first ) ) : ext::variant < StateType, std::string > ( lastUS );
 
                if ( popPushIndex != 0 ) lastUS = common::createUnique ( us + ext::to_string ( ++i ), res.getStates ( ) );
 
                ext::variant < StateType, std::string > toState = ( popPushIndex == popPushSymbols - 1 ) ? ext::variant < StateType, std::string > ( to.first ) : ext::variant < StateType, std::string > ( lastUS );
 
                res.addState ( fromState );
                res.addState ( toState );
 
                if ( popPushIndex == 0 )
                    res.addCallTransition ( fromState, std::get < 1 > ( transition.first ), toState, push );
                else
                    res.addCallTransition ( fromState, toState, push );
 
                popPushIndex++;
            }
        }
    }
 
    return res;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, ext::variant < StateType, std::string > > PDAToRHPDA::convert ( const automaton::NPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & pda ) {
    RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, ext::variant < StateType, std::string > > res ( alphabet::BottomOfTheStackSymbol::instance < DefaultSymbolType > ( ) );
 
    res.setInputAlphabet ( pda.getInputAlphabet ( ) );
 
    for ( const auto & state : pda.getStates ( ) )
        res.addState ( state );
    for ( const auto & state : pda.getFinalStates ( ) )
        res.addFinalState ( state );
 
    ext::set < InputSymbolType > pushdownStoreAlphabet = pda.getPushdownStoreAlphabet ( );
    pushdownStoreAlphabet.insert ( alphabet::BottomOfTheStackSymbol::instance < InputSymbolType > ( ) );
    res.setPushdownStoreAlphabet ( pushdownStoreAlphabet );
 
    StateType q0 = common::createUnique ( label::InitialStateLabel::instance < StateType > ( ), res.getStates ( ) );
    res.addState ( q0 );
    res.addInitialState ( q0 );
 
    res.addCallTransition ( q0, pda.getInitialState ( ), pda.getInitialSymbol ( ) );
 
    std::string us ( "us" );
    int i = 0;
 
    for ( const auto & transition : pda.getTransitions ( ) )
        if ( ( std::get < 2 > ( transition.first ).empty ( ) ) && ( transition.second.second.empty ( ) ) ) {
            res.addLocalTransition ( std::get < 0 > ( transition.first ), std::get < 1 > ( transition.first ), transition.second.first );
        } else if ( ( std::get < 2 > ( transition.first ).size ( ) == 1 ) && ( transition.second.second.empty ( ) ) ) {
            res.addReturnTransition ( std::get < 0 > ( transition.first ), std::get < 1 > ( transition.first ), std::get < 2 > ( transition.first )[0], transition.second.first );
        } else if ( ( std::get < 2 > ( transition.first ).empty ( ) ) && ( transition.second.second.size ( ) == 1 ) ) {
            res.addCallTransition ( std::get < 0 > ( transition.first ), std::get < 1 > ( transition.first ), transition.second.first, transition.second.second[0] );
        } else {
            int popPushIndex = 0;
            int popPushSymbols = std::get < 2 > ( transition.first ).size ( ) + transition.second.second.size ( );
 
            std::string lastUS = common::createUnique ( us + ext::to_string ( i ), res.getStates ( ) );
            std::for_each ( std::get < 2 > ( transition.first ).begin ( ), std::get < 2 > ( transition.first ).end ( ), [&] ( const InputSymbolType & pop ) {
                    ext::variant < StateType, std::string > fromState = ( popPushIndex == 0 ) ? ext::variant < StateType, std::string > ( std::get < 0 > ( transition.first ) ) : ext::variant < StateType, std::string > ( lastUS );
 
                    if ( popPushIndex != 0 ) lastUS = common::createUnique ( us + ext::to_string ( ++i ), res.getStates ( ) );
 
                    ext::variant < StateType, std::string > toState = ( popPushIndex == popPushSymbols - 1 ) ? ext::variant < StateType, std::string > ( transition.second.first ) : ext::variant < StateType, std::string > ( lastUS );
 
                    res.addState ( fromState );
                    res.addState ( toState );
 
                    if ( popPushIndex == 0 )
                        res.addReturnTransition ( fromState, std::get < 1 > ( transition.first ), pop, toState );
                    else
                        res.addReturnTransition ( fromState, pop, toState );
 
                    popPushIndex++;
                } );
            std::for_each ( transition.second.second.rbegin ( ), transition.second.second.rend ( ), [&] ( const InputSymbolType & push ) {
                    ext::variant < StateType, std::string > fromState = ( popPushIndex == 0 ) ? ext::variant < StateType, std::string > ( std::get < 0 > ( transition.first ) ) : ext::variant < StateType, std::string > ( lastUS );
 
                    if ( popPushIndex != 0 ) lastUS = common::createUnique ( us + ext::to_string ( ++i ), res.getStates ( ) );
 
                    ext::variant < StateType, std::string > toState = ( popPushIndex == popPushSymbols - 1 ) ? ext::variant < StateType, std::string > ( transition.second.first ) : ext::variant < StateType, std::string > ( lastUS );
 
                    res.addState ( fromState );
                    res.addState ( toState );
 
                    if ( popPushIndex == 0 )
                        res.addCallTransition ( fromState, std::get < 1 > ( transition.first ), toState, push );
                    else
                        res.addCallTransition ( fromState, toState, push );
 
                    popPushIndex++;
                } );
        }
 
    return res;
}
 
} /* namespace transform */
 
} /* namespace automaton */