DeterminizeRHDPDAPart.hxx

Go to the documentation of this file.

 
#include "common/RHDPDACommon.h"
 
#include <automaton/PDA/RealTimeHeightDeterministicNPDA.h>
#include <alib/set>
#include <global/GlobalData.h>
 
namespace automaton {
 
namespace determinize {
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
ext::set<common::symbol_or_epsilon < InputSymbolType >> getRetPartitioning(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & npda, const ext::set < StateType > & dSubSet ) {
    ext::set<common::symbol_or_epsilon < InputSymbolType >> ret;
 
    for(const auto& transition : npda.getReturnTransitions())
        if ( dSubSet.contains ( std::get < 0 > ( transition.first ) ) )
            ret.insert(std::get<1>(transition.first));
 
    return ret;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
ext::set<common::symbol_or_epsilon < InputSymbolType >> getCallPartitioning(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & npda, const ext::set < StateType > & dSubSet ) {
    ext::set<common::symbol_or_epsilon < InputSymbolType >> call;
 
    for(const auto& transition : npda.getCallTransitions())
        if ( dSubSet.contains ( transition.first.first ) )
            call.insert(transition.first.second);
 
    return call;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
ext::set<common::symbol_or_epsilon < InputSymbolType >> getLocalPartitioning(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & npda, const ext::set < StateType > & dSubSet ) {
    ext::set<common::symbol_or_epsilon < InputSymbolType >> local;
 
    for(const auto& transition : npda.getLocalTransitions())
        if ( dSubSet.contains ( transition.first.first ) )
            local.insert(transition.first.second);
 
    return local;
}
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, ext::pair < ext::set < ext::pair < StateType, StateType > >, common::symbol_or_epsilon < InputSymbolType > >, ext::set < ext::pair < StateType, StateType > > > Determinize::determinize ( const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & npda ) {
    using DeterministicStateType = ext::set < ext::pair < StateType, StateType > >;
    using DeterministicPushdownStoreSymbolType = ext::pair < DeterministicStateType, common::symbol_or_epsilon < InputSymbolType > >;
 
    DeterministicStateType initialLabel = createIdentity(npda.getInitialStates());
    DeterministicPushdownStoreSymbolType bottom = ext::make_pair ( DeterministicStateType { }, common::symbol_or_epsilon < InputSymbolType > ( alphabet::BottomOfTheStackSymbol::instance < InputSymbolType > ( ) ) );
 
    automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, DeterministicPushdownStoreSymbolType, DeterministicStateType > dpda ( initialLabel, bottom );
    dpda.setInputAlphabet ( npda.getInputAlphabet ( ) );
 
    ext::map < DeterministicStateType, ext::set < DeterministicStateType > > localClosure;
    ext::map < DeterministicStateType, ext::set < DeterministicPushdownStoreSymbolType > > topSymbols;
 
    std::queue < DeterministicStateType > dirtyStates;
    dirtyStates.push ( initialLabel );
 
    std::queue < ext::pair<DeterministicStateType, DeterministicPushdownStoreSymbolType> > dirtyStateSymbols;
    dirtyStateSymbols.push ( ext::make_pair ( initialLabel, bottom ) );
 
    while ( ! dirtyStateSymbols.empty ( ) || ! dirtyStates.empty ( ) ) {
        if ( ! dirtyStateSymbols.empty ( ) ) {
            DeterministicStateType state = std::move ( dirtyStateSymbols.front ( ).first );
            DeterministicPushdownStoreSymbolType pdaSymbol = std::move ( dirtyStateSymbols.front ( ).second );
 
            dirtyStateSymbols.pop ( );
 
            if ( common::GlobalData::verbose )
                common::Streams::log << "Dirty state: " << state << " symbol: " << pdaSymbol << std::endl;
 
            ext::set<common::symbol_or_epsilon < InputSymbolType >> retPart = getRetPartitioning(npda, retrieveDSubSet(state));
 
            for( common::symbol_or_epsilon < InputSymbolType > && input : ext::make_mover ( retPart ) ) {
                DeterministicStateType to;
 
                if ( pdaSymbol == dpda.getBottomOfTheStackSymbol ( ) )
                    to = retInitial ( state, input, npda );
                else
                    to = ret ( state, pdaSymbol, input, npda );
 
                if ( to.empty ( ) )
                    continue;
 
                if ( dpda.addState ( to ) )
                    dirtyStates.push ( to );
 
                localClosure [ pdaSymbol.first ].insert ( to );
 
                updateTopSymbols ( localClosure, topSymbols, dirtyStateSymbols, to, topSymbols [ pdaSymbol.first ] );
 
                dpda.addReturnTransition ( state, std::move ( input ), pdaSymbol, std::move ( to ) );
            }
        } else { // ! dirtyStates.empty ( )
            DeterministicStateType state = std::move ( dirtyStates.front ( ) );
            dirtyStates.pop ( );
 
            if ( common::GlobalData::verbose )
                common::Streams::log << "Dirty state: " << state << std::endl;
 
            ext::set < StateType > dSubSet = retrieveDSubSet(state);
            ext::set<common::symbol_or_epsilon < InputSymbolType >> localPart = getLocalPartitioning(npda, dSubSet);
            ext::set<common::symbol_or_epsilon < InputSymbolType >> callPart = getCallPartitioning(npda, dSubSet);
 
            for ( common::symbol_or_epsilon < InputSymbolType > && input : ext::make_mover ( localPart ) ) {
                DeterministicStateType to = local ( state, input, npda );
 
                if ( to.empty ( ) )
                    continue;
 
                if ( dpda.addState ( to ) )
                    dirtyStates.push ( to );
 
                localClosure [ state ].insert ( to );
 
                updateTopSymbols ( localClosure, topSymbols, dirtyStateSymbols, to, topSymbols [ state ] );
 
                dpda.addLocalTransition ( state, std::move ( input ), std::move ( to ) );
            }
            for ( common::symbol_or_epsilon < InputSymbolType > && input : ext::make_mover ( callPart ) ) {
                DeterministicStateType to = call ( state, input, npda );
 
                if ( to.empty ( ) )
                    continue;
 
                ext::pair < DeterministicStateType, common::symbol_or_epsilon < InputSymbolType > > pdaSymbol = ext::make_pair ( state, input );
 
                if ( dpda.addState ( to ) )
                    dirtyStates.push ( to );
 
                updateTopSymbols ( localClosure, topSymbols, dirtyStateSymbols, to, { pdaSymbol } );
 
                dpda.addPushdownStoreSymbol ( pdaSymbol );
                dpda.addCallTransition ( state, std::move ( input ), std::move ( to ), std::move ( pdaSymbol ) );
            }
        }
    }
 
    const ext::set<StateType>& finalLabels = npda.getFinalStates();
    for(const DeterministicStateType & state : dpda.getStates()) {
        ext::set<StateType> labels = retrieveDSubSet(state);
 
        if(!ext::excludes(finalLabels.begin(), finalLabels.end(), labels.begin(), labels.end()))
            dpda.addFinalState(state);
    }
 
    return dpda;
}
 
} /* namespace determinize */
 
} /* namespace automaton */