DeterminizeVPAPart.hxx

Go to the documentation of this file.

 
#include "common/RHDPDACommon.h"
 
#include <alphabet/BottomOfTheStackSymbol.h>
#include <automaton/PDA/VisiblyPushdownNPDA.h>
#include <alib/set>
 
namespace automaton {
 
namespace determinize {
 
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
automaton::VisiblyPushdownDPDA < InputSymbolType, ext::pair < ext::set < ext::pair < StateType, StateType > >, InputSymbolType >, ext::set < ext::pair < StateType, StateType > > > Determinize::determinize ( const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & npda ) {
    using DeterministicStateType = ext::set < ext::pair < StateType, StateType > >;
    using DeterministicPushdownStoreSymbolType = ext::pair < DeterministicStateType, InputSymbolType >;
 
    DeterministicStateType initialLabel = createIdentity(npda.getInitialStates());
    DeterministicPushdownStoreSymbolType bottom = ext::make_pair ( DeterministicStateType { }, alphabet::BottomOfTheStackSymbol::instance < InputSymbolType > ( ) );
 
    automaton::VisiblyPushdownDPDA < InputSymbolType, DeterministicPushdownStoreSymbolType, DeterministicStateType > dpda(initialLabel, bottom);
 
    dpda.setCallInputAlphabet(npda.getCallInputAlphabet());
    dpda.setLocalInputAlphabet(npda.getLocalInputAlphabet());
    dpda.setReturnInputAlphabet(npda.getReturnInputAlphabet());
 
    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 ( );
 
            for ( const InputSymbolType & input : npda.getReturnInputAlphabet ( ) ) {
                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, input, pdaSymbol, std::move ( to ) );
            }
        } else { // ! dirtyStates.empty ( )
            DeterministicStateType state = std::move ( dirtyStates.front ( ) );
            dirtyStates.pop ( );
 
            for ( const InputSymbolType & input : npda.getLocalInputAlphabet ( ) ) {
                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, input, std::move ( to ) );
            }
            for ( const InputSymbolType & input : npda.getCallInputAlphabet ( ) ) {
                DeterministicStateType to = call ( state, input, npda );
                ext::pair < DeterministicStateType, InputSymbolType > pdaSymbol = ext::make_pair ( state, input );
 
                if ( to.empty ( ) )
                    continue;
 
                if ( dpda.addState ( to ) )
                    dirtyStates.push ( to );
 
                updateTopSymbols ( localClosure, topSymbols, dirtyStateSymbols, to, { pdaSymbol } );
 
                dpda.addPushdownStoreSymbol ( pdaSymbol );
                dpda.addCallTransition ( state, 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 */