diff --git a/adeterminize.vpa/src/VPADeterminizer.cpp b/adeterminize.vpa/src/VPADeterminizer.cpp
index 8227d968fa1f77d09a9aee8975841dafc4760d56..9cca7a21452d479570c814551b4218b3c2a2c1ac 100644
--- a/adeterminize.vpa/src/VPADeterminizer.cpp
+++ b/adeterminize.vpa/src/VPADeterminizer.cpp
@@ -1,196 +1,36 @@
#include "VPADeterminizer.h"
namespace determinization {
-
-const Symbol VPADeterminizer::BOTTOM_OF_STACK_SYMBOL("⊥");
-
-
-string VPADeterminizer::buildStateName(const SComponent& s, const RComponent& r) {
- string name = "{";
- for (set<StatesPair>::const_iterator statesPair = s.statesPairs.begin();
- statesPair != s.statesPairs.end();
- statesPair++) {
- if (statesPair != s.statesPairs.begin()) {
- name += ", ";
- }
- name += "('" + statesPair->state1.getName() + "', '" + statesPair->state2.getName() + "')";
- }
- name += "}, {";
- for (set<State>::const_iterator state = r.states.begin(); state != r.states.end(); state++) {
- if (state != r.states.begin()) {
- name += ", ";
- }
- name += "'" + state->getName() + "'";
- }
- name += "}";
- return name;
-}
-
-
-const State& VPADeterminizer::getOrCreateState(const SComponent& s, const RComponent& r) {
- string stateName = this->buildStateName(s, r);
-
- map<string, StateData>::iterator statesIter = this->states.find(stateName);
- if (statesIter != this->states.end()) {
- return statesIter->second.state;
- }
-
- State state(stateName);
- StateData stateData(state, s, r);
- StateData& insertedData = this->states.insert(pair<string, StateData>(stateName, stateData)).first->second;
- this->deterministicVPA->addState(state);
- return insertedData.state;
-}
-
-
-const VPADeterminizer::SComponent VPADeterminizer::getSComponentWithStatesIdentity() {
- set<State> states = this->nondeterministicVPA->getStates();
- set<StatesPair> statesPairs;
- for (set<State>::const_iterator state = states.begin(); state != states.end(); state++) {
- statesPairs.insert(StatesPair(*state, *state));
- }
- return SComponent(statesPairs);
-}
-
-
-void VPADeterminizer::divideInputAlphabet() {
- this->internalSymbols.clear();
- this->callSymbols.clear();
- this->returnSymbols.clear();
- set<Symbol> alphabet = this->nondeterministicVPA->getInputAlphabet();
- set<TransitionPDA> transitions = this->nondeterministicVPA->getTransitions();
- for (set<Symbol>::iterator input = alphabet.begin(); input != alphabet.end(); input++) {
- for (set<TransitionPDA>::iterator transition = transitions.begin();
- transition != transitions.end();
- transition++) {
- if (transition->getInput() == *input) {
- if (transition->getPush().size() != 0) {
- this->callSymbols.insert(*input);
- } else if (transition->getPop().size() != 0) {
- this->returnSymbols.insert(*input);
- } else {
- this->internalSymbols.insert(*input);
- }
- break;
- }
- }
- }
-}
-
-
-string VPADeterminizer::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input) {
- string name = "(" + this->buildStateName(s, r) + ")";
- name += ", " + input.getSymbol();
- return name;
-}
-
-void VPADeterminizer::buildStackAlphabet() {
- const set<State>& states = this->nondeterministicVPA->getStates();
-
- // Generate all possible states pairs
- vector<StatesPair> possibleStatesPairs;
- for (set<State>::iterator state1 = states.begin(); state1 != states.end(); state1++) {
- for (set<State>::iterator state2 = states.begin(); state2 != states.end(); state2++) {
- possibleStatesPairs.push_back(StatesPair(*state1, *state2));
- }
- }
-
- // Generate all possible s components
- vector<SComponent> possibleS;
- int possibleSSize = pow(2, possibleStatesPairs.size());
- for (int i = 0; i < possibleSSize; i++) {
- set<StatesPair> statesPairsSet;
- int mask = 1;
- for (vector<StatesPair>::iterator statesPair = possibleStatesPairs.begin();
- statesPair != possibleStatesPairs.end();
- statesPair++) {
- if ((i & mask) != 0) {
- statesPairsSet.insert(*statesPair);
- }
- mask <<= 1;
- }
- possibleS.push_back(SComponent(statesPairsSet));
- }
-
- // Generate all possible r components
- vector<RComponent> possibleR;
- int possibleRSize = pow(2, states.size());
- for (int i = 0; i < possibleRSize; i++) {
- set<State> statesSet;
- int mask = 1;
- for (set<State>::iterator state = states.begin(); state != states.end(); state++) {
- if ((i & mask) != 0) {
- statesSet.insert(*state);
- }
- mask <<= 1;
- }
- possibleR.push_back(RComponent(statesSet));
- }
-
- // Generate whole stack alphabet
- set<Symbol> alphabet = this->nondeterministicVPA->getInputAlphabet();
- for (vector<SComponent>::iterator s = possibleS.begin(); s != possibleS.end(); s++) {
- for (vector<RComponent>::iterator r = possibleR.begin(); r != possibleR.end(); r++) {
- this->partialStackAlphabet.push_back(PartialStackData(*s, *r));
- for (set<Symbol>::iterator callSymbol = this->callSymbols.begin();
- callSymbol != this->callSymbols.end();
- callSymbol++) {
- string stackSymbolName = this->buildStackSymbolName(*s, *r, *callSymbol);
- this->deterministicVPA->addStackSymbol(Symbol(stackSymbolName));
- }
- }
- }
-
- // Add bottom of stack symbol
- this->deterministicVPA->addStackSymbol(BOTTOM_OF_STACK_SYMBOL);
-}
-
-
-VPADeterminizer::StateData* VPADeterminizer::getUnmarkedState() {
- StateData* unmarkedStateData = NULL;
- for (map<string, StateData>::iterator stateIter = this->states.begin();
- stateIter != this->states.end();
- stateIter++) {
- if (!stateIter->second.isMarked) {
- unmarkedStateData = &stateIter->second;
- unmarkedStateData->isMarked = true;
- return unmarkedStateData;
- }
- }
- return NULL;
-}
-
-
-VPADeterminizer::VPADeterminizer(PDA* automaton) {
- this->nondeterministicVPA = automaton;
-}
+PDA VPADeterminizer::determinize(PDA& nondeterministicVPA) {
+ PDA deterministicVPA;
+ map<string, StateData> states;
+ set<Symbol> internalSymbols;
+ set<Symbol> callSymbols;
+ set<Symbol> returnSymbols;
-PDA* VPADeterminizer::determinize() {
- this->deterministicVPA = new PDA();
- DeterminizationUtils::copyInputAlphabet(*this->nondeterministicVPA, *this->deterministicVPA);
- this->divideInputAlphabet();
- this->states.clear();
- this->partialStackAlphabet.clear();
- this->buildStackAlphabet();
+ DeterminizationUtils::copyInputAlphabet(nondeterministicVPA, deterministicVPA);
+ VPADeterminizationUtils::divideInputAlphabet(nondeterministicVPA, internalSymbols, callSymbols, returnSymbols);
+ vector<PartialStackData> partialStackAlphabet = VPADeterminizationUtils::buildStackAlphabet(nondeterministicVPA,
+ deterministicVPA, callSymbols);
- const SComponent& initialStateS = this->getSComponentWithStatesIdentity();
- const RComponent& initialStateR(this->nondeterministicVPA->getInitialStates());
- const State& initialState = this->getOrCreateState(initialStateS, initialStateR);
- this->deterministicVPA->addInitialState(initialState);
+ const SComponent& initialS = VPADeterminizationUtils::getSComponentWithStatesIdentity(nondeterministicVPA.getStates());
+ const RComponent& initialR(nondeterministicVPA.getInitialStates());
+ const State& initialState = VPADeterminizationUtils::getOrCreateState(initialS, initialR, states, deterministicVPA);
+ deterministicVPA.addInitialState(initialState);
- set<TransitionPDA> transitions = this->nondeterministicVPA->getTransitions();
+ set<TransitionPDA> transitions = nondeterministicVPA.getTransitions();
while (true) {
- StateData* unmarkedStateData = this->getUnmarkedState();
+ StateData* unmarkedStateData = VPADeterminizationUtils::getUnmarkedState(states);
if (unmarkedStateData == NULL) {
break;
}
// Internal symbols
- for (set<Symbol>::iterator internalSymbol = this->internalSymbols.begin();
- internalSymbol != this->internalSymbols.end();
+ for (set<Symbol>::iterator internalSymbol = internalSymbols.begin();
+ internalSymbol != internalSymbols.end();
internalSymbol++) {
SComponent sPrimed;
SComponent& s = unmarkedStateData->s;
@@ -221,14 +61,14 @@ PDA* VPADeterminizer::determinize() {
}
}
const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
+ const State& toState = VPADeterminizationUtils::getOrCreateState(sPrimed, rPrimed, states, deterministicVPA);
const TransitionPDA transition(fromState, *internalSymbol, toState);
- this->deterministicVPA->addTransition(transition);
+ deterministicVPA.addTransition(transition);
}
// Call symbols
- for (set<Symbol>::iterator callSymbol = this->callSymbols.begin();
- callSymbol != this->callSymbols.end();
+ for (set<Symbol>::iterator callSymbol = callSymbols.begin();
+ callSymbol != callSymbols.end();
callSymbol++) {
RComponent rPrimed;
RComponent& r = unmarkedStateData->r;
@@ -243,24 +83,25 @@ PDA* VPADeterminizer::determinize() {
}
}
SComponent& s = unmarkedStateData->s;
+ const SComponent& sPrimed = VPADeterminizationUtils::getSComponentWithStatesIdentity(nondeterministicVPA.getStates());
const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(this->getSComponentWithStatesIdentity(), rPrimed);
- string stackSymbolName = this->buildStackSymbolName(s, r, *callSymbol);
+ const State& toState = VPADeterminizationUtils::getOrCreateState(sPrimed, rPrimed, states, deterministicVPA);
+ string stackSymbolName = VPADeterminizationUtils::buildStackSymbolName(s, r, *callSymbol);
list<Symbol> pop;
list<Symbol> push(1, Symbol(stackSymbolName));
const TransitionPDA transition(fromState, *callSymbol, toState, pop, push);
- this->deterministicVPA->addTransition(transition);
+ deterministicVPA.addTransition(transition);
}
// Return symbols
- for (set<Symbol>::iterator returnSymbol = this->returnSymbols.begin();
- returnSymbol != this->returnSymbols.end();
+ for (set<Symbol>::iterator returnSymbol = returnSymbols.begin();
+ returnSymbol != returnSymbols.end();
returnSymbol++) {
SComponent& s = unmarkedStateData->s;
RComponent& r = unmarkedStateData->r;
// Empty stack
- list<Symbol> bottomOfStack(1, BOTTOM_OF_STACK_SYMBOL);
+ list<Symbol> bottomOfStack(1, VPADeterminizationUtils::BOTTOM_OF_STACK_SYMBOL);
SComponent sPrimed;
for (set<StatesPair>::iterator statesPair = s.statesPairs.begin();
statesPair != s.statesPairs.end();
@@ -290,16 +131,14 @@ PDA* VPADeterminizer::determinize() {
}
}
const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- list<Symbol> pop(1, BOTTOM_OF_STACK_SYMBOL);
+ const State& toState = VPADeterminizationUtils::getOrCreateState(sPrimed, rPrimed, states, deterministicVPA);
+ list<Symbol> pop(1, VPADeterminizationUtils::BOTTOM_OF_STACK_SYMBOL);
list<Symbol> push;
const TransitionPDA transition(fromState, *returnSymbol, toState, pop, push);
- this->deterministicVPA->addTransition(transition);
+ deterministicVPA.addTransition(transition);
// Otherwise
- for (set<Symbol>::iterator callSymbol = this->callSymbols.begin();
- callSymbol != this->callSymbols.end();
- callSymbol++) {
+ for (set<Symbol>::iterator callSymbol = callSymbols.begin(); callSymbol != callSymbols.end(); callSymbol++) {
set<StatesPair> update;
for (set<StatesPair>::iterator sPair = s.statesPairs.begin();
sPair != s.statesPairs.end();
@@ -328,8 +167,8 @@ PDA* VPADeterminizer::determinize() {
continue;
}
- for (vector<PartialStackData>::iterator partialStackSymbol = this->partialStackAlphabet.begin();
- partialStackSymbol != this->partialStackAlphabet.end();
+ for (vector<PartialStackData>::iterator partialStackSymbol = partialStackAlphabet.begin();
+ partialStackSymbol != partialStackAlphabet.end();
partialStackSymbol++) {
SComponent& sPrimed = partialStackSymbol->s;
RComponent& rPrimed = partialStackSymbol->r;
@@ -361,28 +200,27 @@ PDA* VPADeterminizer::determinize() {
}
const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(sPrimed, rPrimed, *callSymbol);
+ const State& toState = VPADeterminizationUtils::getOrCreateState(sDoublePrimed, rDoublePrimed,
+ states, deterministicVPA);
+ string stackSymbolName = VPADeterminizationUtils::buildStackSymbolName(sPrimed, rPrimed, *callSymbol);
list<Symbol> pop(1, Symbol(stackSymbolName));
list<Symbol> push;
const TransitionPDA transition(fromState, *returnSymbol, toState, pop, push);
- this->deterministicVPA->addTransition(transition);
+ deterministicVPA.addTransition(transition);
}
}
}
}
// Final states
- for (map<string, StateData>::iterator stateIter = this->states.begin();
- stateIter != this->states.end();
- stateIter++) {
+ for (map<string, StateData>::iterator stateIter = states.begin(); stateIter != states.end(); stateIter++) {
const StateData& stateData = stateIter->second;
- if (DeterminizationUtils::containSomeFinalStateOfAutomaton(stateData.r.states, *this->nondeterministicVPA)) {
- this->deterministicVPA->addFinalState(stateData.state);
+ if (DeterminizationUtils::containSomeFinalStateOfAutomaton(stateData.r.states, nondeterministicVPA)) {
+ deterministicVPA.addFinalState(stateData.state);
}
}
- return this->deterministicVPA;
+ return deterministicVPA;
}
} /* namespace determinization */
diff --git a/adeterminize.vpa/src/VPADeterminizer.h b/adeterminize.vpa/src/VPADeterminizer.h
index fee14797e9acd326538b588cbe1e87cd87d2b6e6..a208ce094e9f1711d4cfb310078c8e060dfc7f18 100644
--- a/adeterminize.vpa/src/VPADeterminizer.h
+++ b/adeterminize.vpa/src/VPADeterminizer.h
@@ -1,8 +1,6 @@
#ifndef VPADETERMINIZER_H_
#define VPADETERMINIZER_H_
-#include <iostream>
-#include <math.h>
#include <string>
#include <set>
#include <map>
@@ -10,9 +8,10 @@
#include "automaton/PDA/PDA.h"
#include "automaton/Transition.h"
-#include "automaton/exception/AutomatonException.h"
#include "alphabet/Symbol.h"
#include "DeterminizationUtils.h"
+#include "VPADeterminizationUtils.h"
+#include "VPADeterminizationStructs.h"
using namespace std;
using namespace automaton;
@@ -21,86 +20,8 @@ using namespace alphabet;
namespace determinization {
class VPADeterminizer {
-protected:
- struct StatesPair {
- State state1;
- State state2;
-
- StatesPair(const State& state1, const State& state2)
- : state1(state1),
- state2(state2) {}
-
- bool operator < (const StatesPair& other) const {
- return state1 < other.state1 || state1 == other.state1 && state2 < other.state2;
- }
-
- bool operator == (const StatesPair& other) const {
- return state1 == other.state1 && state2 == other.state2;
- }
-
- bool operator != (const StatesPair& other) const {
- return state1 != other.state1 || state2 != other.state2;
- }
- };
-
- struct SComponent {
- set<StatesPair> statesPairs;
- SComponent() {}
- SComponent(const set<StatesPair>& statesPairs)
- : statesPairs(statesPairs) {}
- };
-
- struct RComponent {
- set<State> states;
- RComponent() {}
- RComponent(const set<State>& states)
- : states(states) {}
- };
-
- struct StateData {
- State state;
- SComponent s;
- RComponent r;
- bool isMarked;
-
- StateData(const State& state, const SComponent& s, const RComponent& r)
- : s(s),
- r(r),
- state(state),
- isMarked(false) {}
- };
-
- struct PartialStackData {
- SComponent s;
- RComponent r;
-
- PartialStackData(const SComponent& s, const RComponent& r)
- : s(s),
- r(r) {}
- };
-
- PDA* nondeterministicVPA;
- PDA* deterministicVPA;
- map<string, StateData> states;
- vector<PartialStackData> partialStackAlphabet;
- set<Symbol> internalSymbols;
- set<Symbol> callSymbols;
- set<Symbol> returnSymbols;
-
- string buildStateName(const SComponent& s, const RComponent& r);
- const State& getOrCreateState(const SComponent& s, const RComponent& r);
- const SComponent getSComponentWithStatesIdentity();
- void divideInputAlphabet();
- string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input);
- void buildStackAlphabet();
- StateData* getUnmarkedState();
-
public:
- static const Symbol BOTTOM_OF_STACK_SYMBOL;
-
- VPADeterminizer(PDA* automaton);
- PDA* determinize();
-
+ static PDA determinize(PDA& automaton);
};
} /* namespace determinization */
diff --git a/adeterminize.vpa/src/adeterminize.vpa.cpp b/adeterminize.vpa/src/adeterminize.vpa.cpp
index c29150b4b2d73a12d787623fdf6394540384527f..fccb49688abe7e4db7608540bcd204d32619d861 100644
--- a/adeterminize.vpa/src/adeterminize.vpa.cpp
+++ b/adeterminize.vpa/src/adeterminize.vpa.cpp
@@ -22,12 +22,10 @@ int main(int argc, char** argv) {
Automaton* knownAutomaton = AutomatonFactory::buildAutomaton(automaton);
// TODO check that automaton is VPA
- VPADeterminizer determinizer((PDA*) knownAutomaton);
- PDA* deterministicVPA = determinizer.determinize();
- deterministicVPA->toXML(cout);
+ PDA deterministicVPA = VPADeterminizer::determinize(*((PDA*) knownAutomaton));
+ deterministicVPA.toXML(cout);
delete knownAutomaton;
- delete deterministicVPA;
} catch (AlibException& e) {
cout << e.what() << endl;
diff --git a/adeterminize/src/VPADeterminizationStructs.h b/adeterminize/src/VPADeterminizationStructs.h
new file mode 100644
index 0000000000000000000000000000000000000000..29772cdcb5b44e14dcc6fd25ac81bb473fe48d46
--- /dev/null
+++ b/adeterminize/src/VPADeterminizationStructs.h
@@ -0,0 +1,72 @@
+#ifndef VPADETERKMINIZATIONSTRUCTS_H_
+#define VPADETERKMINIZATIONSTRUCTS_H_
+
+#include <set>
+
+using namespace automaton;
+
+namespace determinization {
+
+struct StatesPair {
+ State state1;
+ State state2;
+
+ StatesPair(const State& state1, const State& state2)
+ : state1(state1),
+ state2(state2) {}
+
+ bool operator < (const StatesPair& other) const {
+ return state1 < other.state1 || state1 == other.state1 && state2 < other.state2;
+ }
+
+ bool operator == (const StatesPair& other) const {
+ return state1 == other.state1 && state2 == other.state2;
+ }
+
+ bool operator != (const StatesPair& other) const {
+ return state1 != other.state1 || state2 != other.state2;
+ }
+};
+
+
+struct SComponent {
+ set<StatesPair> statesPairs;
+ SComponent() {}
+ SComponent(const set<StatesPair>& statesPairs)
+ : statesPairs(statesPairs) {}
+};
+
+
+struct RComponent {
+ set<State> states;
+ RComponent() {}
+ RComponent(const set<State>& states)
+ : states(states) {}
+};
+
+
+struct StateData {
+ State state;
+ SComponent s;
+ RComponent r;
+ bool isMarked;
+
+ StateData(const State& state, const SComponent& s, const RComponent& r)
+ : s(s),
+ r(r),
+ state(state),
+ isMarked(false) {}
+};
+
+
+struct PartialStackData {
+ SComponent s;
+ RComponent r;
+
+ PartialStackData(const SComponent& s, const RComponent& r)
+ : s(s),
+ r(r) {}
+};
+
+} /* namespace determinization */
+#endif /* VPADETERKMINIZATIONSTRUCTS_H_ */
\ No newline at end of file
diff --git a/adeterminize/src/VPADeterminizationUtils.cpp b/adeterminize/src/VPADeterminizationUtils.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..b08063e169498d14b449a5945ae79df4dad2a0a7
--- /dev/null
+++ b/adeterminize/src/VPADeterminizationUtils.cpp
@@ -0,0 +1,162 @@
+#include "VPADeterminizationUtils.h"
+
+namespace determinization {
+
+const Symbol VPADeterminizationUtils::BOTTOM_OF_STACK_SYMBOL("⊥");
+
+
+string VPADeterminizationUtils::buildStateName(const SComponent& s, const RComponent& r) {
+ string name = "{";
+ for (set<StatesPair>::const_iterator statesPair = s.statesPairs.begin();
+ statesPair != s.statesPairs.end();
+ statesPair++) {
+ if (statesPair != s.statesPairs.begin()) {
+ name += ", ";
+ }
+ name += "('" + statesPair->state1.getName() + "', '" + statesPair->state2.getName() + "')";
+ }
+ name += "}, {";
+ for (set<State>::const_iterator state = r.states.begin(); state != r.states.end(); state++) {
+ if (state != r.states.begin()) {
+ name += ", ";
+ }
+ name += "'" + state->getName() + "'";
+ }
+ name += "}";
+ return name;
+}
+
+
+const State& VPADeterminizationUtils::getOrCreateState(const SComponent& s, const RComponent& r, map<string,
+ StateData>& states,PDA& deterministicVPA) {
+ string stateName = buildStateName(s, r);
+
+ map<string, StateData>::iterator statesIter = states.find(stateName);
+ if (statesIter != states.end()) {
+ return statesIter->second.state;
+ }
+
+ State state(stateName);
+ StateData stateData(state, s, r);
+ StateData& insertedData = states.insert(pair<string, StateData>(stateName, stateData)).first->second;
+ deterministicVPA.addState(state);
+ return insertedData.state;
+}
+
+
+const SComponent VPADeterminizationUtils::getSComponentWithStatesIdentity(const set<State>& states) {
+ set<StatesPair> statesPairs;
+ for (set<State>::const_iterator state = states.begin(); state != states.end(); state++) {
+ statesPairs.insert(StatesPair(*state, *state));
+ }
+ return SComponent(statesPairs);
+}
+
+
+void VPADeterminizationUtils::divideInputAlphabet(PDA& nondeterministicVPA, set<Symbol>& internalSymbols,
+ set<Symbol>& callSymbols, set<Symbol>& returnSymbols) {
+ const set<Symbol>& alphabet = nondeterministicVPA.getInputAlphabet();
+ const set<TransitionPDA>& transitions = nondeterministicVPA.getTransitions();
+ for (set<Symbol>::iterator input = alphabet.begin(); input != alphabet.end(); input++) {
+ for (set<TransitionPDA>::iterator transition = transitions.begin();
+ transition != transitions.end();
+ transition++) {
+ if (transition->getInput() == *input) {
+ if (transition->getPush().size() != 0) {
+ callSymbols.insert(*input);
+ } else if (transition->getPop().size() != 0) {
+ returnSymbols.insert(*input);
+ } else {
+ internalSymbols.insert(*input);
+ }
+ break;
+ }
+ }
+ }
+}
+
+
+string VPADeterminizationUtils::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input) {
+ string name = "(" + buildStateName(s, r) + ")";
+ name += ", " + input.getSymbol();
+ return name;
+}
+
+
+vector<PartialStackData> VPADeterminizationUtils::buildStackAlphabet(PDA& nondeterministicVPA, PDA& deterministicVPA,
+ set<Symbol>& callSymbols) {
+ vector<PartialStackData> partialStackAlphabet;
+ const set<State>& states = nondeterministicVPA.getStates();
+
+ // Generate all possible states pairs
+ vector<StatesPair> possibleStatesPairs;
+ for (set<State>::iterator state1 = states.begin(); state1 != states.end(); state1++) {
+ for (set<State>::iterator state2 = states.begin(); state2 != states.end(); state2++) {
+ possibleStatesPairs.push_back(StatesPair(*state1, *state2));
+ }
+ }
+
+ // Generate all possible s components
+ vector<SComponent> possibleS;
+ int possibleSSize = pow(2, possibleStatesPairs.size());
+ for (int i = 0; i < possibleSSize; i++) {
+ set<StatesPair> statesPairsSet;
+ int mask = 1;
+ for (vector<StatesPair>::iterator statesPair = possibleStatesPairs.begin();
+ statesPair != possibleStatesPairs.end();
+ statesPair++) {
+ if ((i & mask) != 0) {
+ statesPairsSet.insert(*statesPair);
+ }
+ mask <<= 1;
+ }
+ possibleS.push_back(SComponent(statesPairsSet));
+ }
+
+ // Generate all possible r components
+ vector<RComponent> possibleR;
+ int possibleRSize = pow(2, states.size());
+ for (int i = 0; i < possibleRSize; i++) {
+ set<State> statesSet;
+ int mask = 1;
+ for (set<State>::iterator state = states.begin(); state != states.end(); state++) {
+ if ((i & mask) != 0) {
+ statesSet.insert(*state);
+ }
+ mask <<= 1;
+ }
+ possibleR.push_back(RComponent(statesSet));
+ }
+
+ // Generate whole stack alphabet
+ set<Symbol> alphabet = nondeterministicVPA.getInputAlphabet();
+ for (vector<SComponent>::iterator s = possibleS.begin(); s != possibleS.end(); s++) {
+ for (vector<RComponent>::iterator r = possibleR.begin(); r != possibleR.end(); r++) {
+ partialStackAlphabet.push_back(PartialStackData(*s, *r));
+ for (set<Symbol>::iterator callSymbol = callSymbols.begin(); callSymbol != callSymbols.end(); callSymbol++) {
+ string stackSymbolName = buildStackSymbolName(*s, *r, *callSymbol);
+ deterministicVPA.addStackSymbol(Symbol(stackSymbolName));
+ }
+ }
+ }
+
+ // Add bottom of stack symbol
+ deterministicVPA.addStackSymbol(BOTTOM_OF_STACK_SYMBOL);
+
+ return partialStackAlphabet;
+}
+
+
+StateData* VPADeterminizationUtils::getUnmarkedState(map<string, StateData>& states) {
+ StateData* unmarkedStateData = NULL;
+ for (map<string, StateData>::iterator stateIter = states.begin(); stateIter != states.end(); stateIter++) {
+ if (!stateIter->second.isMarked) {
+ unmarkedStateData = &stateIter->second;
+ unmarkedStateData->isMarked = true;
+ return unmarkedStateData;
+ }
+ }
+ return NULL;
+}
+
+} /* namespace determinization */
diff --git a/adeterminize/src/VPADeterminizationUtils.h b/adeterminize/src/VPADeterminizationUtils.h
new file mode 100644
index 0000000000000000000000000000000000000000..f24f318c2644ad15b902ea0b527d189f2af45442
--- /dev/null
+++ b/adeterminize/src/VPADeterminizationUtils.h
@@ -0,0 +1,38 @@
+#ifndef VPADETERKMINIZATIONUTILS_H_
+#define VPADETERKMINIZATIONUTILS_H_
+
+#include <math.h>
+#include <string>
+#include <set>
+#include <map>
+#include <vector>
+
+#include "automaton/PDA/PDA.h"
+#include "automaton/Transition.h"
+#include "alphabet/Symbol.h"
+#include "VPADeterminizationStructs.h"
+
+using namespace automaton;
+using namespace alphabet;
+
+namespace determinization {
+
+class VPADeterminizationUtils {
+public:
+ static const Symbol BOTTOM_OF_STACK_SYMBOL;
+
+ static string buildStateName(const SComponent& s, const RComponent& r);
+ static const State& getOrCreateState(const SComponent& s, const RComponent& r, map<string, StateData>& states,
+ PDA& deterministicVPA);
+ static const SComponent getSComponentWithStatesIdentity(const set<State>& states);
+ static void divideInputAlphabet(PDA& nondeterministicVPA, set<Symbol>& internalSymbols, set<Symbol>& callSymbols,
+ set<Symbol>& returnSymbols);
+ static string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input);
+ static vector<PartialStackData> buildStackAlphabet(PDA& nondeterministicVPA, PDA& deterministicVPA,
+ set<Symbol>& callSymbols);
+ static StateData* getUnmarkedState(map<string, StateData>& states);
+
+};
+
+} /* namespace determinization */
+#endif /* VPADETERKMINIZATIONUTILS_H_ */
\ No newline at end of file