diff --git a/adeterminize.vpa3/src/VPADeterminizer3.cpp b/adeterminize.vpa3/src/VPADeterminizer3.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..a4e0016072c981c01f2f548bf6cf3a070f0856b8
--- /dev/null
+++ b/adeterminize.vpa3/src/VPADeterminizer3.cpp
@@ -0,0 +1,277 @@
+#include "VPADeterminizer3.h"
+
+namespace determinization {
+
+
+string VPADeterminizer3::buildStateName(const SComponent& s) {
+ 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 += "}";
+ return name;
+}
+
+
+string VPADeterminizer3::buildStackSymbolName(const SComponent& s, const Symbol& input) {
+ string name = "(" + buildStateName(s) + ")";
+ name += ", " + input.getSymbol();
+ return name;
+}
+
+
+const State& VPADeterminizer3::getOrCreateState(const SComponent& s, map<string, StateData>& states,
+ PDA& deterministicVPA) {
+ string stateName = buildStateName(s);
+
+ map<string, StateData>::iterator statesIter = states.find(stateName);
+ if (statesIter != states.end()) {
+ return statesIter->second.state;
+ }
+
+ State state(stateName);
+ StateData stateData(state, s);
+ StateData& insertedData = states.insert(pair<string, StateData>(stateName, stateData)).first->second;
+ deterministicVPA.addState(state);
+ return insertedData.state;
+}
+
+
+vector<SComponent> VPADeterminizer3::buildStackAlphabet(PDA& nondeterministicVPA, PDA& deterministicVPA,
+ set<Symbol>& callSymbols) {
+ 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 = partial stack alphabet
+ vector<SComponent> partialStackAlphabet;
+ 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;
+ }
+ partialStackAlphabet.push_back(SComponent(statesPairsSet));
+ }
+
+ // Generate whole stack alphabet
+ set<Symbol> alphabet = nondeterministicVPA.getInputAlphabet();
+ for (vector<SComponent>::iterator s = partialStackAlphabet.begin(); s != partialStackAlphabet.end(); s++) {
+ for (set<Symbol>::iterator callSymbol = callSymbols.begin(); callSymbol != callSymbols.end(); callSymbol++) {
+ string stackSymbolName = VPADeterminizer3::buildStackSymbolName(*s, *callSymbol);
+ deterministicVPA.addStackSymbol(Symbol(stackSymbolName));
+ }
+ }
+
+ // Add bottom of stack symbol
+ deterministicVPA.addStackSymbol(VPADeterminizationUtils::BOTTOM_OF_STACK_SYMBOL);
+
+ return partialStackAlphabet;
+}
+
+
+PDA VPADeterminizer3::determinize(PDA& nondeterministicVPA) {
+ PDA deterministicVPA;
+ map<string, StateData> states;
+ set<Symbol> internalSymbols;
+ set<Symbol> callSymbols;
+ set<Symbol> returnSymbols;
+
+ DeterminizationUtils::copyInputAlphabet(nondeterministicVPA, deterministicVPA);
+ VPADeterminizationUtils::divideInputAlphabet(nondeterministicVPA, internalSymbols, callSymbols, returnSymbols);
+ vector<SComponent> partialStackAlphabet = VPADeterminizer3::buildStackAlphabet(nondeterministicVPA,
+ deterministicVPA, callSymbols);
+
+ const SComponent& initialS = VPADeterminizationUtils::getSComponentWithStatesIdentity(
+ nondeterministicVPA.getInitialStates());
+ const State& initialState = VPADeterminizer3::getOrCreateState(initialS, states, deterministicVPA);
+ deterministicVPA.addInitialState(initialState);
+
+ set<TransitionPDA> transitions = nondeterministicVPA.getTransitions();
+
+ while (true) {
+ StateData* unmarkedStateData = VPADeterminizationUtils::getUnmarkedState(states);
+ if (unmarkedStateData == NULL) {
+ break;
+ }
+
+ // Internal symbols
+ for (set<Symbol>::iterator internalSymbol = internalSymbols.begin();
+ internalSymbol != internalSymbols.end();
+ internalSymbol++) {
+ SComponent sPrimed;
+ SComponent& s = unmarkedStateData->s;
+ for (set<StatesPair>::iterator statesPair = s.statesPairs.begin();
+ statesPair != s.statesPairs.end();
+ statesPair++) {
+ const State& q = statesPair->state1;
+ const State& qDoublePrimed = statesPair->state2;
+ for (set<TransitionPDA>::iterator transition = transitions.begin();
+ transition != transitions.end();
+ transition++) {
+ if (transition->getFrom() == qDoublePrimed && transition->getInput() == *internalSymbol) {
+ const State& qPrimed = transition->getTo();
+ sPrimed.statesPairs.insert(StatesPair(q, qPrimed));
+ }
+ }
+ }
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = VPADeterminizer3::getOrCreateState(sPrimed, states, deterministicVPA);
+ const TransitionPDA transition(fromState, *internalSymbol, toState);
+ deterministicVPA.addTransition(transition);
+ }
+
+ // Call symbols
+ for (set<Symbol>::iterator callSymbol = callSymbols.begin();
+ callSymbol != callSymbols.end();
+ callSymbol++) {
+ RComponent rPrimed;
+ SComponent& s = unmarkedStateData->s;
+ for (set<StatesPair>::iterator statesPair = s.statesPairs.begin();
+ statesPair != s.statesPairs.end();
+ statesPair++) {
+ const State& q = statesPair->state2;
+ for (set<TransitionPDA>::iterator transition = transitions.begin();
+ transition != transitions.end();
+ transition++) {
+ if (transition->getFrom() == q && transition->getInput() == *callSymbol) {
+ const State& qPrimed = transition->getTo();
+ rPrimed.states.insert(qPrimed);
+ }
+ }
+ }
+ const SComponent& sPrimed = VPADeterminizationUtils::getSComponentWithStatesIdentity(rPrimed.states);
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = VPADeterminizer3::getOrCreateState(sPrimed, states, deterministicVPA);
+ string stackSymbolName = VPADeterminizer3::buildStackSymbolName(s, *callSymbol);
+ list<Symbol> pop;
+ list<Symbol> push(1, Symbol(stackSymbolName));
+ const TransitionPDA transition(fromState, *callSymbol, toState, pop, push);
+ deterministicVPA.addTransition(transition);
+ }
+
+ // Return symbols
+ for (set<Symbol>::iterator returnSymbol = returnSymbols.begin();
+ returnSymbol != returnSymbols.end();
+ returnSymbol++) {
+ SComponent& s = unmarkedStateData->s;
+
+ // Empty stack
+ list<Symbol> bottomOfStack(1, VPADeterminizationUtils::BOTTOM_OF_STACK_SYMBOL);
+ SComponent sPrimed;
+ for (set<StatesPair>::iterator statesPair = s.statesPairs.begin();
+ statesPair != s.statesPairs.end();
+ statesPair++) {
+ const State& q = statesPair->state1;
+ const State& qDoublePrimed = statesPair->state2;
+ for (set<TransitionPDA>::iterator transition = transitions.begin();
+ transition != transitions.end();
+ transition++) {
+ if (transition->getFrom() == qDoublePrimed && transition->getInput() == *returnSymbol &&
+ transition->getPop() == bottomOfStack) {
+ const State& qPrimed = transition->getTo();
+ sPrimed.statesPairs.insert(StatesPair(q, qPrimed));
+ }
+ }
+ }
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = VPADeterminizer3::getOrCreateState(sPrimed, states, deterministicVPA);
+ list<Symbol> pop(1, VPADeterminizationUtils::BOTTOM_OF_STACK_SYMBOL);
+ list<Symbol> push;
+ const TransitionPDA transition(fromState, *returnSymbol, toState, pop, push);
+ deterministicVPA.addTransition(transition);
+
+ // Otherwise
+ 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();
+ sPair++) {
+ const State& q1 = sPair->state1;
+ const State& q2 = sPair->state2;
+ for (set<TransitionPDA>::iterator transitionPush = transitions.begin();
+ transitionPush != transitions.end();
+ transitionPush++) {
+ for (set<TransitionPDA>::iterator transitionPop = transitions.begin();
+ transitionPop != transitions.end();
+ transitionPop++) {
+ const State& q = transitionPush->getFrom();
+ const State& qPrimed = transitionPop->getTo();
+ if (transitionPush->getInput() == *callSymbol && transitionPush->getTo() == q1 &&
+ transitionPop->getInput() == *returnSymbol && transitionPop->getFrom() == q2 &&
+ transitionPush->getPush() == transitionPop->getPop()) {
+ update.insert(StatesPair(q, qPrimed));
+ }
+ }
+ }
+ }
+ if (update.size() == 0) {
+ continue;
+ }
+
+ for (vector<SComponent>::iterator partialStackSymbol = partialStackAlphabet.begin();
+ partialStackSymbol != partialStackAlphabet.end();
+ partialStackSymbol++) {
+ SComponent& sPrimed = *partialStackSymbol;
+ SComponent sDoublePrimed;
+ for (set<StatesPair>::iterator updateItem = update.begin();
+ updateItem != update.end();
+ updateItem++) {
+ const State& q3 = updateItem->state1;
+ const State& qPrimed = updateItem->state2;
+ for (set<StatesPair>::iterator sPrimedPair = sPrimed.statesPairs.begin();
+ sPrimedPair != sPrimed.statesPairs.end();
+ sPrimedPair++) {
+ if (sPrimedPair->state2 == q3) {
+ const State& q = sPrimedPair->state1;
+ sDoublePrimed.statesPairs.insert(StatesPair(q, qPrimed));
+ }
+ }
+ }
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = VPADeterminizer3::getOrCreateState(sDoublePrimed, states, deterministicVPA);
+ string stackSymbolName = VPADeterminizer3::buildStackSymbolName(sPrimed, *callSymbol);
+ list<Symbol> pop(1, Symbol(stackSymbolName));
+ list<Symbol> push;
+ const TransitionPDA transition(fromState, *returnSymbol, toState, pop, push);
+ deterministicVPA.addTransition(transition);
+ }
+ }
+ }
+ }
+
+ // Final states
+ for (map<string, StateData>::iterator stateIter = states.begin(); stateIter != states.end(); stateIter++) {
+ const StateData& stateData = stateIter->second;
+ set<State> secondStates;
+ for (set<StatesPair>::iterator sPair = stateData.s.statesPairs.begin();
+ sPair != stateData.s.statesPairs.end();
+ sPair++) {
+ secondStates.insert(sPair->state2);
+ }
+ if (DeterminizationUtils::containSomeFinalStateOfAutomaton(secondStates, nondeterministicVPA)) {
+ deterministicVPA.addFinalState(stateData.state);
+ }
+ }
+
+ return deterministicVPA;
+}
+
+} /* namespace determinization */
diff --git a/adeterminize.vpa3/src/VPADeterminizer3.h b/adeterminize.vpa3/src/VPADeterminizer3.h
new file mode 100644
index 0000000000000000000000000000000000000000..f1a252f5d10e0abd97d57c2d866a3c0fc4880f84
--- /dev/null
+++ b/adeterminize.vpa3/src/VPADeterminizer3.h
@@ -0,0 +1,34 @@
+#ifndef VPADETERMINIZER2_H_
+#define VPADETERMINIZER2_H_
+
+#include <string>
+#include <set>
+#include <map>
+#include <vector>
+
+#include "automaton/PDA/PDA.h"
+#include "automaton/Transition.h"
+#include "alphabet/Symbol.h"
+#include "DeterminizationUtils.h"
+#include "VPADeterminizationUtils.h"
+#include "VPADeterminizationStructs.h"
+
+using namespace std;
+using namespace automaton;
+using namespace alphabet;
+
+namespace determinization {
+
+class VPADeterminizer3 {
+protected:
+ static string buildStateName(const SComponent& s);
+ static string buildStackSymbolName(const SComponent& s, const Symbol& input);
+ static const State& getOrCreateState(const SComponent& s, map<string, StateData>& states, PDA& deterministicVPA);
+ static vector<SComponent> buildStackAlphabet(PDA& nondeterministicVPA, PDA& deterministicVPA, set<Symbol>& callSymbols);
+
+public:
+ static PDA determinize(PDA& automaton);
+};
+
+} /* namespace determinization */
+#endif /* VPADETERMINIZER2_H_ */
\ No newline at end of file
diff --git a/adeterminize.vpa3/src/adeterminize.vpa3.cpp b/adeterminize.vpa3/src/adeterminize.vpa3.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..364824b69ae6fbd3c488b9d26cadc3da6c541d7e
--- /dev/null
+++ b/adeterminize.vpa3/src/adeterminize.vpa3.cpp
@@ -0,0 +1,34 @@
+#include <iostream>
+#include <set>
+
+#include "automaton/UnknownAutomaton.h"
+#include "AutomatonFactory.h"
+#include "AlibException.h"
+#include "VPADeterminizer3.h"
+
+
+using namespace std;
+using namespace automaton;
+using namespace determinization;
+using namespace alib;
+
+
+int main(int argc, char** argv) {
+ UnknownAutomaton automaton;
+
+ try {
+ string input(istreambuf_iterator<char>(cin), (istreambuf_iterator<char>()));
+ automaton = AutomatonFactory::fromString(input);
+
+ Automaton* knownAutomaton = AutomatonFactory::buildAutomaton(automaton);
+ // TODO check that automaton is VPA
+ PDA deterministicVPA = VPADeterminizer3::determinize(*((PDA*) knownAutomaton));
+ deterministicVPA.toXML(cout);
+
+ delete knownAutomaton;
+
+ } catch (AlibException& e) {
+ cout << e.what() << endl;
+ return 0;
+ }
+}
\ No newline at end of file
diff --git a/adeterminize/src/VPADeterminizationStructs.h b/adeterminize/src/VPADeterminizationStructs.h
index 29772cdcb5b44e14dcc6fd25ac81bb473fe48d46..cdf196a15be8980975bf06980d7e6add87c26a0f 100644
--- a/adeterminize/src/VPADeterminizationStructs.h
+++ b/adeterminize/src/VPADeterminizationStructs.h
@@ -56,6 +56,11 @@ struct StateData {
r(r),
state(state),
isMarked(false) {}
+
+ StateData(const State& state, const SComponent& s)
+ : s(s),
+ state(state),
+ isMarked(false) {}
};