From fc68c6734748f25f456545061899be4be380cc6a Mon Sep 17 00:00:00 2001
From: Jan Vesely <janvesely@janvesely.net>
Date: Thu, 24 Apr 2014 18:13:38 +0200
Subject: [PATCH] add rhdpda determinization with optimized s-component
---
adeterminize/src/adeterminize.cpp | 10 +-
.../src/rhdpda/RhdpdaDeterminizer3.cpp | 237 ++++++++++++++++++
adeterminize/src/rhdpda/RhdpdaDeterminizer3.h | 131 ++++++++++
3 files changed, 373 insertions(+), 5 deletions(-)
create mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer3.cpp
create mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer3.h
diff --git a/adeterminize/src/adeterminize.cpp b/adeterminize/src/adeterminize.cpp
index 5f0e608b44..6fc8bff09d 100644
--- a/adeterminize/src/adeterminize.cpp
+++ b/adeterminize/src/adeterminize.cpp
@@ -17,6 +17,7 @@
#include "vpa/VpaDeterminizer3.h"
#include "rhdpda/RhdpdaDeterminizer.h"
#include "rhdpda/RhdpdaDeterminizer2.h"
+#include "rhdpda/RhdpdaDeterminizer3.h"
using namespace std;
using namespace automaton;
@@ -32,7 +33,7 @@ void printHelp() {
cout << "Usage: adeterminize -t TYPE [SWITCH...]" << endl;
cout << "Possible arguments:" << endl;
cout << " -t, --type=TYPE \t Specifies type of input automaton, possible values are 'FSM' for final-state machine, 'IDPDA' for input-driven pushdown automaton, 'VPA' for visible pushdown automaton and 'RHDPDA' for real-time height deterministic pushdown automaton." << endl;
- cout << " -a, --algorithm=VERSION_OF_ALGORITHM \t Specifies version of algorithm. This argument works only with VPA or RHDPDA type. VPA determinization has 3 versions (use numbers 1, 2 and 3) and RHDPDA determinization has 2 versions (use numbers 1, 2). Default value is always number 1." << endl;
+ cout << " -a, --algorithm=VERSION_OF_ALGORITHM \t Specifies version of algorithm. This argument works only with VPA or RHDPDA type. VPA determinization has 3 versions (use numbers 1, 2 and 3) and RHDPDA determinization has also 3 versions (use numbers 1, 2 and 3). Default value is always number 1." << endl;
cout << " -h, --help \t Displays this help message." << endl;
cout << endl;
}
@@ -41,20 +42,19 @@ void printHelp() {
Determinizer* getVpaDeterminizer(Automaton* automaton, string version) {
if (version == "3") {
return new vpa::VpaDeterminizer3((PDA*) automaton);
-
} else if (version == "2") {
return new vpa::VpaDeterminizer2((PDA*) automaton);
}
-
return new vpa::VpaDeterminizer((PDA*) automaton);
}
Determinizer* getRhdpdaDeterminizer(Automaton* automaton, string version) {
- if (version == "2") {
+ if (version == "3") {
+ return new rhdpda::RhdpdaDeterminizer3((PDA*) automaton);
+ } else if (version == "2") {
return new rhdpda::RhdpdaDeterminizer2((PDA*) automaton);
}
-
return new rhdpda::RhdpdaDeterminizer((PDA*) automaton);
}
diff --git a/adeterminize/src/rhdpda/RhdpdaDeterminizer3.cpp b/adeterminize/src/rhdpda/RhdpdaDeterminizer3.cpp
new file mode 100644
index 0000000000..57ea354fbb
--- /dev/null
+++ b/adeterminize/src/rhdpda/RhdpdaDeterminizer3.cpp
@@ -0,0 +1,237 @@
+#include "RhdpdaDeterminizer3.h"
+
+namespace determinization {
+namespace rhdpda {
+
+
+void RhdpdaDeterminizer3::divideTransitions()
+{
+ for (const auto& transition : this->rhdpda->getTransitions()) {
+ if (transition.getPush().size() == 1) {
+ this->pushTransitions.insert(transition);
+ } else if (transition.getPop().size() == 1) {
+ this->popTransitions.insert(transition);
+ } else {
+ this->internalTransitions.insert(transition);
+ }
+ }
+}
+
+
+string RhdpdaDeterminizer3::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input)
+{
+ return RhdpdaUtils::buildStackSymbolName(s, r, input, *this->rdpda);
+}
+
+
+set<StateSymbolPair> RhdpdaDeterminizer3::combineStatesWithSymbol(const set<State>& states, const Symbol& symbol)
+{
+ return RhdpdaUtils::combineStatesWithSymbol(states, symbol);
+}
+
+
+const SComponent RhdpdaDeterminizer3::getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs)
+{
+ return RhdpdaUtils::getSComponentWithPairsIdentity(pairs);
+}
+
+
+const State& RhdpdaDeterminizer3::getOrCreateState(const SComponent& s, const RComponent& r)
+{
+ return RhdpdaUtils::getOrCreateState(s, r, this->states, *this->rdpda);
+}
+
+
+void RhdpdaDeterminizer3::initDeterminization()
+{
+ this->states.clear();
+ this->internalTransitions.clear();
+ this->pushTransitions.clear();
+ this->popTransitions.clear();
+
+ this->allStateSymbolPairs = RhdpdaUtils::buildAllStateSymbolPairs(*this->rhdpda);
+ this->allSComponents = RhdpdaUtils::generateAllPossibleSComponents(this->allStateSymbolPairs);
+ this->allRComponents = RhdpdaUtils::generateAllPossibleRComponents(this->allStateSymbolPairs);
+
+ Utils::copyInputAlphabet(*this->rhdpda, *this->rdpda);
+ this->divideTransitions();
+}
+
+
+RhdpdaDeterminizer3::RhdpdaDeterminizer3(PDA* rhdpda)
+{
+ this->rhdpda = rhdpda;
+}
+
+
+Automaton* RhdpdaDeterminizer3::determinize()
+{
+ const Symbol& BOTTOM_OF_STACK_SYMBOL = RhdpdaUtils::BOTTOM_OF_STACK_SYMBOL;
+
+ this->rdpda = new PDA();
+ this->initDeterminization();
+
+ set<StateSymbolPair> initialPairs = this->combineStatesWithSymbol(this->rhdpda->getInitialStates(), BOTTOM_OF_STACK_SYMBOL);
+ const SComponent& initialS = this->getSComponentWithPairsIdentity(initialPairs);
+ const RComponent& initialR(initialPairs);
+ const State& initialState = this->getOrCreateState(initialS, initialR);
+ this->rdpda->addInitialState(initialState);
+
+ while (true) {
+ StateData* unmarkedStateData = RhdpdaUtils::getUnmarkedState(this->states);
+ if (unmarkedStateData == NULL) {
+ break;
+ }
+
+ // Internal
+ for (const auto& a : this->rhdpda->getInputAlphabet()) {
+ SComponent sPrimed;
+ SComponent& s = unmarkedStateData->s;
+ for (const auto& pairOfPairs : s.pairsOfPairs) {
+ const StateSymbolPair& x = pairOfPairs.pair1;
+ const State& r = pairOfPairs.pair2.state;
+ const Symbol& Y = pairOfPairs.pair2.symbol;
+ for (const auto& transition : this->internalTransitions) {
+ if (transition.getFrom() == r && transition.getInput() == a) {
+ const State& q = transition.getTo();
+ sPrimed.pairsOfPairs.insert(PairOfPairs(x, StateSymbolPair(q, Y)));
+ }
+ }
+ }
+ RComponent rPrimed;
+ RComponent& r = unmarkedStateData->r;
+ for (const auto& pair : r.pairs) {
+ const State& p = pair.state;
+ const Symbol& Y = pair.symbol;
+ for (const auto& transition : this->internalTransitions) {
+ if (transition.getFrom() == p && transition.getInput() == a) {
+ 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 = this->getOrCreateState(sPrimed, rPrimed);
+ const TransitionPDA transition(fromState, a, toState);
+ this->rdpda->addTransition(transition);
+ }
+ }
+
+ // Push
+ for (const auto& a : this->rhdpda->getInputAlphabet()) {
+ RComponent rDoublePrimed;
+ RComponent& r = unmarkedStateData->r;
+ for (const auto& pair : r.pairs) {
+ const State& p = pair.state;
+ for (const auto& transition : this->pushTransitions) {
+ if (transition.getFrom() == p && transition.getInput() == a) {
+ const State& q = transition.getTo();
+ const Symbol& Z = transition.getPush().front();
+ rDoublePrimed.pairs.insert(StateSymbolPair(q, Z));
+ }
+ }
+ }
+ SComponent sDoublePrimed = this->getSComponentWithPairsIdentity(rDoublePrimed.pairs);
+ SComponent& s = unmarkedStateData->s;
+ if (rDoublePrimed.pairs.size() > 0) {
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
+ string stackSymbolName = this->buildStackSymbolName(s, r, a);
+ list<Symbol> pop = {};
+ list<Symbol> push = {Symbol(stackSymbolName)};
+ const TransitionPDA transition(fromState, a, toState, pop, push);
+ this->rdpda->addTransition(transition);
+ }
+ }
+
+ // Pop
+ for (const auto& a : this->rhdpda->getInputAlphabet()) {
+ for (const auto& b : this->rhdpda->getInputAlphabet()) {
+ SComponent& s = unmarkedStateData->s;
+
+ set<PairOfPairs> update;
+ for (const auto& pairOfPairs : s.pairsOfPairs) {
+ const State& r = pairOfPairs.pair1.state;
+ const Symbol& Z = pairOfPairs.pair1.symbol;
+ const State& rPrimed = pairOfPairs.pair2.state;
+ if (pairOfPairs.pair2.symbol == Z) {
+ for (const auto& pushTransition : this->pushTransitions) {
+ for (const auto& popTransition : this->popTransitions) {
+ 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) {
+ StateSymbolPair pair1(p, Z);
+ StateSymbolPair pair2(q, Z);
+ update.insert(PairOfPairs(pair1, pair2));
+ }
+ }
+ }
+ }
+ }
+ if (update.size() == 0) {
+ continue;
+ }
+
+ for (const auto& sPrimed : this->allSComponents) {
+ for (const auto& rPrimed : this->allRComponents) {
+ RComponent rDoublePrimed;
+ for (const auto& updateItem : update) {
+ const State& p = updateItem.pair1.state;
+ const State& q = updateItem.pair2.state;
+ for (const auto& rPrimedPair : rPrimed.pairs) {
+ if (rPrimedPair.state == p) {
+ const Symbol& Y = rPrimedPair.symbol;
+ rDoublePrimed.pairs.insert(StateSymbolPair(q, Y));
+ }
+ }
+ }
+ SComponent sDoublePrimed;
+ for (const auto& updateItem : update) {
+ const State& p = updateItem.pair1.state;
+ const State& q = updateItem.pair2.state;
+ for (const auto& sPrimedPair : sPrimed.pairsOfPairs) {
+ if (sPrimedPair.pair2.state == p) {
+ const StateSymbolPair& x = sPrimedPair.pair1;
+ const Symbol& Y = sPrimedPair.pair2.symbol;
+ sDoublePrimed.pairsOfPairs.insert(PairOfPairs(x, StateSymbolPair(q, Y)));
+ }
+ }
+ }
+ if (sDoublePrimed.pairsOfPairs.size() > 0 && rDoublePrimed.pairs.size() > 0) {
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
+ string stackSymbolName = this->buildStackSymbolName(sPrimed, rPrimed, a);
+ list<Symbol> pop = {Symbol(stackSymbolName)};
+ list<Symbol> push = {};
+ const TransitionPDA transition(fromState, b, toState, pop, push);
+ this->rdpda->addTransition(transition);
+ }
+ }
+ }
+ }
+ }
+ }
+
+ const set<State>& rhdpdaFinalStates = this->rhdpda->getFinalStates();
+ for (const auto& state : this->states) {
+ bool isFinalState = false;
+ const RComponent& r = state.second.r;
+ for (const auto& pair : r.pairs) {
+ if (rhdpdaFinalStates.find(pair.state) != rhdpdaFinalStates.end()) {
+ isFinalState = true;
+ }
+ }
+ if (isFinalState) {
+ this->rdpda->addFinalState(state.second.state);
+ }
+ }
+
+ return this->rdpda;
+}
+
+
+}
+}
diff --git a/adeterminize/src/rhdpda/RhdpdaDeterminizer3.h b/adeterminize/src/rhdpda/RhdpdaDeterminizer3.h
new file mode 100644
index 0000000000..c111621be2
--- /dev/null
+++ b/adeterminize/src/rhdpda/RhdpdaDeterminizer3.h
@@ -0,0 +1,131 @@
+#ifndef RHDPDADETERMINZER3_H_
+#define RHDPDADETERMINZER3_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 "../common/Utils.h"
+#include "../Determinizer.h"
+#include "RhdpdaUtils.h"
+#include "RhdpdaStructs.h"
+
+using namespace std;
+using namespace automaton;
+using namespace alphabet;
+using namespace determinization;
+
+namespace determinization {
+namespace rhdpda {
+
+/**
+ * Class for running second version of determinization algorithm on rhdpda.
+ */
+class RhdpdaDeterminizer3 : public Determinizer
+{
+
+ private:
+
+ /** Real-time height-deterministic pushdown automaton */
+ PDA* rhdpda;
+
+ /** Real-time deterministic pushdown automaton */
+ PDA* rdpda;
+
+ /** Map of states of deterministic pda, where key is the name of state and value is data about this state */
+ map<string, StateData> states;
+
+ /** Set of internal transitions from rhdpda */
+ set<TransitionPDA> internalTransitions;
+
+ /** Set of push transitions from rhdpda */
+ set<TransitionPDA> pushTransitions;
+
+ /** Set of pop transitions from rhdpda */
+ set<TransitionPDA> popTransitions;
+
+ /** Set of all possible pairs of states and stack symbols */
+ set<StateSymbolPair> allStateSymbolPairs;
+
+ /** Vector with all possible S components of deterministic pda */
+ vector<SComponent> allSComponents;
+
+ /** Vector with all possible R components of deterministic pda */
+ vector<RComponent> allRComponents;
+
+ /**
+ * Divides transitions of rhdpda into internal, push and pop transitions.
+ *
+ * @return void
+ */
+ void divideTransitions();
+
+ /**
+ * Returns name of stack symbol of deterministic pda which is created from given S and R component and input symbol.
+ * This method also ensures that this stack symbol is already added into deterministic pda.
+ *
+ * @param s S component of stack symbol
+ * @param r R component of stack symbol
+ * @param input input symbol
+ * @return name of stack symbol
+ */
+ string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input);
+
+ /**
+ * Returns state and symbol pairs that are created by combining state from given set of states and given symbol.
+ *
+ * @param states
+ * @param symbol
+ * @return state and symbol pairs that are created by combining given states and symbol
+ */
+ set<StateSymbolPair> combineStatesWithSymbol(const set<State>& states, const Symbol& symbol);
+
+ /**
+ * Returns S component that contains pairs where both elements are same. These pairs are created from given set
+ * of state and symbol pairs.
+ *
+ * @param pairs set of state and symbol pairs from which to create identity pairs
+ * @return pairs where both elements are same
+ */
+ const SComponent getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs);
+
+ /**
+ * Returns existing state from states map, if there is one with same name, or creates new one and adds it into
+ * states map and deterministic pda.
+ *
+ * @param s S component of state
+ * @param r R component of state
+ * @return state of deterministic pda
+ */
+ const State& getOrCreateState(const SComponent& s, const RComponent& r);
+
+ /**
+ * Runs some initializiation stuff before determinization algorithm.
+ */
+ void initDeterminization();
+
+ public:
+
+ /**
+ * @param rhdpda real-time height-deterministic pushdown automaton given for determinization
+ */
+ RhdpdaDeterminizer3(PDA* rhdpda);
+
+ /**
+ * Runs determinization algorithm on rhdpda given in constructor.
+ *
+ * @return real-time deterministic pushdown automaton
+ */
+ Automaton* determinize();
+
+};
+
+}
+}
+#endif
--
GitLab