diff --git a/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.hxx b/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.hxx
index 455e241d7a55f32daf414c63bc29fcd9d932df49..3be9c33574795471bea10070886198361b308477 100644
--- a/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.hxx
+++ b/alib2algo/src/automaton/determinize/DeterminizeRHDPDAPart.hxx
@@ -15,157 +15,37 @@ namespace automaton {
namespace determinize {
-template < class InputSymbolType, class EpsilonType, class StateType >
-void addRetTransition(const ext::set < ext::pair < StateType, StateType > > & from, const ext::variant < EpsilonType, InputSymbolType > & input, const ext::pair < ext::set < ext::pair < StateType, StateType > >, ext::variant < EpsilonType, InputSymbolType > > & dvpdaSymbol, const ext::set < ext::pair < StateType, StateType > > & to, automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, EpsilonType, ext::pair < ext::set < ext::pair < StateType, StateType > >, ext::variant < EpsilonType, InputSymbolType > >, ext::set < ext::pair < StateType, StateType > > > & deterministic) {
- deterministic.addState(from);
- deterministic.addState(to);
- deterministic.addPushdownStoreSymbol(dvpdaSymbol);
-
- deterministic.addReturnTransition(from, input, dvpdaSymbol, to);
-}
-
-template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
-ext::set < ext::pair < StateType, StateType > > retInitial(const ext::set < ext::pair < StateType, StateType > > & state, const ext::variant < EpsilonType, InputSymbolType>& input, const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & nondeterministic ) {
- const ext::set<ext::pair<StateType, StateType>> & S = state;
-
- 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()) {
- if(q2 != std::get<0>(transition.first)) continue;
- if(input != std::get<1>(transition.first)) continue;
- if(nondeterministic.getBottomOfTheStackSymbol() != std::get<2>(transition.first)) continue;
-
- for(const auto& to : transition.second) {
- const StateType& q1 = to;
- S1.insert(ext::make_pair(q, q1));
- }
- }
- }
-
- return S1;
-}
-
template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
-ext::set < ext::pair < StateType, StateType > > ret(const ext::set < ext::pair < StateType, StateType > > & state, const ext::pair < ext::set < ext::pair < StateType, StateType > >, ext::variant < EpsilonType, InputSymbolType > > & pdaSymbol, const ext::variant < EpsilonType, InputSymbolType > & input, const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & nondeterministic ) {
- const ext::set<ext::pair<StateType, StateType>> & S = state;
- const ext::set<ext::pair<StateType, StateType>>& S1 = pdaSymbol.first;
-
- 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);
- for(const auto& to : transition.second) {
- const StateType& q1 = to.first;
- const PushdownStoreSymbolType& gamma = to.second;
-
- for(const auto& entry : S) {
- if(q1 != entry.first) continue;
- const StateType& q2 = entry.second;
-
- for(const auto& transition2 : nondeterministic.getReturnTransitions()) {
- if(q2 != std::get<0>(transition2.first)) continue;
- if(input != std::get<1>(transition2.first)) continue;
- if(gamma != std::get<2>(transition2.first)) continue;
-
- for(const auto& to2 : transition2.second) {
- const StateType& qI = to2;
-
- update.insert(ext::make_pair(q, qI));
- }
- }
- }
- }
- }
-
- 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) {
- if(q3 != entry2.first) continue;
-
- const StateType& qI = entry2.second;
-
- S2.insert(ext::make_pair(q, qI));
- }
- }
-
- return S2;
-}
-
-template < class InputSymbolType, class EpsilonType, class StateType >
-void addCallTransition(const ext::set < ext::pair < StateType, StateType > > & from, const ext::variant<EpsilonType, InputSymbolType > & input, const ext::set < ext::pair < StateType, StateType > > & to, const ext::pair < ext::set < ext::pair < StateType, StateType > >, ext::variant < EpsilonType, InputSymbolType > > & dvpdaSymbol, automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, EpsilonType, ext::pair < ext::set < ext::pair < StateType, StateType > >, ext::variant < EpsilonType, InputSymbolType > >, ext::set < ext::pair < StateType, StateType > > > & deterministic) {
- deterministic.addState(from);
- deterministic.addState(to);
- deterministic.addPushdownStoreSymbol(dvpdaSymbol);
-
- deterministic.addCallTransition(from, input, to, dvpdaSymbol);
-}
-
-template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
-ext::set < ext::pair < StateType, StateType > > call(const ext::set < ext::pair < StateType, StateType > > & state, const ext::variant < EpsilonType, InputSymbolType > & input, const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & nondeterministic ) {
- const ext::set < ext::pair < StateType, StateType > > & S = state;
-
- ext::set < StateType > R = retrieveDSubSet(S);
- ext::set < StateType > R1;
-
- for(const StateType& q : R) {
- for ( const auto & transition : nondeterministic.getCallTransitions()) {
- if(q != transition.first.first) continue;
- if(input != transition.first.second) continue;
+ext::set<ext::variant<EpsilonType, InputSymbolType>> getRetPartitioning(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & n, const ext::set < ext::pair < StateType, StateType > > & state) {
+ ext::set<ext::variant<EpsilonType, InputSymbolType>> ret;
- for(const auto& to : transition.second) {
- const StateType& q1 = to.first;
+ const ext::set<StateType> dSubSet = retrieveDSubSet(state);
- R1.insert(q1);
- }
- }
+ for(const auto& transition : n.getReturnTransitions()) {
+ if(dSubSet.count(std::get<0>(transition.first)))
+ ret.insert(std::get<1>(transition.first));
}
- return createIdentity ( std::move ( R1 ) );
-}
-
-template < class InputSymbolType, class EpsilonType, class StateType >
-void addLocalTransition ( const ext::set < ext::pair < StateType, StateType > > & from, const ext::variant < EpsilonType, InputSymbolType > & input, const ext::set < ext::pair < StateType, StateType > > & to, automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, EpsilonType, ext::pair < ext::set < ext::pair < StateType, StateType > >, ext::variant < EpsilonType, InputSymbolType > >, ext::set < ext::pair < StateType, StateType > > > & deterministic) {
- deterministic.addState(from);
- deterministic.addState(to);
-
- deterministic.addLocalTransition(from, input, to);
+ return ret;
}
template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
-ext::set < ext::pair < StateType, StateType > > local(const ext::set < ext::pair < StateType, StateType > > & state, const ext::variant < EpsilonType, InputSymbolType > & input, const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & nondeterministic ) {
- const ext::set<ext::pair<StateType, StateType>> & S = state;
- 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()) {
- if(q2 != transition.first.first) continue;
- if(input != transition.first.second) continue;
+ext::set<ext::variant<EpsilonType, InputSymbolType>> getCallPartitioning(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & n, const ext::set < ext::pair < StateType, StateType > > & state) {
+ ext::set<ext::variant<EpsilonType, InputSymbolType>> call;
- for(const auto& to : transition.second) {
- const StateType & q1 = to;
+ const ext::set<StateType> dSubSet = retrieveDSubSet(state);
- S1.insert(ext::make_pair(q, q1));
- }
- }
+ for(const auto& transition : n.getCallTransitions()) {
+ if(dSubSet.count(transition.first.first))
+ call.insert(transition.first.second);
}
- return S1;
+ return call;
}
template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
-ext::tuple<ext::set<ext::variant<EpsilonType, InputSymbolType>>, ext::set<ext::variant<EpsilonType, InputSymbolType>>, ext::set<ext::variant<EpsilonType, InputSymbolType>>> getLocalCallRetPartitioning(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & n, const ext::set < ext::pair < StateType, StateType > > & state) {
+ext::set<ext::variant<EpsilonType, InputSymbolType>> getLocalPartitioning(const automaton::RealTimeHeightDeterministicNPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & n, const ext::set < ext::pair < StateType, StateType > > & state) {
ext::set<ext::variant<EpsilonType, InputSymbolType>> local;
- ext::set<ext::variant<EpsilonType, InputSymbolType>> call;
- ext::set<ext::variant<EpsilonType, InputSymbolType>> ret;
const ext::set<StateType> dSubSet = retrieveDSubSet(state);
@@ -174,17 +54,7 @@ ext::tuple<ext::set<ext::variant<EpsilonType, InputSymbolType>>, ext::set<ext::v
local.insert(transition.first.second);
}
- for(const auto& transition : n.getCallTransitions()) {
- if(dSubSet.count(transition.first.first))
- call.insert(transition.first.second);
- }
-
- for(const auto& transition : n.getReturnTransitions()) {
- if(dSubSet.count(std::get<0>(transition.first)))
- ret.insert(std::get<1>(transition.first));
- }
-
- return ext::make_tuple(std::move(local), std::move(call), std::move(ret));
+ return local;
}
template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType >
@@ -215,49 +85,50 @@ automaton::RealTimeHeightDeterministicDPDA < InputSymbolType, EpsilonType, ext::
if ( common::GlobalData::verbose )
common::Streams::log << "Dirty state symbol: " << stateSymbol << std::endl;
- ext::tuple<ext::set<ext::variant<EpsilonType, InputSymbolType>>, ext::set<ext::variant<EpsilonType, InputSymbolType>>, ext::set<ext::variant<EpsilonType, InputSymbolType>>> partitioning = getLocalCallRetPartitioning(n, stateSymbol.first);
-
- ext::set<ext::variant<EpsilonType, InputSymbolType>>& retPart = std::get<2>(partitioning);
+ ext::set<ext::variant<EpsilonType, InputSymbolType>> retPart = getRetPartitioning(n, stateSymbol.first);
const DeterministicStateType & state = stateSymbol.first;
const DeterministicPushdownStoreSymbolType & pdaSymbol = stateSymbol.second;
for(const ext::variant < EpsilonType, InputSymbolType > & input : retPart ) {
- if ( pdaSymbol == d.getBottomOfTheStackSymbol()) {
- DeterministicStateType to = retInitial ( state, input, n );
-
- if ( ! to.empty ( ) )
- addRetTransition ( state, input, pdaSymbol, std::move ( to ), d );
- else
- rubbishReturnTransitions.insert(ext::make_pair(state, pdaSymbol ) );
- } else {
- DeterministicStateType to = ret(state, pdaSymbol, input, n );
-
- if ( ! to.empty ( ) )
- addRetTransition ( state, input, pdaSymbol, std::move ( to ), d );
- else
- rubbishReturnTransitions.insert ( ext::make_pair ( state, pdaSymbol ) );
- }
+ DeterministicStateType to;
+
+ if ( pdaSymbol == d.getBottomOfTheStackSymbol ( ) )
+ to = retInitial ( state, input, n );
+ else
+ to = ret ( state, pdaSymbol, input, n );
+
+ if ( ! to.empty ( ) ) {
+ d.addState ( to );
+ d.addReturnTransition ( state, input, pdaSymbol, std::move ( to ) );
+ } else
+ rubbishReturnTransitions.insert ( ext::make_pair ( state, pdaSymbol ) );
}
}
for(const auto& state : states) {
if ( common::GlobalData::verbose )
common::Streams::log << "Dirty state: " << state << std::endl;
- ext::tuple<ext::set<ext::variant<EpsilonType, InputSymbolType>>, ext::set<ext::variant<EpsilonType, InputSymbolType>>, ext::set<ext::variant<EpsilonType, InputSymbolType>>> partitioning = getLocalCallRetPartitioning(n, state);
- ext::set<ext::variant<EpsilonType, InputSymbolType>>& localPart = std::get<0>(partitioning);
- ext::set<ext::variant<EpsilonType, InputSymbolType>>& callPart = std::get<1>(partitioning);
+ ext::set<ext::variant<EpsilonType, InputSymbolType>> localPart = getLocalPartitioning(n, state);
+ ext::set<ext::variant<EpsilonType, InputSymbolType>> callPart = getCallPartitioning(n, state);
for ( const ext::variant < EpsilonType, InputSymbolType > & input : localPart ) {
DeterministicStateType to = local ( state, input, n );
- if ( ! to.empty ( ) )
- addLocalTransition ( state, input, std::move ( to ), d );
+ if ( ! to.empty ( ) ) {
+ d.addState ( to );
+ d.addLocalTransition ( state, input, std::move ( to ) );
+ }
}
for ( const ext::variant < EpsilonType, InputSymbolType > & input : callPart ) {
DeterministicStateType to = call ( state, input, n );
- if ( ! to.empty ( ) )
- addCallTransition ( state, input, to, ext::make_pair ( state, input ), d );
+ if ( ! to.empty ( ) ) {
+ ext::pair < DeterministicStateType, ext::variant < EpsilonType, InputSymbolType > > pdaSymbol = ext::make_pair ( state, input );
+
+ d.addState ( to );
+ d.addPushdownStoreSymbol ( pdaSymbol );
+ d.addCallTransition ( state, input, std::move ( to ), std::move ( pdaSymbol ) );
+ }
}
}
}
diff --git a/alib2algo/src/automaton/determinize/DeterminizeVPAPart.hxx b/alib2algo/src/automaton/determinize/DeterminizeVPAPart.hxx
index b5fb44b3031d5038e92a368c35e1de5ab518b99d..ce5e46e16f49e9e1d9152d867b89379bbf98ec1d 100644
--- a/alib2algo/src/automaton/determinize/DeterminizeVPAPart.hxx
+++ b/alib2algo/src/automaton/determinize/DeterminizeVPAPart.hxx
@@ -15,152 +15,6 @@ namespace automaton {
namespace determinize {
-template < class InputSymbolType, class StateType >
-void addRetTransition(const ext::set < ext::pair < StateType, StateType > > & from, const InputSymbolType& input, const ext::pair < ext::set < ext::pair < StateType, StateType > >, InputSymbolType > & dvpdaSymbol, const ext::set < ext::pair < StateType, StateType > > & to, automaton::VisiblyPushdownDPDA < InputSymbolType, ext::pair < ext::set < ext::pair < StateType, StateType > >, InputSymbolType >, ext::set < ext::pair < StateType, StateType > > > & deterministic) {
- deterministic.addState(from);
- deterministic.addState(to);
- deterministic.addPushdownStoreSymbol(dvpdaSymbol);
-
- deterministic.addReturnTransition(from, input, dvpdaSymbol, to);
-}
-
-template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
-ext::set<ext::pair<StateType, StateType>> retInitial ( const ext::set < ext::pair < StateType, StateType > > & state, const InputSymbolType & input, const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & nondeterministic ) {
- const ext::set<ext::pair<StateType, StateType>> & S = state;
-
- 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()) {
- if(q2 != std::get<0>(transition.first)) continue;
- if(input != std::get<1>(transition.first)) continue;
- if(nondeterministic.getBottomOfTheStackSymbol() != std::get<2>(transition.first)) continue;
-
- for(const auto& to : transition.second) {
- const StateType& q1 = to;
- S1.insert(ext::make_pair(q, q1));
- }
- }
- }
-
- return S1;
-}
-
-template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
-ext::set<ext::pair<StateType, StateType>> ret(const ext::set < ext::pair < StateType, StateType > > & state, const ext::pair < ext::set < ext::pair < StateType, StateType > >, InputSymbolType > & pdaSymbol, const InputSymbolType & input, const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & nondeterministic ) {
- const ext::set<ext::pair<StateType, StateType>> & S = state;
- const ext::set<ext::pair<StateType, StateType>>& S1 = pdaSymbol.first;
-
- 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);
- for(const auto& to : transition.second) {
- const StateType& q1 = to.first;
- const PushdownStoreSymbolType& gamma = to.second;
-
- for(const auto& entry : S) {
- if(q1 != entry.first) continue;
- const StateType& q2 = entry.second;
-
- for(const auto& transition2 : nondeterministic.getReturnTransitions()) {
- if(q2 != std::get<0>(transition2.first)) continue;
- if(input != std::get<1>(transition2.first)) continue;
- if(gamma != std::get<2>(transition2.first)) continue;
-
- for(const auto& to2 : transition2.second) {
- const StateType& qI = to2;
-
- update.insert(ext::make_pair(q, qI));
- }
- }
- }
- }
- }
-
- 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) {
- if(q3 != entry2.first) continue;
-
- const StateType& qI = entry2.second;
-
- S2.insert(ext::make_pair(q, qI));
- }
- }
-
- return S2;
-}
-
-template < class InputSymbolType, class StateType >
-void addCallTransition(const ext::set < ext::pair < StateType, StateType > > & from, const InputSymbolType& input, const ext::set < ext::pair < StateType, StateType > >& to, const ext::pair < ext::set < ext::pair < StateType, StateType > >, InputSymbolType > & dvpdaSymbol, automaton::VisiblyPushdownDPDA < InputSymbolType, ext::pair < ext::set < ext::pair < StateType, StateType > >, InputSymbolType >, ext::set < ext::pair < StateType, StateType > > > & deterministic) {
- deterministic.addState(from);
- deterministic.addState(to);
- deterministic.addPushdownStoreSymbol(dvpdaSymbol);
-
- deterministic.addCallTransition(from, input, to, dvpdaSymbol);
-}
-
-template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
-ext::set<ext::pair<StateType, StateType>> call(const ext::set < ext::pair < StateType, StateType > > & state, const InputSymbolType& input, const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & nondeterministic ) {
- const ext::set<ext::pair<StateType, StateType>> & S = state;
-
- ext::set<StateType> R = retrieveDSubSet(S);
- ext::set<StateType> R1;
-
- for(const StateType& q : R) {
- for(const auto& transition : nondeterministic.getCallTransitions()) {
- if(q != transition.first.first) continue;
- if(input != transition.first.second) continue;
-
- for(const auto& to : transition.second) {
- const StateType& q1 = to.first;
-
- R1.insert(q1);
- }
- }
- }
-
- return createIdentity ( std::move ( R1 ) );
-}
-
-template < class InputSymbolType, class StateType >
-void addLocalTransition(const ext::set < ext::pair < StateType, StateType > > & from, const InputSymbolType & input, const ext::set < ext::pair < StateType, StateType > > & to, automaton::VisiblyPushdownDPDA < InputSymbolType, ext::pair < ext::set < ext::pair < StateType, StateType > >, InputSymbolType >, ext::set < ext::pair < StateType, StateType > > > & deterministic) {
- deterministic.addState(from);
- deterministic.addState(to);
-
- deterministic.addLocalTransition(from, input, to);
-}
-
-template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
-ext::set<ext::pair<StateType, StateType>> local(const ext::set < ext::pair < StateType, StateType > > & state, const InputSymbolType& input, const automaton::VisiblyPushdownNPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & nondeterministic ) {
- const ext::set<ext::pair<StateType, StateType>> & S = state;
- 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()) {
- if(q2 != transition.first.first) continue;
- if(input != transition.first.second) continue;
-
- for(const auto& to : transition.second) {
- const StateType & q1 = to;
-
- S1.insert(ext::make_pair(q, q1));
- }
- }
- }
-
- return S1;
-}
-
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 > & n ) {
using DeterministicStateType = ext::set < ext::pair < StateType, StateType > >;
@@ -187,23 +41,33 @@ automaton::VisiblyPushdownDPDA < InputSymbolType, ext::pair < ext::set < ext::pa
for ( const InputSymbolType & input : n.getReturnInputAlphabet ( ) ) {
if ( pdaSymbol == d.getBottomOfTheStackSymbol ( ) ) {
- DeterministicStateType to = retInitial ( state, input, n);
- addRetTransition ( state, input, pdaSymbol, std::move ( to ), d );
+ DeterministicStateType to = retInitial ( state, input, n );
+
+ d.addState ( to );
+ d.addReturnTransition ( state, input, pdaSymbol, std::move ( to ) );
} else {
DeterministicStateType to = ret ( state, pdaSymbol, input, n );
- addRetTransition ( state, input, pdaSymbol, std::move ( to ), d );
+
+ d.addState ( to );
+ d.addReturnTransition ( state, input, pdaSymbol, std::move ( to ) );
}
}
}
for ( const DeterministicStateType & state : states ) {
for ( const InputSymbolType & input : n.getLocalInputAlphabet ( ) ) {
- DeterministicStateType to = local(state, input, n );
- addLocalTransition ( state, input, std::move ( to ), d );
+ DeterministicStateType to = local ( state, input, n );
+
+ d.addState ( to );
+ d.addLocalTransition ( state, input, std::move ( to ) );
}
for ( const InputSymbolType & input : n.getCallInputAlphabet ( ) ) {
- DeterministicStateType to = call(state, input, n );
- addCallTransition ( state, input, std::move ( to ), ext::make_pair ( state, input ), d );
+ DeterministicStateType to = call ( state, input, n );
+ ext::pair < DeterministicStateType, InputSymbolType > pdaSymbol = ext::make_pair ( state, input );
+
+ d.addState ( to );
+ d.addPushdownStoreSymbol ( pdaSymbol );
+ d.addCallTransition ( state, input, std::move ( to ), std::move ( pdaSymbol ) );
}
}
}
diff --git a/alib2algo/src/automaton/determinize/common/RHDPDACommon.h b/alib2algo/src/automaton/determinize/common/RHDPDACommon.h
index b53774a22b4b9533cf244331b434daa238357414..d61d5ce6ef5849421628226e7ce973755c26def2 100644
--- a/alib2algo/src/automaton/determinize/common/RHDPDACommon.h
+++ b/alib2algo/src/automaton/determinize/common/RHDPDACommon.h
@@ -32,6 +32,126 @@ ext::set<ext::pair<StateType, StateType>> createIdentity(const ext::set<StateTyp
return id;
}
+template < class InputSymbolType, class StateType, class N >
+ext::set < ext::pair < StateType, StateType > > retInitial ( const ext::set < ext::pair < StateType, StateType > > & state, const InputSymbolType & input, const N & nondeterministic ) {
+ const ext::set<ext::pair<StateType, StateType>> & S = state;
+
+ 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()) {
+ if(q2 != std::get<0>(transition.first)) continue;
+ if(input != std::get<1>(transition.first)) continue;
+ if(nondeterministic.getBottomOfTheStackSymbol() != std::get<2>(transition.first)) continue;
+
+ for(const auto& to : transition.second) {
+ const StateType& q1 = to;
+ 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 > > & state, const DeterministicPushdownStoreSymbolType & pdaSymbol, const InputSymbolType & input, const N & nondeterministic ) {
+ const ext::set<ext::pair<StateType, StateType>> & S = state;
+ const ext::set<ext::pair<StateType, StateType>>& S1 = pdaSymbol.first;
+
+ 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);
+ for(const auto& to : transition.second) {
+ const StateType& q1 = to.first;
+ const auto & gamma = to.second;
+
+ for(const auto& entry : S) {
+ if(q1 != entry.first) continue;
+ const StateType& q2 = entry.second;
+
+ for(const auto& transition2 : nondeterministic.getReturnTransitions()) {
+ if(q2 != std::get<0>(transition2.first)) continue;
+ if(input != std::get<1>(transition2.first)) continue;
+ if(gamma != std::get<2>(transition2.first)) continue;
+
+ for(const auto& to2 : transition2.second) {
+ const StateType& qI = to2;
+
+ update.insert(ext::make_pair(q, qI));
+ }
+ }
+ }
+ }
+ }
+
+ 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) {
+ if(q3 != entry2.first) continue;
+
+ 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 > > & state, const InputSymbolType & input, const N & nondeterministic ) {
+ const ext::set < ext::pair < StateType, StateType > > & S = state;
+
+ ext::set < StateType > R = retrieveDSubSet(S);
+ ext::set < StateType > R1;
+
+ for(const StateType& q : R) {
+ for ( const auto & transition : nondeterministic.getCallTransitions()) {
+ if(q != transition.first.first) continue;
+ if(input != transition.first.second) continue;
+
+ for(const auto& to : transition.second) {
+ const StateType& q1 = to.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 > > & state, const InputSymbolType & input, const N & nondeterministic ) {
+ const ext::set<ext::pair<StateType, StateType>> & S = state;
+ 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()) {
+ if(q2 != transition.first.first) continue;
+ if(input != transition.first.second) continue;
+
+ for(const auto& to : transition.second) {
+ const StateType & q1 = to;
+
+ S1.insert(ext::make_pair(q, q1));
+ }
+ }
+ }
+
+ 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;