RHDPDACommon.h

Go to the documentation of this file.

 
#pragma once
 
#include "common/DefaultStateType.h"
#include "common/DefaultSymbolType.h"
#include <alib/set>
#include <alib/map>
#include "automaton/PDA/VisiblyPushdownDPDA.h"
#include "automaton/PDA/RealTimeHeightDeterministicDPDA.h"
#include <queue>
 
namespace automaton {
 
namespace determinize {
 
template < class StateType >
ext::set<StateType> retrieveDSubSet(const ext::set<ext::pair<StateType, StateType>>& localOperation) {
    ext::set<StateType> id;
    for(const ext::pair < StateType, StateType > & entry : localOperation) {
        id.insert(entry.second);
    }
    return id;
}
 
template < class StateType >
ext::set<ext::pair<StateType, StateType>> createIdentity(const ext::set<StateType>& states) {
    ext::set<ext::pair<StateType, StateType>> id;
    for(const StateType& state : states) {
        id.insert(ext::make_pair(state, state));
    }
    return id;
}
 
template < class InputSymbolType, class StateType, class N >
ext::set < ext::pair < StateType, StateType > > retInitial ( const ext::set < ext::pair < StateType, StateType > > & S, const InputSymbolType & input, const N & nondeterministic ) {
    ext::set<ext::pair<StateType, StateType>> S1;
 
    for ( const auto & entry : S ) {
        const StateType & q = entry.first;
        const StateType & q2 = entry.second;
 
        for ( const auto & transition : nondeterministic.getReturnTransitions ( ).equal_range ( ext::make_tuple ( q2, input, nondeterministic.getBottomOfTheStackSymbol ( ) ) ) ) {
            const StateType & q1 = transition.second;
 
            S1.insert ( ext::make_pair ( q, q1 ) );
        }
    }
 
    return S1;
}
 
template < class InputSymbolType, class DeterministicPushdownStoreSymbolType, class StateType, class N >
ext::set < ext::pair < StateType, StateType > > ret ( const ext::set < ext::pair < StateType, StateType > > & S, const DeterministicPushdownStoreSymbolType & pdaSymbol, const InputSymbolType & input, const N & nondeterministic ) {
    ext::set<ext::pair<StateType, StateType>> update;
 
    for(const auto& transition : nondeterministic.getCallTransitions()) {
        if(pdaSymbol.second != std::get<1>(transition.first)) continue;
 
        const StateType & q = std::get<0>(transition.first);
        const StateType & q1 = transition.second.first;
        const auto & gamma = transition.second.second;
 
        for(const auto& entry : S.equal_range ( ext::slice_comp ( q1 ) ) ) {
            const StateType& q2 = entry.second;
 
            for ( const auto & returnTransition : nondeterministic.getReturnTransitions ( ).equal_range ( ext::make_tuple ( q2, input, gamma ) ) ) {
                const StateType & qI = returnTransition.second;
                update.insert(ext::make_pair(q, qI));
            }
        }
    }
 
    const ext::set<ext::pair<StateType, StateType>>& S1 = pdaSymbol.first;
 
    ext::set<ext::pair<StateType, StateType>> S2;
    for(const auto& entry : S1) {
        const StateType& q = entry.first;
        const StateType& q3 = entry.second;
        for(const auto& entry2 : update.equal_range ( ext::slice_comp ( q3 ) ) ) {
            const StateType& qI = entry2.second;
 
            S2.insert(ext::make_pair(q, qI));
        }
    }
 
    return S2;
}
 
template < class InputSymbolType, class StateType, class N >
ext::set < ext::pair < StateType, StateType > > call ( const ext::set < ext::pair < StateType, StateType > > & S, const InputSymbolType & input, const N & nondeterministic ) {
    ext::set < StateType > R1;
 
    for(const StateType& q : retrieveDSubSet ( S ) ) {
        for ( const auto & to : nondeterministic.getCallTransitions ( ).equal_range ( ext::make_pair ( q, input ) ) ) {
            const StateType& q1 = to.second.first;
 
            R1.insert(q1);
        }
    }
 
    return createIdentity ( std::move ( R1 ) );
}
 
template < class InputSymbolType, class StateType, class N >
ext::set < ext::pair < StateType, StateType > > local ( const ext::set < ext::pair < StateType, StateType > > & S, const InputSymbolType & input, const N & nondeterministic ) {
    ext::set<ext::pair<StateType, StateType>> S1;
 
    for ( const auto & entry : S ) {
        const StateType & q = entry.first;
        const StateType & q2 = entry.second;
 
        for ( const auto & transition : nondeterministic.getLocalTransitions ( ).equal_range ( ext::make_pair ( q2, input ) ) ) {
            const StateType & q1 = transition.second;
            S1.insert(ext::make_pair(q, q1));
        }
    }
 
    return S1;
}
 
template < class DeterministicStateType, class DeterministicPushdownStoreSymbolType >
void updateTopSymbols ( ext::map < DeterministicStateType, ext::set < DeterministicStateType > > & localClosure, ext::map < DeterministicStateType, ext::set < DeterministicPushdownStoreSymbolType > > & topSymbols, std::queue < ext::pair<DeterministicStateType, DeterministicPushdownStoreSymbolType> > & dirtyStateSymbols, const DeterministicStateType & state, const ext::set < DeterministicPushdownStoreSymbolType > & newSymbols ) {
    ext::set < DeterministicPushdownStoreSymbolType > missingSymbols;
    std::set_difference ( newSymbols.begin ( ), newSymbols.end ( ), topSymbols [ state ].begin ( ), topSymbols [ state ].end ( ), std::inserter ( missingSymbols, missingSymbols.end ( ) ) );
 
    if ( missingSymbols.empty ( ) )
        return;
 
    topSymbols [ state ].insert ( missingSymbols.begin ( ), missingSymbols.end ( ) );
 
    for ( const DeterministicStateType & adv : localClosure [ state ] )
        updateTopSymbols ( localClosure, topSymbols, dirtyStateSymbols, adv, missingSymbols );
 
    for ( DeterministicPushdownStoreSymbolType && symbol : ext::make_mover ( missingSymbols ) )
        dirtyStateSymbols.push ( ext::make_pair ( state, std::move ( symbol ) ) );
}
 
} /* namespace determinize */
 
} /* namespace automaton */