From 1be54fa9b76abd439e1789f340ab5aeb5727c5e1 Mon Sep 17 00:00:00 2001
From: Jan Vesely <janvesely@janvesely.net>
Date: Thu, 24 Apr 2014 18:45:10 +0200
Subject: [PATCH] add rhdpda determinization with removed r-component
---
adeterminize/src/adeterminize.cpp | 7 +-
.../src/rhdpda/RhdpdaDeterminizer4.cpp | 237 ++++++++++++++++++
adeterminize/src/rhdpda/RhdpdaDeterminizer4.h | 135 ++++++++++
adeterminize/src/rhdpda/RhdpdaStructs.h | 5 +
4 files changed, 382 insertions(+), 2 deletions(-)
create mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer4.cpp
create mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer4.h
diff --git a/adeterminize/src/adeterminize.cpp b/adeterminize/src/adeterminize.cpp
index 6fc8bff09d..890e48526d 100644
--- a/adeterminize/src/adeterminize.cpp
+++ b/adeterminize/src/adeterminize.cpp
@@ -18,6 +18,7 @@
#include "rhdpda/RhdpdaDeterminizer.h"
#include "rhdpda/RhdpdaDeterminizer2.h"
#include "rhdpda/RhdpdaDeterminizer3.h"
+#include "rhdpda/RhdpdaDeterminizer4.h"
using namespace std;
using namespace automaton;
@@ -33,7 +34,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 also 3 versions (use numbers 1, 2 and 3). 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 4 versions (use numbers 1, 2, 3 and 4). Default value is always number 1." << endl;
cout << " -h, --help \t Displays this help message." << endl;
cout << endl;
}
@@ -50,7 +51,9 @@ Determinizer* getVpaDeterminizer(Automaton* automaton, string version) {
Determinizer* getRhdpdaDeterminizer(Automaton* automaton, string version) {
- if (version == "3") {
+ if (version == "4") {
+ return new rhdpda::RhdpdaDeterminizer4((PDA*) automaton);
+ } else if (version == "3") {
return new rhdpda::RhdpdaDeterminizer3((PDA*) automaton);
} else if (version == "2") {
return new rhdpda::RhdpdaDeterminizer2((PDA*) automaton);
diff --git a/adeterminize/src/rhdpda/RhdpdaDeterminizer4.cpp b/adeterminize/src/rhdpda/RhdpdaDeterminizer4.cpp
new file mode 100644
index 0000000000..a14f23b5b4
--- /dev/null
+++ b/adeterminize/src/rhdpda/RhdpdaDeterminizer4.cpp
@@ -0,0 +1,237 @@
+#include "RhdpdaDeterminizer4.h"
+
+namespace determinization {
+namespace rhdpda {
+
+
+void RhdpdaDeterminizer4::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 RhdpdaDeterminizer4::buildStateName(const SComponent& s)
+{
+ string name = "{";
+ for (const auto& pairOfPairs : s.pairsOfPairs) {
+ if (&pairOfPairs != &(*begin(s.pairsOfPairs))) {
+ name += ", ";
+ }
+ name += "(" + RhdpdaUtils::buildPairName(pairOfPairs.pair1) + ", " +
+ RhdpdaUtils::buildPairName(pairOfPairs.pair2) + ")";
+ }
+ return name + "}";
+}
+
+
+string RhdpdaDeterminizer4::buildStackSymbolName(const SComponent& s, const Symbol& input)
+{
+ string name = "(" + this->buildStateName(s) + ")";
+ name += ", " + input.getSymbol();
+ try {
+ this->rdpda->addStackSymbol(name);
+ } catch (AutomatonException e) {
+ /* Stack symbol already exists */
+ }
+ return name;
+}
+
+
+set<StateSymbolPair> RhdpdaDeterminizer4::combineStatesWithSymbol(const set<State>& states, const Symbol& symbol)
+{
+ return RhdpdaUtils::combineStatesWithSymbol(states, symbol);
+}
+
+
+const SComponent RhdpdaDeterminizer4::getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs)
+{
+ return RhdpdaUtils::getSComponentWithPairsIdentity(pairs);
+}
+
+
+const State& RhdpdaDeterminizer4::getOrCreateState(const SComponent& s)
+{
+ string stateName = this->buildStateName(s);
+ 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);
+ StateData& insertedData = this->states.insert(pair<string, StateData>(stateName, stateData)).first->second;
+ this->rdpda->addState(state);
+ return insertedData.state;
+}
+
+
+void RhdpdaDeterminizer4::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);
+
+ Utils::copyInputAlphabet(*this->rhdpda, *this->rdpda);
+ this->divideTransitions();
+}
+
+
+RhdpdaDeterminizer4::RhdpdaDeterminizer4(PDA* rhdpda)
+{
+ this->rhdpda = rhdpda;
+}
+
+
+Automaton* RhdpdaDeterminizer4::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 State& initialState = this->getOrCreateState(initialS);
+ 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)));
+ }
+ }
+ }
+ if (sPrimed.pairsOfPairs.size() > 0) {
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = this->getOrCreateState(sPrimed);
+ const TransitionPDA transition(fromState, a, toState);
+ this->rdpda->addTransition(transition);
+ }
+ }
+
+ // Push
+ for (const auto& a : this->rhdpda->getInputAlphabet()) {
+ RComponent rDoublePrimed;
+ SComponent& s = unmarkedStateData->s;
+ for (const auto& pairOfPairs : s.pairsOfPairs) {
+ const State& p = pairOfPairs.pair2.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));
+ }
+ }
+ }
+ if (rDoublePrimed.pairs.size() > 0) {
+ const State& fromState = unmarkedStateData->state;
+ SComponent sDoublePrimed = this->getSComponentWithPairsIdentity(rDoublePrimed.pairs);
+ const State& toState = this->getOrCreateState(sDoublePrimed);
+ string stackSymbolName = this->buildStackSymbolName(s, 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) {
+ 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) {
+ const State& fromState = unmarkedStateData->state;
+ const State& toState = this->getOrCreateState(sDoublePrimed);
+ string stackSymbolName = this->buildStackSymbolName(sPrimed, 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 SComponent& s = state.second.s;
+ for (const auto& pairOfPairs : s.pairsOfPairs) {
+ if (rhdpdaFinalStates.find(pairOfPairs.pair2.state) != rhdpdaFinalStates.end()) {
+ isFinalState = true;
+ }
+ }
+ if (isFinalState) {
+ this->rdpda->addFinalState(state.second.state);
+ }
+ }
+
+ return this->rdpda;
+}
+
+
+}
+}
diff --git a/adeterminize/src/rhdpda/RhdpdaDeterminizer4.h b/adeterminize/src/rhdpda/RhdpdaDeterminizer4.h
new file mode 100644
index 0000000000..1df0da7bb4
--- /dev/null
+++ b/adeterminize/src/rhdpda/RhdpdaDeterminizer4.h
@@ -0,0 +1,135 @@
+#ifndef RHDPDADETERMINZER4_H_
+#define RHDPDADETERMINZER4_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 fourth version of determinization algorithm on rhdpda.
+ */
+class RhdpdaDeterminizer4 : 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;
+
+ /**
+ * Divides transitions of rhdpda into internal, push and pop transitions.
+ *
+ * @return void
+ */
+ void divideTransitions();
+
+ /**
+ * Returns name of state of deterministic pda which is created from given S.
+ *
+ * @param s S component of state
+ * @return name of state
+ */
+ string buildStateName(const SComponent& s);
+
+ /**
+ * 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 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
+ * @return state of deterministic pda
+ */
+ const State& getOrCreateState(const SComponent& s);
+
+ /**
+ * Runs some initializiation stuff before determinization algorithm.
+ */
+ void initDeterminization();
+
+ public:
+
+ /**
+ * @param rhdpda real-time height-deterministic pushdown automaton given for determinization
+ */
+ RhdpdaDeterminizer4(PDA* rhdpda);
+
+ /**
+ * Runs determinization algorithm on rhdpda given in constructor.
+ *
+ * @return real-time deterministic pushdown automaton
+ */
+ Automaton* determinize();
+
+};
+
+}
+}
+#endif
diff --git a/adeterminize/src/rhdpda/RhdpdaStructs.h b/adeterminize/src/rhdpda/RhdpdaStructs.h
index 238ff5ea96..2db3c2b746 100644
--- a/adeterminize/src/rhdpda/RhdpdaStructs.h
+++ b/adeterminize/src/rhdpda/RhdpdaStructs.h
@@ -114,6 +114,11 @@ struct StateData
s(s),
r(r),
isMarked(false) {}
+
+ StateData(const State& state, const SComponent& s)
+ : state(state),
+ s(s),
+ isMarked(false) {}
};
--
GitLab