ToPrefixPushdownAutomaton.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/TA/ArcFactoredDeterministicZAutomaton.h>
#include <automaton/TA/ArcFactoredNondeterministicZAutomaton.h>
#include <automaton/PDA/NPDA.h>
#include <automaton/PDA/DPDA.h>
 
#include <alphabet/BottomOfTheStackSymbol.h>
#include <alphabet/BarSymbol.h>
 
namespace automaton {
 
namespace convert {
 
class ToPrefixPushdownAutomaton {
public:
    template < class SymbolType, class StateType >
    static automaton::DPDA < SymbolType, ext::variant < StateType, alphabet::BottomOfTheStackSymbol >, char > convert ( const automaton::ArcFactoredDeterministicZAutomaton < SymbolType, StateType > & afdza );
 
    template < class SymbolType, class StateType >
    static automaton::NPDA < SymbolType, ext::variant < StateType, alphabet::BottomOfTheStackSymbol >, char > convert ( const automaton::ArcFactoredNondeterministicZAutomaton < SymbolType, StateType > & afnza );
};
 
template < class SymbolType, class StateType >
automaton::DPDA < SymbolType, ext::variant < StateType, alphabet::BottomOfTheStackSymbol >, char > ToPrefixPushdownAutomaton::convert ( const automaton::ArcFactoredDeterministicZAutomaton < SymbolType, StateType > & afdza ) {
    char nonFinalPDAState = 'q';
    char finalPDAState = 'r';
    automaton::DPDA < SymbolType, ext::variant < StateType, alphabet::BottomOfTheStackSymbol >, char > automaton ( nonFinalPDAState, alphabet::BottomOfTheStackSymbol ( ) );
    automaton.addState ( finalPDAState );
    automaton.addFinalState ( finalPDAState );
 
    for ( const auto & symbol : afdza.getInputAlphabet ( ) ) {
        automaton.addInputSymbol ( symbol );
    }
    automaton.addInputSymbol ( alphabet::BarSymbol::instance < SymbolType > ( ) );
 
    for ( const StateType & state : afdza.getStates ( ) ) {
        automaton.addPushdownStoreSymbol ( state );
    }
 
    for (const auto & transition : afdza.getTransitions()) {
        const StateType & to = transition.second;
 
        if ( transition.first.template is < SymbolType > ( ) ) {
            const SymbolType & from = transition.first.template get < SymbolType > ( );
 
            ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > pop { };
            ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > push { to };
 
            automaton.addTransition ( nonFinalPDAState, from, pop, nonFinalPDAState, push );
            automaton.addTransition ( finalPDAState, from, pop, nonFinalPDAState, push );
        } else {
            const ext::pair < StateType, StateType > & from = transition.first.template get < ext::pair < StateType, StateType > > ( );
 
            ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > pop { from.second, from.first };
            ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > push { to };
 
            char targetState = afdza.getFinalStates ( ).contains ( from.second ) ? finalPDAState : nonFinalPDAState;
 
            automaton.addTransition ( nonFinalPDAState, alphabet::BarSymbol::instance < SymbolType > ( ), pop, targetState, push );
            automaton.addTransition ( finalPDAState, alphabet::BarSymbol::instance < SymbolType > ( ), pop, targetState, push );
        }
    }
 
    for ( const auto & finalState : afdza.getFinalStates ( ) ) {
        ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > pop = { finalState, alphabet::BottomOfTheStackSymbol ( ) };
        ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > push;
 
        automaton.addTransition ( nonFinalPDAState, alphabet::BarSymbol::instance < SymbolType > ( ), pop, finalPDAState, push );
        automaton.addTransition ( finalPDAState, alphabet::BarSymbol::instance < SymbolType > ( ), pop, finalPDAState, push );
    }
 
    return automaton;
}
 
template < class SymbolType, class StateType >
automaton::NPDA < SymbolType, ext::variant < StateType, alphabet::BottomOfTheStackSymbol >, char > ToPrefixPushdownAutomaton::convert ( const automaton::ArcFactoredNondeterministicZAutomaton < SymbolType, StateType > & afnza ) {
    automaton::NPDA < SymbolType, ext::variant < StateType, alphabet::BottomOfTheStackSymbol >, char > automaton ( 'q', alphabet::BottomOfTheStackSymbol ( ) );
 
    for ( const auto & symbol : afnza.getInputAlphabet ( ) ) {
        automaton.addInputSymbol ( symbol );
    }
    automaton.addInputSymbol ( alphabet::BarSymbol::instance < SymbolType > ( ) );
 
    for ( const StateType & state : afnza.getStates ( ) ) {
        automaton.addPushdownStoreSymbol ( state );
    }
 
    for (const auto & transition : afnza.getTransitions()) {
        const StateType & to = transition.second;
        if ( transition.first.template is < SymbolType > ( ) ) {
            const SymbolType & from = transition.first.template get < SymbolType > ( );
            ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > pop { };
            ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > push { to };
            automaton.addTransition ( automaton.getInitialState ( ), from, pop, automaton.getInitialState ( ), push );
        } else {
            const ext::pair < StateType, StateType > & from = transition.first.template get < ext::pair < StateType, StateType > > ( );
 
            ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > pop { from.second, from.first };
            ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > push { to };
 
            automaton.addTransition ( automaton.getInitialState ( ), alphabet::BarSymbol::instance < SymbolType > ( ), pop, automaton.getInitialState ( ), push );
        }
    }
 
    auto finalPDAState = 'r';
    automaton.addState ( finalPDAState );
    automaton.addFinalState ( finalPDAState );
 
    for ( const auto & finalState : afnza.getFinalStates ( ) ) {
        ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > pop = { finalState, alphabet::BottomOfTheStackSymbol ( ) };
        ext::vector < ext::variant < StateType, alphabet::BottomOfTheStackSymbol > > push;
        automaton.addTransition ( automaton.getInitialState ( ), alphabet::BarSymbol::instance < SymbolType > ( ), pop, finalPDAState, push );
    }
 
    return automaton;
}
 
} /* namespace convert */
 
} /* namespace automaton */