diff --git a/alib2algo/src/automaton/determinize/DeterminizeNFTAPart.hxx b/alib2algo/src/automaton/determinize/DeterminizeNFTAPart.hxx index 8a13e4c854e0c7cdb646f3db9025e938540221ef..ca666b5829a819c4ca83366b5226eb9c5c4e1280 100644 --- a/alib2algo/src/automaton/determinize/DeterminizeNFTAPart.hxx +++ b/alib2algo/src/automaton/determinize/DeterminizeNFTAPart.hxx @@ -14,23 +14,18 @@ namespace automaton { namespace determinize { template < class SymbolType, class RankType, class StateType > -ext::set < StateType > getTransitionRightSide ( const NFTA < SymbolType, RankType, StateType > & nfta, const common::ranked_symbol < SymbolType, RankType > & symbol, const ext::vector< ext::set < StateType > > & states ) { - ext::set < StateType > res; - - for ( const auto & transition : nfta.getTransitions ( ) ) { - if ( transition.first.first != symbol ) - continue; - - unsigned i = ( unsigned ) symbol.getRank ( ); - for ( ; i > 0; --i ) - if ( ! states [ i - 1 ].count ( transition.first.second [ i - 1 ] ) ) - break; - - if ( i == 0 ) - res.insert ( transition.second.begin ( ), transition.second.end ( ) ); +void constructTransitions ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType, RankType > , ext::vector < StateType > >, ext::set < StateType > > & transition, unsigned i, const ext::multimap < StateType, ext::set < StateType > > & nftaStateToDftaStates, ext::vector < ext::set < StateType > > & transitionLHS, ext::map < ext::pair < common::ranked_symbol < SymbolType, RankType >, ext::vector < ext::set < StateType > > >, ext::set < StateType > > & resultTransition ) { + if ( i == transition.first.second.size ( ) ) { + resultTransition [ ext::make_pair ( transition.first.first, transitionLHS ) ].insert ( transition.second.begin ( ), transition.second.end ( ) ); + } else { + const StateType & nftaState = transition.first.second [ i ]; + + for ( const std::pair < StateType, ext::set < StateType > > & dftaState : nftaStateToDftaStates.equal_range ( nftaState ) ) { + transitionLHS.push_back ( dftaState.second ); + constructTransitions ( transition, i + 1, nftaStateToDftaStates, transitionLHS, resultTransition ); + transitionLHS.pop_back ( ); + } } - - return res; } template < class SymbolType, class RankType, class StateType > @@ -38,78 +33,56 @@ automaton::DFTA < SymbolType, RankType, ext::set < StateType > > Determinize::de automaton::DFTA < SymbolType, RankType, ext::set < StateType > > res; res.setInputAlphabet ( nfta.getInputAlphabet ( ) ); - for ( const auto & state : nfta.getStates ( ) ) - res.addState ( { state } ); - for ( const auto & state : nfta.getFinalStates ( ) ) - res.addFinalState ( { state } ); + ext::multimap < StateType, ext::set < StateType > > nftaStateToDftaStates; // each dfta state must be inserted only once to each nfta d-subset state - ext::deque < ext::set < StateType > > todo; + for ( const auto & symbol : nfta.getInputAlphabet ( ) ) { + if ( symbol.getRank ( ) != 0 ) + continue; - for ( const auto & transition : nfta.getTransitions ( ) ) { - ext::set < StateType > state = transition.second; - ext::vector < ext::set < StateType > > states; + ext::set < StateType > dftaState; + ext::vector < StateType > source { }; + for ( const auto & transition : nfta.getTransitions ( ).equal_range ( ext::tie ( symbol, source ) ) ) + dftaState.insert ( transition.second.begin ( ), transition.second.end ( ) ); - for ( const auto & s : transition.first.second ) - states.push_back ( { s } ); + for ( const auto & state : dftaState ) + nftaStateToDftaStates.insert ( state, dftaState ); - if ( transition.second.size ( ) > 1 && res.addState ( state ) ) - todo.push_back ( state ); + res.addState ( dftaState ); - res.addTransition ( transition.first.first, states, state ); + res.addTransition ( symbol, ext::vector < ext::set < StateType > > { }, dftaState ); } - while ( ! todo.empty ( ) ) { - ext::set < StateType > currentState = todo.front(); - todo.pop_front(); + bool added = true; + while ( added ) { + added = false; - ext::deque < std::pair < std::pair < common::ranked_symbol < SymbolType, RankType >, ext::vector < ext::set < StateType > > >, ext::set < StateType > > > transitions; - ext::deque < unsigned > stops; + ext::map < ext::pair < common::ranked_symbol < SymbolType, RankType >, ext::vector < ext::set < StateType > > >, ext::set < StateType > > transitions; - for ( const auto & transition : res.getTransitions ( ) ) { - transitions.push_back ( transition ); - stops.push_back ( 0 ); + for ( const auto & transition : nfta.getTransitions ( ) ) { + ext::vector < ext::set < StateType > > transitionLHS; + constructTransitions ( transition, 0, nftaStateToDftaStates, transitionLHS, transitions ); } - while ( ! transitions.empty ( ) ) { - auto transition = transitions.front ( ); - transitions.pop_front ( ); + for ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType, RankType >, ext::vector < ext::set < StateType > > >, ext::set < StateType > > transition : transitions ) { + if ( res.addState ( transition.second ) ) { + added = true; - unsigned stop = stops.front ( ); - stops.pop_front ( ); - - const ext::vector < ext::set < StateType > > & states = transition.first.second; - - for ( unsigned i = stop; i < states.size ( ); ++i ) { - if ( states [ i ].size ( ) != 1 ) - continue; - - StateType nftaState = * states [ i ].begin ( ); - if ( currentState.count ( nftaState ) ) { - ext::vector < ext::set < StateType > > newStates = states; - newStates [ i ] = currentState; - - ext::set < StateType > newNextState = getTransitionRightSide ( nfta, transition.first.first, newStates ); - if ( ! newNextState.empty ( ) ) { - if ( res.addState ( newNextState ) ) - todo.push_back ( newNextState ); - - if ( res.addTransition ( transition.first.first, newStates, newNextState ) && i + 1 != states.size ( ) ) { - transitions.push_back ( ext::make_pair ( ext::make_pair ( transition.first.first, newStates ), newNextState ) ); - stops.push_back(i + 1); - } - } - } + for ( const auto & state : transition.second ) + nftaStateToDftaStates.insert ( state, transition.second ); } + res.addTransition ( transition.first.first, transition.first.second, transition.second ); } - for ( const auto & state : currentState ) { + } + + for ( const auto & dftaState : res.getStates ( ) ) { + for ( const auto & state : dftaState ) { if ( nfta.getFinalStates ( ).count ( state ) ) { - res.addFinalState ( currentState ); + res.addFinalState ( dftaState ); break; } } - } return res;