diff --git a/adeterminize.rhdpda/makefile b/adeterminize.rhdpda/makefile
new file mode 100644
index 0000000000000000000000000000000000000000..43ba50085733582654d168446141891a1659b02b
--- /dev/null
+++ b/adeterminize.rhdpda/makefile
@@ -0,0 +1,20 @@
+CC=g++
+EXECUTIBLE=adeterminize.rhdpda
+CCFLAGS= -std=c++11 -O2 -c -Wall -I../alib/src -I../adeterminize/src
+LDFLAGS= -L../alib/lib -L../adeterminize/lib -lxml2 -lalib -ladeterminize -Wl,-rpath,.
+
+SOURCES=$(shell find src/ -name *cpp)
+OBJECTS=$(patsubst src/%.cpp, obj/%.o, $(SOURCES))
+
+all: $(SOURCES) bin/$(EXECUTIBLE)
+
+bin/$(EXECUTIBLE): $(OBJECTS)
+ mkdir -p bin
+ $(CC) $(OBJECTS) -o $@ $(LDFLAGS)
+
+obj/%.o: src/%.cpp
+ mkdir -p $(dir $@)
+ $(CC) $(CCFLAGS) $< -o $@
+
+clean:
+ $(RM) -r *.o *.d bin obj
diff --git a/adeterminize.rhdpda/src/RHDPDADeterminizationStructs.h b/adeterminize.rhdpda/src/RHDPDADeterminizationStructs.h
new file mode 100644
index 0000000000000000000000000000000000000000..bf5e4b29365e33aed71da02d84f2e2b018b3da93
--- /dev/null
+++ b/adeterminize.rhdpda/src/RHDPDADeterminizationStructs.h
@@ -0,0 +1,93 @@
+#ifndef RHDPDADETERKMINIZATIONSTRUCTS_H_
+#define RHDPDADETERKMINIZATIONSTRUCTS_H_
+
+#include <set>
+
+using namespace automaton;
+
+namespace determinization {
+
+struct StateSymbolPair {
+ State state;
+ Symbol symbol;
+
+ StateSymbolPair(const State& state, const Symbol& symbol)
+ : state(state),
+ symbol(symbol) {}
+
+ bool operator < (const StateSymbolPair& other) const {
+ return (state < other.state) || ((state == other.state) && (symbol < other.symbol));
+ }
+
+ bool operator == (const StateSymbolPair& other) const {
+ return (state == other.state) && (symbol == other.symbol);
+ }
+
+ bool operator != (const StateSymbolPair& other) const {
+ return (state != other.state) || (symbol != other.symbol);
+ }
+};
+
+struct PairOfPairs {
+ StateSymbolPair pair1;
+ StateSymbolPair pair2;
+
+ PairOfPairs(const StateSymbolPair& pair1, const StateSymbolPair& pair2)
+ : pair1(pair1),
+ pair2(pair2) {}
+
+ bool operator < (const PairOfPairs& other) const {
+ return (pair1 < other.pair1) || ((pair1 == other.pair1) && (pair2 < other.pair2));
+ }
+
+ bool operator == (const PairOfPairs& other) const {
+ return (pair1 == other.pair1) && (pair2 == other.pair2);
+ }
+
+ bool operator != (const PairOfPairs& other) const {
+ return (pair1 != other.pair1) || (pair2 != other.pair2);
+ }
+};
+
+
+struct SComponent {
+ set<PairOfPairs> pairsOfPairs;
+ SComponent() {}
+ SComponent(const set<PairOfPairs>& pairsOfPairs)
+ : pairsOfPairs(pairsOfPairs) {}
+};
+
+
+struct RComponent {
+ set<StateSymbolPair> pairs;
+ RComponent() {}
+ RComponent(const set<StateSymbolPair>& pairs)
+ : pairs(pairs) {}
+};
+
+
+struct StateData {
+ State state;
+ SComponent s;
+ RComponent r;
+ bool isMarked;
+
+ StateData(const State& state, const SComponent& s, const RComponent& r)
+ : state(state),
+ s(s),
+ r(r),
+ isMarked(false) {}
+};
+
+
+struct PartialStackData {
+ SComponent s;
+ RComponent r;
+
+ PartialStackData(const SComponent& s, const RComponent& r)
+ : s(s),
+ r(r) {}
+};
+
+} /* namespace determinization */
+#endif /* RHDPDADETERKMINIZATIONSTRUCTS_H_ */
\ No newline at end of file
diff --git a/adeterminize.rhdpda/src/RHDPDADeterminizer.cpp b/adeterminize.rhdpda/src/RHDPDADeterminizer.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..bfa72149c2fb0d6fc1e4beb684c1ae8fc99272fb
--- /dev/null
+++ b/adeterminize.rhdpda/src/RHDPDADeterminizer.cpp
@@ -0,0 +1,374 @@
+#include "RHDPDADeterminizer.h"
+
+namespace determinization {
+
+const Symbol RHDPDADeterminizer::BOTTOM_OF_STACK_SYMBOL("_"); // TODO specialni symbol pro dno zasobniku zpusobuje chybu
+
+
+string RHDPDADeterminizer::buildPairName(const StateSymbolPair& pair) {
+ return "('" + pair.state.getName() + "', '" + pair.symbol.getSymbol() + "')";;
+}
+
+
+string RHDPDADeterminizer::buildStateName(const SComponent& s, const RComponent& r) {
+ string name = "{";
+ for (set<PairOfPairs>::const_iterator pairOfPairs = s.pairsOfPairs.begin();
+ pairOfPairs != s.pairsOfPairs.end();
+ pairOfPairs++) {
+ if (pairOfPairs != s.pairsOfPairs.begin()) {
+ name += ", ";
+ }
+ name += "(" + buildPairName(pairOfPairs->pair1) + ", " + buildPairName(pairOfPairs->pair2) + ")";
+ }
+ name += "}, {";
+ for (set<StateSymbolPair>::const_iterator pair = r.pairs.begin();
+ pair != r.pairs.end();
+ pair++) {
+ if (pair != r.pairs.begin()) {
+ name += ", ";
+ }
+ name += buildPairName(*pair);
+ }
+ return name + "}";
+}
+
+
+const State& RHDPDADeterminizer::getOrCreateState(const SComponent& s, const RComponent& r,
+ map<string, StateData>& states, PDA& rdpda) {
+ 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;
+ rdpda.addState(state);
+ return insertedData.state;
+}
+
+
+const SComponent RHDPDADeterminizer::getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs) {
+ set<PairOfPairs> pairsOfPairs;
+ for (set<StateSymbolPair>::const_iterator pair = pairs.begin(); pair != pairs.end(); pair++) {
+ pairsOfPairs.insert(PairOfPairs(*pair, *pair));
+ }
+ return SComponent(pairsOfPairs);
+}
+
+
+void RHDPDADeterminizer::divideTransitions(const set<TransitionPDA>& transitions, set<TransitionPDA>& internalTransitions,
+ set<TransitionPDA>& pushTransitions, set<TransitionPDA>& popTransitions) {
+ for (set<TransitionPDA>::iterator transition = transitions.begin(); transition != transitions.end(); transition++) {
+ if (transition->getPush().size() == 2) {
+ pushTransitions.insert(*transition);
+ } else if (transition->getPush().size() == 1) {
+ internalTransitions.insert(*transition);
+ } else {
+ popTransitions.insert(*transition);
+ }
+ }
+}
+
+
+string RHDPDADeterminizer::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input, PDA& rdpda) {
+ string name = "(" + buildStateName(s, r) + ")";
+ name += ", " + input.getSymbol();
+ try {
+ rdpda.addStackSymbol(name);
+ } catch (AutomatonException e) { /* Stack symbol already exists */ }
+ return name;
+}
+
+
+vector<SComponent> RHDPDADeterminizer::generateAllPossibleSComponents(set<StateSymbolPair>& pairs) {
+ // Generate all possible pairs of pairs
+ vector<PairOfPairs> possiblePairsOfPairs;
+ for (set<StateSymbolPair>::iterator pair1 = pairs.begin(); pair1 != pairs.end(); pair1++) {
+ for (set<StateSymbolPair>::iterator pair2 = pairs.begin(); pair2 != pairs.end(); pair2++) {
+ possiblePairsOfPairs.push_back(PairOfPairs(*pair1, *pair2));
+ }
+ }
+
+ // Generate all possible s components
+ vector<SComponent> possibleS;
+ int possibleSSize = pow(2, possiblePairsOfPairs.size());
+ for (int i = 0; i < possibleSSize; i++) {
+ set<PairOfPairs> pairsOfPairsSet;
+ int mask = 1;
+ for (vector<PairOfPairs>::iterator pairOfPairs = possiblePairsOfPairs.begin();
+ pairOfPairs != possiblePairsOfPairs.end();
+ pairOfPairs++) {
+ if ((i & mask) != 0) {
+ pairsOfPairsSet.insert(*pairOfPairs);
+ }
+ mask <<= 1;
+ }
+ possibleS.push_back(SComponent(pairsOfPairsSet));
+ }
+
+ return possibleS;
+}
+
+
+vector<RComponent> RHDPDADeterminizer::generateAllPossibleRComponents(set<StateSymbolPair>& pairs) {
+ // Generate all possible r components
+ vector<RComponent> possibleR;
+ int possibleRSize = pow(2, pairs.size());
+ for (int i = 0; i < possibleRSize; i++) {
+ set<StateSymbolPair> pairsSet;
+ int mask = 1;
+ for (set<StateSymbolPair>::iterator pair = pairs.begin(); pair != pairs.end(); pair++) {
+ if ((i & mask) != 0) {
+ pairsSet.insert(*pair);
+ }
+ mask <<= 1;
+ }
+ possibleR.push_back(RComponent(pairsSet));
+ }
+
+ return possibleR;
+}
+
+
+StateData* RHDPDADeterminizer::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;
+}
+
+
+set<StateSymbolPair> RHDPDADeterminizer::combineStatesWithSymbol(const set<State>& states, const Symbol& symbol) {
+ set<StateSymbolPair> pairs;
+ for (set<State>::iterator state = states.begin(); state != states.end(); state++) {
+ pairs.insert(StateSymbolPair(*state, symbol));
+ }
+ return pairs;
+}
+
+
+set<StateSymbolPair> RHDPDADeterminizer::buildAllStateSymbolPairs(PDA& rhdpda) {
+ set<StateSymbolPair> allStateSymbolPairs;
+ const set<State>& states = rhdpda.getStates();
+ const set<Symbol>& stackAlphabet = rhdpda.getStackAlphabet();
+ for (set<State>::iterator state = states.begin(); state != states.end(); state++) {
+ for (set<Symbol>::iterator symbol = stackAlphabet.begin(); symbol != stackAlphabet.end(); symbol++) {
+ allStateSymbolPairs.insert(StateSymbolPair(*state, *symbol));
+ }
+ }
+ return allStateSymbolPairs;
+}
+
+
+PDA RHDPDADeterminizer::determinize(PDA& rhdpda) {
+ PDA rdpda;
+ map<string, StateData> states;
+ const set<TransitionPDA>& transitions = rhdpda.getTransitions();
+ set<TransitionPDA> internalTransitions;
+ set<TransitionPDA> pushTransitions;
+ set<TransitionPDA> popTransitions;
+ set<StateSymbolPair> allStateSymbolPairs = buildAllStateSymbolPairs(rhdpda);
+ vector<SComponent> allScomponents = generateAllPossibleSComponents(allStateSymbolPairs);
+ vector<RComponent> allRcomponents = generateAllPossibleRComponents(allStateSymbolPairs);
+ const set<Symbol>& inputAlphabet = rhdpda.getInputAlphabet();
+
+ DeterminizationUtils::copyInputAlphabet(rhdpda, rdpda);
+ divideTransitions(transitions, internalTransitions, pushTransitions, popTransitions);
+
+ set<StateSymbolPair> initialSPairs = combineStatesWithSymbol(rhdpda.getStates(), BOTTOM_OF_STACK_SYMBOL);
+ set<StateSymbolPair> initialRPairs = combineStatesWithSymbol(rhdpda.getInitialStates(), BOTTOM_OF_STACK_SYMBOL);
+ const SComponent& initialS = getSComponentWithPairsIdentity(initialSPairs);
+ const RComponent& initialR(initialRPairs);
+ const State& initialState = getOrCreateState(initialS, initialR, states, rdpda);
+ rdpda.addInitialState(initialState);
+
+ while (true) {
+ StateData* unmarkedStateData = getUnmarkedState(states);
+ if (unmarkedStateData == NULL) {
+ break;
+ }
+
+ // Internal
+ for (set<Symbol>::iterator a = inputAlphabet.begin(); a != inputAlphabet.end(); a++) {
+ SComponent sPrimed;
+ SComponent& s = unmarkedStateData->s;
+ for (set<PairOfPairs>::iterator pairOfPairs = s.pairsOfPairs.begin();
+ pairOfPairs != s.pairsOfPairs.end();
+ pairOfPairs++) {
+ const StateSymbolPair& x = pairOfPairs->pair1;
+ const State& r = pairOfPairs->pair2.state;
+ const Symbol& Y = pairOfPairs->pair2.symbol;
+ for (set<TransitionPDA>::iterator transition = internalTransitions.begin();
+ transition != internalTransitions.end();
+ transition++) {
+ if (transition->getFrom() == r && transition->getInput() == *a && transition->getPop().front() == Y) {
+ const State& q = transition->getTo();
+ sPrimed.pairsOfPairs.insert(PairOfPairs(x, StateSymbolPair(q, Y)));
+ }
+ }
+ }
+ RComponent rPrimed;
+ RComponent& r = unmarkedStateData->r;
+ for (set<StateSymbolPair>::iterator pair = r.pairs.begin(); pair != r.pairs.end(); pair++) {
+ const State& p = pair->state;
+ const Symbol& Y = pair->symbol;
+ for (set<TransitionPDA>::iterator transition = internalTransitions.begin();
+ transition != internalTransitions.end();
+ transition++) {
+ if (transition->getFrom() == p && transition->getInput() == *a && transition->getPop().front() == Y) {
+ const State& q = transition->getTo();
+ rPrimed.pairs.insert(StateSymbolPair(q, Y));
+ }
+ }
+ }
+ if (sPrimed.pairsOfPairs.size() > 0 && rPrimed.pairs.size() > 0) {
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = getOrCreateState(sPrimed, rPrimed, states, rdpda);
+ const TransitionPDA transition(fromState, *a, toState);
+ rdpda.addTransition(transition);
+ }
+ }
+
+ // Push
+ for (set<Symbol>::iterator a = inputAlphabet.begin(); a != inputAlphabet.end(); a++) {
+ SComponent sDoublePrimed = getSComponentWithPairsIdentity(allStateSymbolPairs);
+ SComponent& s = unmarkedStateData->s;
+ RComponent rDoublePrimed;
+ RComponent& r = unmarkedStateData->r;
+ for (set<StateSymbolPair>::iterator pair = r.pairs.begin(); pair != r.pairs.end(); pair++) {
+ const State& p = pair->state;
+ const Symbol& Y = pair->symbol;
+ for (set<TransitionPDA>::iterator transition = pushTransitions.begin();
+ transition != pushTransitions.end();
+ transition++) {
+ if (transition->getFrom() == p && transition->getInput() == *a && transition->getPop().front() == Y) {
+ const State& q = transition->getTo();
+ const Symbol& Z = transition->getPush().front();
+ rDoublePrimed.pairs.insert(StateSymbolPair(q, Z));
+ }
+ }
+ }
+ if (rDoublePrimed.pairs.size() > 0) {
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = getOrCreateState(sDoublePrimed, rDoublePrimed, states, rdpda);
+ string stackSymbolName = buildStackSymbolName(s, r, *a, rdpda);
+ list<Symbol> pop;
+ list<Symbol> push(1, Symbol(stackSymbolName));
+ const TransitionPDA transition(fromState, *a, toState, pop, push);
+ rdpda.addTransition(transition);
+ }
+ }
+
+ // Pop
+ for (set<Symbol>::iterator a = inputAlphabet.begin(); a != inputAlphabet.end(); a++) {
+ for (set<Symbol>::iterator b = inputAlphabet.begin(); b != inputAlphabet.end(); b++) {
+ SComponent& s = unmarkedStateData->s;
+
+ set<PairOfPairs> update;
+ for (set<PairOfPairs>::iterator pairOfPairs = s.pairsOfPairs.begin();
+ pairOfPairs != s.pairsOfPairs.end();
+ pairOfPairs++) {
+ const State& r = pairOfPairs->pair1.state;
+ const Symbol& Z = pairOfPairs->pair1.symbol;
+ const State& rPrimed = pairOfPairs->pair2.state;
+ if (pairOfPairs->pair2.symbol == Z) {
+ for (set<TransitionPDA>::iterator pushTransition = pushTransitions.begin();
+ pushTransition != pushTransitions.end();
+ pushTransition++) {
+ for (set<TransitionPDA>::iterator popTransition = popTransitions.begin();
+ popTransition != popTransitions.end();
+ popTransition++) {
+ const State& p = pushTransition->getFrom();
+ const State& q = popTransition->getTo();
+ if (pushTransition->getInput() == *a && pushTransition->getTo() == r &&
+ popTransition->getInput() == *b && popTransition->getFrom() == rPrimed &&
+ pushTransition->getPush().front() == Z && popTransition->getPop().front() == Z) {
+ const Symbol& Y = pushTransition->getPop().front();
+ StateSymbolPair pair1(p, Y);
+ StateSymbolPair pair2(q, Y);
+ update.insert(PairOfPairs(pair1, pair2));
+ }
+ }
+ }
+ }
+ }
+ if (update.size() == 0) {
+ continue;
+ }
+
+ for (vector<SComponent>::iterator sPrimed = allScomponents.begin();
+ sPrimed != allScomponents.end();
+ sPrimed++) {
+ for (vector<RComponent>::iterator rPrimed = allRcomponents.begin();
+ rPrimed != allRcomponents.end();
+ rPrimed++) {
+ RComponent rDoublePrimed;
+ for (set<PairOfPairs>::iterator updateItem = update.begin();
+ updateItem != update.end();
+ updateItem++) {
+ const StateSymbolPair& y = updateItem->pair1;
+ const StateSymbolPair& x = updateItem->pair2;
+ if (rPrimed->pairs.find(y) != rPrimed->pairs.end()) {
+ rDoublePrimed.pairs.insert(x);
+ }
+ }
+ SComponent sDoublePrimed;
+ for (set<PairOfPairs>::iterator updateItem = update.begin();
+ updateItem != update.end();
+ updateItem++) {
+ const StateSymbolPair& z = updateItem->pair1;
+ const StateSymbolPair& y = updateItem->pair2;
+ for (set<PairOfPairs>::iterator sPrimedPair = sPrimed->pairsOfPairs.begin();
+ sPrimedPair != sPrimed->pairsOfPairs.end();
+ sPrimedPair++) {
+ if (sPrimedPair->pair2 == z) {
+ const StateSymbolPair& x = sPrimedPair->pair1;
+ sDoublePrimed.pairsOfPairs.insert(PairOfPairs(x, y));
+ }
+ }
+ }
+ if (sDoublePrimed.pairsOfPairs.size() > 0 && rDoublePrimed.pairs.size() > 0) {
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = getOrCreateState(sDoublePrimed, rDoublePrimed, states, rdpda);
+ string stackSymbolName = buildStackSymbolName(*sPrimed, *rPrimed, *a, rdpda);
+ list<Symbol> pop(1, Symbol(stackSymbolName));
+ list<Symbol> push;
+ const TransitionPDA transition(fromState, *b, toState, pop, push);
+ rdpda.addTransition(transition);
+ }
+ }
+ }
+ }
+ }
+ }
+
+ const set<State>& rhdpdaFinalState = rhdpda.getFinalStates();
+ for (map<string, StateData>::iterator state = states.begin();
+ state != states.end();
+ state++) {
+ bool isFinalState = false;
+ RComponent& r = state->second.r;
+ for (set<StateSymbolPair>::iterator pair = r.pairs.begin();
+ pair != r.pairs.end();
+ pair++) {
+ if (rhdpdaFinalState.find(pair->state) != rhdpdaFinalState.end()) {
+ isFinalState = true;
+ }
+ }
+ if (isFinalState) {
+ rdpda.addFinalState(state->second.state);
+ }
+ }
+
+ return rdpda;
+}
+
+} /* namespace determinization */
diff --git a/adeterminize.rhdpda/src/RHDPDADeterminizer.h b/adeterminize.rhdpda/src/RHDPDADeterminizer.h
new file mode 100644
index 0000000000000000000000000000000000000000..701dbd16e9ad6bdd68cff18a0479a923a30ac509
--- /dev/null
+++ b/adeterminize.rhdpda/src/RHDPDADeterminizer.h
@@ -0,0 +1,45 @@
+#ifndef RHDPDADETERMINZER_H_
+#define RHDPDADETERMINZER_H_
+
+#include <string>
+#include <set>
+#include <map>
+#include <vector>
+
+#include "automaton/PDA/PDA.h"
+#include "automaton/Transition.h"
+#include "automaton/exception/AutomatonException.h"
+#include "alphabet/Symbol.h"
+#include "DeterminizationUtils.h"
+#include "RHDPDADeterminizationStructs.h"
+
+using namespace std;
+using namespace automaton;
+using namespace alphabet;
+
+namespace determinization {
+
+class RHDPDADeterminizer {
+protected:
+ static const Symbol BOTTOM_OF_STACK_SYMBOL;
+
+ static string buildPairName(const StateSymbolPair& pair);
+ static string buildStateName(const SComponent& s, const RComponent& r);
+ static const State& getOrCreateState(const SComponent& s, const RComponent& r, map<string, StateData>& states,
+ PDA& rdpda);
+ static const SComponent getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs);
+ static void divideTransitions(const set<TransitionPDA>& transitions, set<TransitionPDA>& internalTransitions,
+ set<TransitionPDA>& pushTransitions, set<TransitionPDA>& popTransitions);
+ static string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input, PDA& rdpda);
+ static vector<SComponent> generateAllPossibleSComponents(set<StateSymbolPair>& pairs);
+ static vector<RComponent> generateAllPossibleRComponents(set<StateSymbolPair>& pairs);
+ static StateData* getUnmarkedState(map<string, StateData>& states);
+ static set<StateSymbolPair> combineStatesWithSymbol(const set<State>& states, const Symbol& symbol);
+ static set<StateSymbolPair> buildAllStateSymbolPairs(PDA& rhdpda);
+
+public:
+ static PDA determinize(PDA& automaton);
+};
+
+} /* namespace determinization */
+#endif /* RHDPDADETERMINZER_H_ */
\ No newline at end of file
diff --git a/adeterminize.rhdpda/src/adeterminize.rhdpda.cpp b/adeterminize.rhdpda/src/adeterminize.rhdpda.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..9eceab0f6c3f51c957195dca86fbdde47d1716f9
--- /dev/null
+++ b/adeterminize.rhdpda/src/adeterminize.rhdpda.cpp
@@ -0,0 +1,34 @@
+#include <iostream>
+#include <set>
+
+#include "automaton/UnknownAutomaton.h"
+#include "AutomatonFactory.h"
+#include "AlibException.h"
+#include "RHDPDADeterminizer.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 RHDPDA
+ PDA deterministicPDA = RHDPDADeterminizer::determinize(*((PDA*) knownAutomaton));
+ deterministicPDA.toXML(cout);
+
+ delete knownAutomaton;
+
+ } catch (AlibException& e) {
+ cout << e.what() << endl;
+ return 0;
+ }
+}
diff --git a/examples/RHDPDA2.xml b/examples/RHDPDA2.xml
new file mode 100644
index 0000000000000000000000000000000000000000..b6ee03f349e36ed2ceb39723ece9befd8b101d90
--- /dev/null
+++ b/examples/RHDPDA2.xml
@@ -0,0 +1,226 @@
+<automaton>
+ <states>
+ <state>0</state>
+ <state>1</state>
+ <state>2</state>
+ <state>3</state>
+ <state>ERR</state>
+ </states>
+ <inputAlphabet>
+ <symbol>a</symbol>
+ <symbol>b</symbol>
+ </inputAlphabet>
+ <stackAlphabet>
+ <symbol>a</symbol>
+ <symbol>x</symbol>
+ <symbol>_</symbol>
+ </stackAlphabet>
+ <transitions>
+ <transition>
+ <from>0</from>
+ <input>a</input>
+ <to>1</to>
+ <pop>
+ <symbol>_</symbol>
+ </pop>
+ <push>
+ <symbol>x</symbol>
+ <symbol>_</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>0</from>
+ <input>b</input>
+ <to>3</to>
+ <pop>
+ <symbol>_</symbol>
+ </pop>
+ <push>
+ <symbol>_</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>1</from>
+ <input>a</input>
+ <to>1</to>
+ <pop>
+ <symbol>a</symbol>
+ </pop>
+ <push>
+ <symbol>a</symbol>
+ <symbol>a</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>1</from>
+ <input>a</input>
+ <to>1</to>
+ <pop>
+ <symbol>x</symbol>
+ </pop>
+ <push>
+ <symbol>a</symbol>
+ <symbol>x</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>1</from>
+ <input>b</input>
+ <to>2</to>
+ <pop>
+ <symbol>a</symbol>
+ </pop>
+ <push>
+ <symbol>a</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>1</from>
+ <input>b</input>
+ <to>2</to>
+ <pop>
+ <symbol>x</symbol>
+ </pop>
+ <push>
+ <symbol>x</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>2</from>
+ <input>a</input>
+ <to>2</to>
+ <pop>
+ <symbol>a</symbol>
+ </pop>
+ <push></push>
+ </transition>
+ <transition>
+ <from>2</from>
+ <input>a</input>
+ <to>3</to>
+ <pop>
+ <symbol>x</symbol>
+ </pop>
+ <push></push>
+ </transition>
+ <transition>
+ <from>2</from>
+ <input>b</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>a</symbol>
+ </pop>
+ <push>
+ <symbol>a</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>2</from>
+ <input>b</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>x</symbol>
+ </pop>
+ <push>
+ <symbol>x</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>3</from>
+ <input>a</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>_</symbol>
+ </pop>
+ <push>
+ <symbol>_</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>3</from>
+ <input>b</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>_</symbol>
+ </pop>
+ <push>
+ <symbol>_</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>ERR</from>
+ <input>a</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>_</symbol>
+ </pop>
+ <push>
+ <symbol>_</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>ERR</from>
+ <input>a</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>a</symbol>
+ </pop>
+ <push>
+ <symbol>a</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>ERR</from>
+ <input>a</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>x</symbol>
+ </pop>
+ <push>
+ <symbol>x</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>ERR</from>
+ <input>b</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>_</symbol>
+ </pop>
+ <push>
+ <symbol>_</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>ERR</from>
+ <input>b</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>a</symbol>
+ </pop>
+ <push>
+ <symbol>a</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>ERR</from>
+ <input>b</input>
+ <to>ERR</to>
+ <pop>
+ <symbol>x</symbol>
+ </pop>
+ <push>
+ <symbol>x</symbol>
+ </push>
+ </transition>
+ </transitions>
+ <initialStates>
+ <state>0</state>
+ </initialStates>
+ <startSymbols>
+ <symbol>_</symbol>
+ </startSymbols>
+ <finalStates>
+ <state>3</state>
+ </finalStates>
+</automaton>
diff --git a/examples/RHDPDA4.xml b/examples/RHDPDA4.xml
new file mode 100644
index 0000000000000000000000000000000000000000..8ca65104a14e75ce1cfee6e26b00cfbef215873d
--- /dev/null
+++ b/examples/RHDPDA4.xml
@@ -0,0 +1,45 @@
+<automaton>
+ <states>
+ <state>0</state>
+ <state>1</state>
+ </states>
+ <inputAlphabet>
+ <symbol>a</symbol>
+ </inputAlphabet>
+ <stackAlphabet>
+ <symbol>a</symbol>
+ <symbol>_</symbol>
+ </stackAlphabet>
+ <transitions>
+ <transition>
+ <from>0</from>
+ <input>a</input>
+ <to>1</to>
+ <pop>
+ <symbol>_</symbol>
+ </pop>
+ <push>
+ <symbol>a</symbol>
+ <symbol>_</symbol>
+ </push>
+ </transition>
+ <transition>
+ <from>1</from>
+ <input>a</input>
+ <to>0</to>
+ <pop>
+ <symbol>a</symbol>
+ </pop>
+ <push></push>
+ </transition>
+ </transitions>
+ <initialStates>
+ <state>0</state>
+ </initialStates>
+ <startSymbols>
+ <symbol>_</symbol>
+ </startSymbols>
+ <finalStates>
+ <state>0</state>
+ </finalStates>
+</automaton>
diff --git a/makefile b/makefile
index 9b5fb54ceb16ac2680085f094f5de86d6582fc6e..3958ffa67c0195d0ced76f40241dc8a4ec161665 100644
--- a/makefile
+++ b/makefile
@@ -6,7 +6,7 @@ SUBDIRS_LIBS = alib adeterminize
SUBDIRS_BINS = acat \
aconvert aconvert.dot aconvert.gastex aconvert.regexp aconvert.automaton aconvert.grammar \
aminimize \
- adeterminize.fsm adeterminize.idpda adeterminize.vpa adeterminize.vpa2 adeterminize.vpa3 \
+ adeterminize.fsm adeterminize.idpda adeterminize.vpa adeterminize.vpa2 adeterminize.vpa3 adeterminize.rhdpda \
adiff adiff.automaton adiff.grammar \
aepsilon \
atrim \