diff --git a/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.hxx b/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.hxx
index 1ce76429cc78e6defee2257f2c8cf70261509032..af0da7566604d0ebf2103c2a9d9cc90f6cf771f2 100644
--- a/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.hxx
+++ b/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.hxx
@@ -68,29 +68,28 @@ automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, ext::pair < ext::s
automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, DeterministicPushdownStoreSymbolType, DeterministicStateType > dpda ( initialLabel, bottom );
dpda.setInputAlphabet ( npda.getInputAlphabet ( ) );
- ext::set < ext::pair < DeterministicStateType, DeterministicPushdownStoreSymbolType > > rubbishReturnTransitions;
+ ext::map < DeterministicStateType, ext::set < DeterministicStateType > > localClosure;
+ ext::map < DeterministicStateType, ext::set < DeterministicPushdownStoreSymbolType > > topSymbols;
- for(;;) {
- ext::set<ext::pair<DeterministicStateType, DeterministicPushdownStoreSymbolType>> stateSymbols = existsDirtyStateSymbol(dpda, npda);
+ std::queue < DeterministicStateType > dirtyStates;
+ dirtyStates.push ( initialLabel );
- for ( const ext::pair < DeterministicStateType, DeterministicPushdownStoreSymbolType > & rubbishStateSymbols : rubbishReturnTransitions ) {
- stateSymbols.erase ( rubbishStateSymbols );
- }
+ std::queue < ext::pair<DeterministicStateType, DeterministicPushdownStoreSymbolType> > dirtyStateSymbols;
+ dirtyStateSymbols.push ( ext::make_pair ( initialLabel, bottom ) );
- ext::set<DeterministicStateType> states = existsDirtyState(dpda, npda);
+ while ( ! dirtyStateSymbols.empty ( ) || ! dirtyStates.empty ( ) ) {
+ if ( ! dirtyStateSymbols.empty ( ) ) {
+ DeterministicStateType state = std::move ( dirtyStateSymbols.front ( ).first );
+ DeterministicPushdownStoreSymbolType pdaSymbol = std::move ( dirtyStateSymbols.front ( ).second );
- if(stateSymbols.empty() && states.empty()) break;
+ dirtyStateSymbols.pop ( );
- for ( const ext::pair<DeterministicStateType, DeterministicPushdownStoreSymbolType> & stateSymbol : stateSymbols ) {
if ( common::GlobalData::verbose )
- common::Streams::log << "Dirty state symbol: " << stateSymbol << std::endl;
-
- ext::set<common::symbol_or_epsilon < InputSymbolType >> retPart = getRetPartitioning(npda, stateSymbol.first);
+ common::Streams::log << "Dirty state: " << state << " symbol: " << pdaSymbol << std::endl;
- const DeterministicStateType & state = stateSymbol.first;
- const DeterministicPushdownStoreSymbolType & pdaSymbol = stateSymbol.second;
+ ext::set<common::symbol_or_epsilon < InputSymbolType >> retPart = getRetPartitioning(npda, state);
- for(const common::symbol_or_epsilon < InputSymbolType > & input : retPart ) {
+ for( common::symbol_or_epsilon < InputSymbolType > && input : ext::make_mover ( retPart ) ) {
DeterministicStateType to;
if ( pdaSymbol == dpda.getBottomOfTheStackSymbol ( ) )
@@ -98,37 +97,58 @@ automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, ext::pair < ext::s
else
to = ret ( state, pdaSymbol, input, npda );
- if ( ! to.empty ( ) ) {
- dpda.addState ( to );
- dpda.addReturnTransition ( state, input, pdaSymbol, std::move ( to ) );
- } else
- rubbishReturnTransitions.insert ( ext::make_pair ( state, pdaSymbol ) );
+ 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 ( );
- for(const auto& state : states) {
if ( common::GlobalData::verbose )
common::Streams::log << "Dirty state: " << state << std::endl;
ext::set<common::symbol_or_epsilon < InputSymbolType >> localPart = getLocalPartitioning(npda, state);
ext::set<common::symbol_or_epsilon < InputSymbolType >> callPart = getCallPartitioning(npda, state);
- for ( const common::symbol_or_epsilon < InputSymbolType > & input : localPart ) {
+ for ( common::symbol_or_epsilon < InputSymbolType > && input : ext::make_mover ( localPart ) ) {
DeterministicStateType to = local ( state, input, npda );
- if ( ! to.empty ( ) ) {
- dpda.addState ( to );
- dpda.addLocalTransition ( state, input, std::move ( to ) );
- }
+
+ 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 ( const common::symbol_or_epsilon < InputSymbolType > & input : callPart ) {
+ for ( common::symbol_or_epsilon < InputSymbolType > && input : ext::make_mover ( callPart ) ) {
DeterministicStateType to = call ( state, input, npda );
- if ( ! to.empty ( ) ) {
- ext::pair < DeterministicStateType, common::symbol_or_epsilon < InputSymbolType > > pdaSymbol = ext::make_pair ( state, input );
- dpda.addState ( to );
- dpda.addPushdownStoreSymbol ( pdaSymbol );
- dpda.addCallTransition ( state, input, std::move ( to ), std::move ( pdaSymbol ) );
- }
+ 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 ) );
}
}
}
@@ -137,13 +157,8 @@ automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, ext::pair < ext::s
for(const DeterministicStateType & state : dpda.getStates()) {
const ext::set<StateType> labels = retrieveDSubSet(state);
- if(!ext::excludes(finalLabels.begin(), finalLabels.end(), labels.begin(), labels.end())) {
+ if(!ext::excludes(finalLabels.begin(), finalLabels.end(), labels.begin(), labels.end()))
dpda.addFinalState(state);
- }
- }
-
- if ( common::GlobalData::verbose ) {
- common::Streams::log << "Rubbish return transitions: " << rubbishReturnTransitions << std::endl;
}
return dpda;
diff --git a/alib2algo/src/automaton/determinize/DeterminizeVPAPart.hxx b/alib2algo/src/automaton/determinize/DeterminizeVPAPart.hxx
index 568fc725a25eae0c900928c278454589a48be5dd..cfad2055cdca6f34a8e233a1d7106ecb35925128 100644
--- a/alib2algo/src/automaton/determinize/DeterminizeVPAPart.hxx
+++ b/alib2algo/src/automaton/determinize/DeterminizeVPAPart.hxx
@@ -29,43 +29,72 @@ automaton::VisiblyPushdownDPDA < InputSymbolType, ext::pair < ext::set < ext::pa
dpda.setLocalInputAlphabet(npda.getLocalInputAlphabet());
dpda.setReturnInputAlphabet(npda.getReturnInputAlphabet());
- for(;;) {
- ext::set<ext::pair<DeterministicStateType, DeterministicPushdownStoreSymbolType>> stateSymbols = existsDirtyStateSymbol(dpda, npda);
- ext::set<DeterministicStateType> states = existsDirtyState(dpda, npda);
+ ext::map < DeterministicStateType, ext::set < DeterministicStateType > > localClosure;
+ ext::map < DeterministicStateType, ext::set < DeterministicPushdownStoreSymbolType > > topSymbols;
- if(stateSymbols.empty() && states.empty()) break;
+ std::queue < DeterministicStateType > dirtyStates;
+ dirtyStates.push ( initialLabel );
- for ( const ext::pair < DeterministicStateType, DeterministicPushdownStoreSymbolType > & stateSymbol : stateSymbols ) {
- const DeterministicStateType & state = stateSymbol.first;
- const DeterministicPushdownStoreSymbolType & pdaSymbol = stateSymbol.second;
+ 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 ( ) ) {
- if ( pdaSymbol == dpda.getBottomOfTheStackSymbol ( ) ) {
- DeterministicStateType to = retInitial ( state, input, npda );
+ 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 );
- dpda.addState ( to );
- dpda.addReturnTransition ( state, input, pdaSymbol, std::move ( to ) );
- } else {
- DeterministicStateType to = ret ( state, pdaSymbol, input, npda );
+ localClosure [ pdaSymbol.first ].insert ( to );
- dpda.addState ( to );
- dpda.addReturnTransition ( state, input, pdaSymbol, std::move ( 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 DeterministicStateType & state : states ) {
for ( const InputSymbolType & input : npda.getLocalInputAlphabet ( ) ) {
DeterministicStateType to = local ( state, input, npda );
- dpda.addState ( to );
+ 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 );
- dpda.addState ( to );
+ 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 ) );
}
@@ -76,9 +105,8 @@ automaton::VisiblyPushdownDPDA < InputSymbolType, ext::pair < ext::set < ext::pa
for(const DeterministicStateType & state : dpda.getStates()) {
const ext::set<StateType> labels = retrieveDSubSet(state);
- if(!ext::excludes(finalLabels.begin(), finalLabels.end(), labels.begin(), labels.end())) {
+ if(!ext::excludes(finalLabels.begin(), finalLabels.end(), labels.begin(), labels.end()))
dpda.addFinalState(state);
- }
}
return dpda;
diff --git a/alib2algo/src/automaton/determinize/common/RHDPDACommon.h b/alib2algo/src/automaton/determinize/common/RHDPDACommon.h
index 7f2aedf58d2f19bb975a8fbedf15d06b15650580..366cdde28e7f2c09a70cd9ab4341137ed2a6495f 100644
--- a/alib2algo/src/automaton/determinize/common/RHDPDACommon.h
+++ b/alib2algo/src/automaton/determinize/common/RHDPDACommon.h
@@ -7,6 +7,7 @@
#include <alib/map>
#include "automaton/PDA/VisiblyPushdownDPDA.h"
#include "automaton/PDA/RealTimeHeightDeterministicDPDA.h"
+#include <queue>
namespace automaton {
@@ -129,129 +130,23 @@ ext::set < ext::pair < StateType, StateType > > local ( const ext::set < ext::pa
return S1;
}
-template<class T, class R>
-ext::set < typename T::StateType_t > existsDirtyState(const T& d, const R& n) {
- ext::set < typename T::StateType_t > dirtyStates;
+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 ( ) ) );
- for(const typename T::StateType_t & state : d.getStates ( ) ) {
- auto dSubSet = retrieveDSubSet(state);
+ if ( missingSymbols.empty ( ) )
+ return;
- bool originalCallsLocals = false;
- for(const auto& transition : n.getCallTransitions()) {
- if(dSubSet.count(transition.first.first)) {
- originalCallsLocals = true;
- break;
- }
- }
- if(!originalCallsLocals) for(const auto& transition : n.getLocalTransitions()) {
- if(dSubSet.count(transition.first.first)) {
- originalCallsLocals = true;
- break;
- }
- }
+ topSymbols [ state ].insert ( missingSymbols.begin ( ), missingSymbols.end ( ) );
- if(!originalCallsLocals) continue;
- bool deterministicCallLocals = false;
+ for ( const DeterministicStateType & adv : localClosure [ state ] )
+ updateTopSymbols ( localClosure, topSymbols, dirtyStateSymbols, adv, missingSymbols );
- for(const auto& transition : d.getCallTransitions ( ) ) {
- if(state == transition.first.first) {
- deterministicCallLocals = true;
- break;
- }
- }
- if(deterministicCallLocals) for(const auto& transition : d.getLocalTransitions ( ) ) {
- if(state == transition.first.first) {
- deterministicCallLocals = true;
- break;
- }
- }
-
- if(originalCallsLocals && !deterministicCallLocals) dirtyStates.insert(state);
-
- }
- return dirtyStates;
+ for ( DeterministicPushdownStoreSymbolType && symbol : ext::make_mover ( missingSymbols ) )
+ dirtyStateSymbols.push ( ext::make_pair ( state, std::move ( symbol ) ) );
}
-template < class T, class DeterministicStateType >
-ext::set < DeterministicStateType > localClosure ( const DeterministicStateType & initState, const T & d ) {
- ext::set < DeterministicStateType > closed { initState };
- ext::deque < DeterministicStateType > queue { initState };
-
- while ( ! queue.empty ( ) ) {
- DeterministicStateType state = std::move ( queue.back ( ) );
- queue.pop_back ( );
-
- for ( const auto & transition : d.getLocalTransitions ( ) ) {
- if ( transition.second != state )
- continue;
-
- if ( closed.insert ( transition.first.first ).second )
- queue.push_back ( transition.first.first );
- }
-
- for ( const auto & transition : d.getReturnTransitions ( ) ) {
- if ( transition.second != state )
- continue;
-
- const auto & popSymbol = std::get < 2 > ( transition.first );
- if ( popSymbol == d.getBottomOfTheStackSymbol ( ) )
- continue;
-
- const DeterministicStateType & statePart = popSymbol.first;
- if ( closed.insert ( statePart ).second )
- queue.push_back ( statePart );
- }
- }
-
- return closed;
-}
-
-template < class T, class R >
-ext::set < ext::pair < typename T::StateType_t, typename T::PushdownStoreSymbolType_t > > existsDirtyStateSymbol ( const T & d, const R & n ) {
- ext::set < ext::pair < typename T::StateType_t, typename T::PushdownStoreSymbolType_t > > dirtyStateSymbols;
-
- for ( const typename T::StateType_t & state : d.getStates ( ) ) {
- bool originalPops = false;
- auto dSubSet = retrieveDSubSet ( state );
-
- for ( const auto & transition : n.getReturnTransitions ( ) ) {
- if ( dSubSet.count ( std::get < 0 > ( transition.first ) ) ) {
- originalPops = true;
- break;
- }
- }
- if ( ! originalPops )
- continue;
-
- ext::set < typename T::PushdownStoreSymbolType_t > topSymbols;
- for ( const typename T::StateType_t & localState : localClosure ( state, d ) ) {
- for ( const auto & transition : d.getCallTransitions ( ) ) {
- const auto & to = transition.second;
- if ( localState != to.first )
- continue;
-
- topSymbols.insert ( to.second );
- }
-
- if ( d.getInitialState ( ) == localState )
- topSymbols.insert ( d.getBottomOfTheStackSymbol ( ) );
- }
-
- for ( const auto & transition : d.getReturnTransitions ( ) ) {
- if ( state != std::get < 0 > ( transition.first ) )
- continue;
-
- topSymbols.erase(std::get<2>(transition.first));
- }
-
- for ( const typename T::PushdownStoreSymbolType_t & topSymbol : topSymbols )
- dirtyStateSymbols.insert ( ext::make_pair ( state, topSymbol ) );
- }
-
- return dirtyStateSymbols;
-}
-
-
} /* namespace determinize */
} /* namespace automaton */
diff --git a/alib2algo/test-src/automaton/determinize/determinizeTest.cpp b/alib2algo/test-src/automaton/determinize/determinizeTest.cpp
index d9e1c8b263b48a5b95efc2c43581b591270e320f..9561b405fde90a5893ed0e882469202fd3893bd7 100644
--- a/alib2algo/test-src/automaton/determinize/determinizeTest.cpp
+++ b/alib2algo/test-src/automaton/determinize/determinizeTest.cpp
@@ -98,10 +98,10 @@ TEST_CASE ( "Determinize", "[unit][algo][automaton][determinize]" ) {
automaton.addFinalState(DefaultStateType(4));
auto determinized = automaton::determinize::Determinize::determinize ( automaton );
- CHECK ( determinized.getStates().size() == 29 );
+ CHECK ( determinized.getStates().size() == 28 );
CHECK ( determinized.getFinalStates().size() == 14 );
CHECK ( determinized.getCallTransitions().size() == 28 );
- CHECK ( determinized.getReturnTransitions().size() == 198 );
+ CHECK ( determinized.getReturnTransitions().size() == 196 );
CHECK ( determinized.getLocalTransitions().size() == 0 );
CHECK ( determinized.getCallTransitions().size() == 28 );