From 656ba0f0d51075dfa55ea90e7bef6380865ac780 Mon Sep 17 00:00:00 2001
From: Jan Travnicek <Jan.Travnicek@fit.cvut.cz>
Date: Sun, 28 Sep 2014 20:53:02 +0200
Subject: [PATCH] add RHDPDA determinisation
---
adeterminize2/src/adeterminize.cpp | 6 +-
.../src/determinize/common/RHDPDACommon.cpp | 223 ++++++++++++++++
.../src/determinize/common/RHDPDACommon.h | 43 +++
.../determinize/hdpda/HDPDADeterminizer.cpp | 244 ++++++++++++++++++
.../src/determinize/hdpda/HDPDADeterminizer.h | 24 ++
.../src/determinize/vpa/VPADeterminizer.cpp | 171 ++----------
.../src/determinize/vpa/VPADeterminizer.h | 7 -
7 files changed, 553 insertions(+), 165 deletions(-)
create mode 100644 alib2algo/src/determinize/common/RHDPDACommon.cpp
create mode 100644 alib2algo/src/determinize/common/RHDPDACommon.h
create mode 100644 alib2algo/src/determinize/hdpda/HDPDADeterminizer.cpp
create mode 100644 alib2algo/src/determinize/hdpda/HDPDADeterminizer.h
diff --git a/adeterminize2/src/adeterminize.cpp b/adeterminize2/src/adeterminize.cpp
index 126f52b603..d557456be8 100644
--- a/adeterminize2/src/adeterminize.cpp
+++ b/adeterminize2/src/adeterminize.cpp
@@ -13,6 +13,7 @@
#include "determinize/nfa/NFADeterminizer.h"
#include "determinize/idpda/IDPDADeterminizer.h"
#include "determinize/vpa/VPADeterminizer.h"
+#include "determinize/hdpda/HDPDADeterminizer.h"
#include "automaton/PDAToRHPDA.h"
#include "automaton/RHPDAToPDA.h"
@@ -116,8 +117,9 @@ int main(int argc, char** argv) {
} else if (type == TYPE_RHDPDA) {
automaton::NPDA npda = alib::DataFactory::fromTokens<automaton::NPDA>(tokens);
automaton::RealTimeHeightDeterministicNPDA rhpda = automaton::PDAToRHPDA::convert(npda);
- automaton::NPDA npda2 = automaton::RHPDAToPDA::convert(rhpda);
- alib::DataFactory::toStdout(npda2);
+ automaton::RealTimeHeightDeterministicNPDA dpda = determinize::HDPDADeterminizer::determinize(rhpda);
+ automaton::NPDA dpda2 = automaton::RHPDAToPDA::convert(dpda);
+ alib::DataFactory::toStdout(dpda2);
return 0;
}
diff --git a/alib2algo/src/determinize/common/RHDPDACommon.cpp b/alib2algo/src/determinize/common/RHDPDACommon.cpp
new file mode 100644
index 0000000000..00dbd3b3c0
--- /dev/null
+++ b/alib2algo/src/determinize/common/RHDPDACommon.cpp
@@ -0,0 +1,223 @@
+#include "RHDPDACommon.h"
+#include "label/LabelPairLabel.h"
+#include "label/LabelSetLabel.h"
+#include "label/ObjectLabel.h"
+#include "object/Object.h"
+#include "alphabet/LabeledSymbol.h"
+
+#include "automaton/PDA/VisiblyPushdownNPDA.h"
+#include "automaton/PDA/RealTimeHeightDeterministicNPDA.h"
+
+namespace determinize {
+
+label::Label packToStateLabel(std::set<std::pair<label::Label, label::Label>>&& data) {
+ std::set<label::Label> res;
+ for(auto&& subData : std::move(data)) {
+ res.insert(label::Label(label::LabelPairLabel(std::move(subData))));
+ }
+ return label::Label(label::LabelSetLabel(std::move(res)));
+}
+
+std::set<std::pair<label::Label, label::Label>> unpackFromStateLabel(const label::Label& data) {
+ std::set<std::pair<label::Label, label::Label>> res;
+ const std::set<label::Label>& labelSet = static_cast<const label::LabelSetLabel&>(data.getData()).getData();
+ for (const auto& subData : labelSet) {
+ const std::pair<label::Label, label::Label>& labelPair = static_cast<const label::LabelPairLabel&>(subData.getData()).getData();
+ res.insert(labelPair);
+ }
+ return res;
+}
+
+label::Label packToStackSymbolLabel(std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol>&& data) {
+ label::Label res1 = packToStateLabel(std::move(data.first));
+ label::Label res2 = label::Label(label::ObjectLabel(alib::Object(std::move(data.second.getData()))));
+ return label::Label(label::LabelPairLabel(std::make_pair(std::move(res1), std::move(res2))));
+}
+
+std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol> unpackFromDVPAStackSymbolLabel(const label::Label& data) {
+ const label::Label& labelPairFirst = static_cast<const label::LabelPairLabel&>(data.getData()).getData().first;
+ std::set<std::pair<label::Label, label::Label>> res = unpackFromStateLabel(labelPairFirst);
+
+ const label::Label& labelPairSecond = static_cast<const label::LabelPairLabel&>(data.getData()).getData().second;
+ const alib::Object& object = static_cast<const label::ObjectLabel&>(labelPairSecond.getData()).getData();
+ return std::make_pair(std::move(res), alphabet::Symbol(static_cast<const alphabet::SymbolBase&>(object.getData())));
+}
+
+label::Label packToStackSymbolLabel(std::pair<std::set<std::pair<label::Label, label::Label>>, std::variant<string::Epsilon, alphabet::Symbol>>&& data) {
+ label::Label res1 = packToStateLabel(std::move(data.first));
+ if(data.second.is<string::Epsilon>()) {
+ label::Label res2 = label::Label(label::ObjectLabel(alib::Object(std::move(data.second.get<string::Epsilon>()))));
+ return label::Label(label::LabelPairLabel(std::make_pair(std::move(res1), std::move(res2))));
+ } else {
+ label::Label res2 = label::Label(label::ObjectLabel(alib::Object(std::move(data.second.get<alphabet::Symbol>().getData()))));
+ return label::Label(label::LabelPairLabel(std::make_pair(std::move(res1), std::move(res2))));
+ }
+}
+
+std::pair<std::set<std::pair<label::Label, label::Label>>, std::variant<string::Epsilon, alphabet::Symbol>> unpackFromDRHDPDAStackSymbolLabel(const label::Label& data) {
+ const label::Label& labelPairFirst = static_cast<const label::LabelPairLabel&>(data.getData()).getData().first;
+ std::set<std::pair<label::Label, label::Label>> res = unpackFromStateLabel(labelPairFirst);
+
+ const label::Label& labelPairSecond = static_cast<const label::LabelPairLabel&>(data.getData()).getData().second;
+ const alib::Object& object = static_cast<const label::ObjectLabel&>(labelPairSecond.getData()).getData();
+ if(object.getData() == string::Epsilon::EPSILON) {
+ return std::make_pair(std::move(res), std::variant<string::Epsilon, alphabet::Symbol>(static_cast<const string::Epsilon&>(object.getData())));
+ } else {
+ return std::make_pair(std::move(res), std::variant<string::Epsilon, alphabet::Symbol>(alphabet::Symbol(static_cast<const alphabet::SymbolBase&>(object.getData()))));
+ }
+}
+
+std::set<label::Label> retrieveDSubSet(const std::set<std::pair<label::Label, label::Label>>& localOperation) {
+ std::set<label::Label> id;
+ for(const auto& entry : localOperation) {
+ id.insert(entry.second);
+ }
+ return id;
+}
+
+std::set<std::pair<label::Label, label::Label>> createIdentity(std::set<label::Label>&& states) {
+ std::set<std::pair<label::Label, label::Label>> id;
+ for(const label::Label& state : states) {
+ id.insert(std::make_pair(state, state));
+ }
+ return id;
+}
+
+template<class T>
+const automaton::State* existsDirtyState(const T& d, const T& n) {
+ for(const automaton::State& state : d.getStates()) {
+ const label::Label& stateLabel = state.getName();
+ const std::set<label::Label> dSubSet = retrieveDSubSet(unpackFromStateLabel(stateLabel));
+
+ bool originalCallsLocals = false;
+ for(const auto& transition : n.getCallTransitions()) {
+ if(dSubSet.count(transition.first.first.getName())) {
+ originalCallsLocals = true;
+ break;
+ }
+ }
+ for(const auto& transition : n.getLocalTransitions()) {
+ if(dSubSet.count(transition.first.first.getName())) {
+ originalCallsLocals = true;
+ break;
+ }
+ }
+
+ if(!originalCallsLocals) continue;
+
+ for(const auto& transition : d.getCallTransitions()) {
+ if(stateLabel != transition.first.first.getName()) continue;
+
+ goto continue2;
+ }
+ for(const auto& transition : d.getLocalTransitions()) {
+ if(stateLabel != transition.first.first.getName()) continue;
+
+ goto continue2;
+ }
+ return &state;
+
+continue2: while(false); //TODO remove this
+ }
+ return NULL;
+}
+
+template const automaton::State* existsDirtyState(const automaton::VisiblyPushdownNPDA& d, const automaton::VisiblyPushdownNPDA& n);
+template const automaton::State* existsDirtyState(const automaton::RealTimeHeightDeterministicNPDA& d, const automaton::RealTimeHeightDeterministicNPDA& n);
+
+template<class T>
+void localClosure(std::set<label::Label>& states, const std::set<label::Label>& oldStates, const T& d) {
+ std::set<label::Label> newStates;
+
+ for(const label::Label& state : oldStates) {
+ for(const auto& transition : d.getLocalTransitions()) {
+ if(transition.second.begin()->getName() != state) continue;
+
+ if(!states.count(transition.first.first.getName())) {
+ states.insert(transition.first.first.getName());
+ newStates.insert(transition.first.first.getName());
+ }
+ }
+
+ for(const auto& transition : d.getReturnTransitions()) {
+ if(transition.second.begin()->getName() != state) continue;
+
+ const alphabet::Symbol& popSymbol = std::get<2>(transition.first);
+ if(popSymbol == d.getBottomOfTheStackSymbol()) continue;
+ const label::Label& popSymbolLabel = static_cast<const alphabet::LabeledSymbol&>(popSymbol.getData()).getLabel();
+ const label::Label& statePart = static_cast<const label::LabelPairLabel&>(popSymbolLabel.getData()).getData().first;
+
+ if(!states.count(statePart)) {
+ states.insert(statePart);
+ newStates.insert(statePart);
+ }
+ }
+ }
+
+ if(newStates.empty()) return;
+ localClosure(states, newStates, d);
+}
+
+template void localClosure(std::set<label::Label>& states, const std::set<label::Label>& oldStates, const automaton::VisiblyPushdownNPDA& d);
+template void localClosure(std::set<label::Label>& states, const std::set<label::Label>& oldStates, const automaton::RealTimeHeightDeterministicNPDA& d);
+
+template<class T>
+std::pair<automaton::State, alphabet::Symbol>* existsDirtyStateSymbol(const T& d, const T& n) {
+ for(const automaton::State& state : d.getStates()) {
+ const label::Label& stateLabel = state.getName();
+
+ std::set<label::Label> lc { stateLabel };
+ localClosure(lc, std::set<label::Label>{stateLabel}, d); //intentional copy
+
+ bool originalPops = false;
+ for(const label::Label& localState : lc) {
+ const std::set<label::Label> dSubSet = retrieveDSubSet(unpackFromStateLabel(localState));
+
+ for(const auto& transition : n.getReturnTransitions()) {
+ if(dSubSet.count(std::get<0>(transition.first).getName())) {
+ originalPops = true;
+ goto break2;
+ }
+ }
+ }
+break2: while(false);
+ if(!originalPops) continue;
+
+ std::set<alphabet::Symbol> topSymbols;
+ for(const label::Label& localState : lc) {
+ for(const auto& transition : d.getCallTransitions()) {
+ for(const auto& to : transition.second) {
+ if(localState != to.first.getName()) continue;
+
+ topSymbols.insert(to.second);
+ }
+ }
+
+ if(d.getInitialStates().begin()->getName() == localState) {
+ topSymbols.insert(d.getBottomOfTheStackSymbol());
+ }
+ }
+
+ for(const auto& transition : d.getReturnTransitions()) {
+ if(stateLabel != std::get<0>(transition.first).getName()) continue;
+
+ topSymbols.erase(std::get<2>(transition.first));
+ }
+
+ if(!topSymbols.empty()) return new std::pair<automaton::State, alphabet::Symbol>(automaton::State(stateLabel), *topSymbols.begin());
+ }
+ return NULL;
+}
+
+template std::pair<automaton::State, alphabet::Symbol>* existsDirtyStateSymbol(const automaton::VisiblyPushdownNPDA& d, const automaton::VisiblyPushdownNPDA& n);
+template std::pair<automaton::State, alphabet::Symbol>* existsDirtyStateSymbol(const automaton::RealTimeHeightDeterministicNPDA& d, const automaton::RealTimeHeightDeterministicNPDA& n);
+
+std::set<label::Label> retrieveLabels(const std::set<automaton::State>& states) {
+ std::set<label::Label> labels;
+ for(const automaton::State& state : states) {
+ labels.insert(state.getName());
+ }
+ return labels;
+}
+
+} /* namespace determinize */
diff --git a/alib2algo/src/determinize/common/RHDPDACommon.h b/alib2algo/src/determinize/common/RHDPDACommon.h
new file mode 100644
index 0000000000..765306ab46
--- /dev/null
+++ b/alib2algo/src/determinize/common/RHDPDACommon.h
@@ -0,0 +1,43 @@
+#ifndef RHDPDA_VPA_COMMON_H_
+#define RHDPDA_VPA_COMMON_H_
+
+#include "label/Label.h"
+#include "automaton/common/State.h"
+#include "alphabet/Symbol.h"
+#include "string/Epsilon.h"
+#include "std/variant.hpp"
+#include <set>
+#include <map>
+
+namespace determinize {
+
+label::Label packToStateLabel(std::set<std::pair<label::Label, label::Label>>&& data);
+
+std::set<std::pair<label::Label, label::Label>> unpackFromStateLabel(const label::Label& data);
+
+label::Label packToStackSymbolLabel(std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol>&& data);
+
+std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol> unpackFromDVPAStackSymbolLabel(const label::Label& data);
+
+label::Label packToStackSymbolLabel(std::pair<std::set<std::pair<label::Label, label::Label>>, std::variant<string::Epsilon, alphabet::Symbol>>&& data);
+
+std::pair<std::set<std::pair<label::Label, label::Label>>, std::variant<string::Epsilon, alphabet::Symbol>> unpackFromDRHDPDAStackSymbolLabel(const label::Label& data);
+
+std::set<label::Label> retrieveDSubSet(const std::set<std::pair<label::Label, label::Label>>& localOperation);
+
+std::set<std::pair<label::Label, label::Label>> createIdentity(std::set<label::Label>&& states);
+
+template<class T>
+const automaton::State* existsDirtyState(const T& d, const T& n);
+
+template<class T>
+void localClosure(std::set<label::Label>& states, const std::set<label::Label>& oldStates, const T& d);
+
+template<class T>
+std::pair<automaton::State, alphabet::Symbol>* existsDirtyStateSymbol(const T& d, const T& n);
+
+std::set<label::Label> retrieveLabels(const std::set<automaton::State>& states);
+
+} /* namespace determinize */
+
+#endif /* RHDPDA_VPA_COMMON_H_ */
diff --git a/alib2algo/src/determinize/hdpda/HDPDADeterminizer.cpp b/alib2algo/src/determinize/hdpda/HDPDADeterminizer.cpp
new file mode 100644
index 0000000000..cde68385e7
--- /dev/null
+++ b/alib2algo/src/determinize/hdpda/HDPDADeterminizer.cpp
@@ -0,0 +1,244 @@
+#include "HDPDADeterminizer.h"
+#include "../common/RHDPDACommon.h"
+
+#include "automaton/common/State.h"
+#include "alphabet/Symbol.h"
+#include "alphabet/LabeledSymbol.h"
+#include "label/Label.h"
+#include "exception/AlibException.h"
+#include <std/set.hpp>
+#include <iostream>
+
+namespace determinize {
+
+void addRetTransition(const automaton::State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const alphabet::Symbol& dvpdaSymbol, const automaton::State& to, automaton::RealTimeHeightDeterministicNPDA& deterministic) {
+ deterministic.addState(from);
+ deterministic.addState(to);
+ deterministic.addStackSymbol(dvpdaSymbol);
+
+ deterministic.addReturnTransition(from, input, dvpdaSymbol, to);
+}
+
+void retInitial(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicNPDA& deterministic) {
+ std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
+
+ std::set<std::pair<label::Label, label::Label>> S1;
+ for(const auto& entry : S) {
+ const label::Label& q = entry.first;
+ const label::Label& q2 = entry.second;
+
+ for(const auto& transition : nondeterministic.getReturnTransitions()) {
+ if(q2 != std::get<0>(transition.first).getName()) continue;
+ if(input != std::get<1>(transition.first)) continue;
+ if(nondeterministic.getBottomOfTheStackSymbol() != std::get<2>(transition.first)) continue;
+
+ for(const auto& to : transition.second) {
+ const label::Label& q1 = to.getName();
+ S1.insert(std::make_pair(q, q1));
+ }
+ }
+ }
+
+ addRetTransition(state, input, pdaSymbol, automaton::State(packToStateLabel(std::move(S1))), deterministic);
+}
+
+void ret(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicNPDA& deterministic) {
+ std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
+ std::pair<std::set<std::pair<label::Label, label::Label>>, std::variant<string::Epsilon, alphabet::Symbol>> pdaSymbolUnpack = unpackFromDRHDPDAStackSymbolLabel(static_cast<const alphabet::LabeledSymbol&>(pdaSymbol.getData()).getLabel());
+ const std::set<std::pair<label::Label, label::Label>>& S1 = pdaSymbolUnpack.first;
+
+ std::set<std::pair<label::Label, label::Label>> update;
+
+ for(const auto& transition : nondeterministic.getCallTransitions()) {
+ if(pdaSymbolUnpack.second != std::get<1>(transition.first)) continue;
+
+ const label::Label& q = std::get<0>(transition.first).getName();
+ for(const auto& to : transition.second) {
+ const label::Label q1 = to.first.getName();
+ const alphabet::Symbol& gamma = to.second;
+
+ for(const auto& entry : S) {
+ if(q1 != entry.first) continue;
+ const label::Label& q2 = entry.second;
+
+ for(const auto& transition2 : nondeterministic.getReturnTransitions()) {
+ if(q2 != std::get<0>(transition2.first).getName()) continue;
+ if(input != std::get<1>(transition2.first)) continue;
+ if(gamma != std::get<2>(transition2.first)) continue;
+
+ for(const auto& to2 : transition2.second) {
+ const label::Label& qI = to2.getName();
+
+ update.insert(std::make_pair(q, qI));
+ }
+ }
+ }
+ }
+ }
+
+ std::set<std::pair<label::Label, label::Label>> S2;
+ for(const auto& entry : S1) {
+ const label::Label& q = entry.first;
+ const label::Label& q3 = entry.second;
+ for(const auto& entry2 : update) {
+ if(q3 != entry2.first) continue;
+
+ const label::Label& qI = entry2.second;
+
+ S2.insert(std::make_pair(q, qI));
+ }
+ }
+
+ addRetTransition(state, input, pdaSymbol, automaton::State(packToStateLabel(std::move(S2))), deterministic);
+}
+
+void addCallTransition(const automaton::State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::State& to, const alphabet::Symbol& dvpdaSymbol, automaton::RealTimeHeightDeterministicNPDA& deterministic) {
+ deterministic.addState(from);
+ deterministic.addState(to);
+ deterministic.addStackSymbol(dvpdaSymbol);
+
+ deterministic.addCallTransition(from, input, to, dvpdaSymbol);
+}
+
+void call(const automaton::State& state, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicNPDA& deterministic) {
+ std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
+
+ std::set<label::Label> R = retrieveDSubSet(S);
+ std::set<label::Label> R1;
+
+ for(const label::Label& q : R) {
+ for(const auto& transition : nondeterministic.getCallTransitions()) {
+ if(q != transition.first.first.getName()) continue;
+ if(input != transition.first.second) continue;
+
+ for(const auto& to : transition.second) {
+ const label::Label& q1 = to.first.getName();
+
+ R1.insert(q1);
+ }
+ }
+ }
+
+ addCallTransition(state, input, automaton::State(packToStateLabel(createIdentity(std::move(R1)))), alphabet::Symbol(alphabet::LabeledSymbol(packToStackSymbolLabel(std::make_pair(std::move(S), input)))), deterministic);
+}
+
+void addLocalTransition(const automaton::State& from, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::State& to, automaton::RealTimeHeightDeterministicNPDA& deterministic) {
+ deterministic.addState(from);
+ deterministic.addState(to);
+
+ deterministic.addLocalTransition(from, input, to);
+}
+
+void local(const automaton::State& state, const std::variant<string::Epsilon, alphabet::Symbol>& input, const automaton::RealTimeHeightDeterministicNPDA& nondeterministic, automaton::RealTimeHeightDeterministicNPDA& deterministic) {
+ std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
+ std::set<std::pair<label::Label, label::Label>> S1;
+
+ for(const auto& entry : S) {
+ label::Label q = entry.first;
+ label::Label q2 = entry.second;
+ for(const auto& transition : nondeterministic.getLocalTransitions()) {
+ if(q2 != transition.first.first.getName()) continue;
+ if(input != transition.first.second) continue;
+
+ for(const auto& to : transition.second) {
+ label::Label q1 = to.getName();
+
+ S1.insert(std::make_pair(q, q1));
+ }
+ }
+ }
+
+ addLocalTransition(state, input, automaton::State(packToStateLabel(std::move(S1))), deterministic);
+}
+
+std::tuple<std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>> getLocalCallRetPartitioning(const automaton::RealTimeHeightDeterministicNPDA& n, const automaton::State& state) {
+ std::set<std::variant<string::Epsilon, alphabet::Symbol>> local;
+ std::set<std::variant<string::Epsilon, alphabet::Symbol>> call;
+ std::set<std::variant<string::Epsilon, alphabet::Symbol>> ret;
+
+ const std::set<label::Label> dSubSet = retrieveDSubSet(unpackFromStateLabel(state.getName()));
+
+ for(const auto& transition : n.getLocalTransitions()) {
+ if(dSubSet.count(transition.first.first.getName()))
+ local.insert(transition.first.second);
+ }
+
+ for(const auto& transition : n.getCallTransitions()) {
+ if(dSubSet.count(transition.first.first.getName()))
+ call.insert(transition.first.second);
+ }
+
+ for(const auto& transition : n.getReturnTransitions()) {
+ if(dSubSet.count(std::get<0>(transition.first).getName()))
+ ret.insert(std::get<1>(transition.first));
+ }
+
+ if(!std::empty_intersection(local, call))
+ throw exception::AlibException("Automaton is not real time height deterministic pushdown");
+
+ if(!std::empty_intersection(local, ret))
+ throw exception::AlibException("Automaton is not real time height deterministic pushdown");
+
+ if(!std::empty_intersection(call, ret))
+ throw exception::AlibException("Automaton is not real time height deterministic pushdown");
+
+ return std::make_tuple(local, call, ret);
+}
+
+automaton::RealTimeHeightDeterministicNPDA HDPDADeterminizer::determinize(const automaton::RealTimeHeightDeterministicNPDA& n) {
+ automaton::RealTimeHeightDeterministicNPDA d(n.getBottomOfTheStackSymbol());
+ d.setInputSymbols(n.getInputAlphabet());
+
+ label::Label initialLabel = packToStateLabel(createIdentity(retrieveLabels(n.getInitialStates())));
+ d.addState(automaton::State(initialLabel));
+ d.addInitialState(automaton::State(initialLabel));
+
+ for(;;) {
+ std::pair<automaton::State, alphabet::Symbol>* stateSymbol = existsDirtyStateSymbol(d, n);
+ const automaton::State* state = existsDirtyState(d, n);
+
+ if(stateSymbol == NULL && state == NULL) break;
+
+ if(stateSymbol != NULL) {
+ std::tuple<std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>> partitioning = getLocalCallRetPartitioning(n, stateSymbol->first);
+
+ std::set<std::variant<string::Epsilon, alphabet::Symbol>>& retPart = std::get<2>(partitioning);
+
+ for(const auto& symbol : retPart) {
+ if(stateSymbol->second == d.getBottomOfTheStackSymbol()) {
+ retInitial(stateSymbol->first, stateSymbol->second, symbol, n, d);
+ } else {
+ ret(stateSymbol->first, stateSymbol->second, symbol, n, d);
+ }
+ }
+ delete stateSymbol; //TODO remove this...
+ }
+
+ if(state != NULL) {
+ std::tuple<std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>, std::set<std::variant<string::Epsilon, alphabet::Symbol>>> partitioning = getLocalCallRetPartitioning(n, *state);
+
+ std::set<std::variant<string::Epsilon, alphabet::Symbol>>& localPart = std::get<0>(partitioning);
+ std::set<std::variant<string::Epsilon, alphabet::Symbol>>& callPart = std::get<1>(partitioning);
+
+ for(const auto& symbol : localPart) {
+ local(*state, symbol, n, d);
+ }
+ for(const auto& symbol : callPart) {
+ call(*state, symbol, n, d);
+ }
+ }
+ }
+
+ std::set<label::Label> finalLabels = retrieveLabels(n.getFinalStates());
+ for(const automaton::State& state : d.getStates()) {
+ const std::set<label::Label> labels = retrieveDSubSet(unpackFromStateLabel(state.getName()));
+
+ if(!std::empty_intersection(finalLabels, labels)) {
+ d.addFinalState(state);
+ }
+ }
+
+ return d;
+}
+
+}
diff --git a/alib2algo/src/determinize/hdpda/HDPDADeterminizer.h b/alib2algo/src/determinize/hdpda/HDPDADeterminizer.h
new file mode 100644
index 0000000000..97caaf125f
--- /dev/null
+++ b/alib2algo/src/determinize/hdpda/HDPDADeterminizer.h
@@ -0,0 +1,24 @@
+#ifndef HDPDA_DETERMINIZER_H_
+#define HDPDA_DETERMINIZER_H_
+
+#include "automaton/PDA/RealTimeHeightDeterministicNPDA.h"
+
+namespace determinize {
+
+/**
+ * Class for running basic determinization algorithm on vpa.
+ */
+class HDPDADeterminizer {
+public:
+ /**
+ * Runs determinization algorithm on nondeterministic vpa given in constructor.
+ *
+ * @return deterministic visibly pushdown automaton
+ */
+ static automaton::RealTimeHeightDeterministicNPDA determinize(const automaton::RealTimeHeightDeterministicNPDA& nondeterministic);
+
+};
+
+} /* namespace determinize */
+
+#endif /* HDPDA_DETERMINIZER_h_ */
diff --git a/alib2algo/src/determinize/vpa/VPADeterminizer.cpp b/alib2algo/src/determinize/vpa/VPADeterminizer.cpp
index 52a196b808..d36257bc41 100644
--- a/alib2algo/src/determinize/vpa/VPADeterminizer.cpp
+++ b/alib2algo/src/determinize/vpa/VPADeterminizer.cpp
@@ -1,51 +1,15 @@
#include "VPADeterminizer.h"
+#include "../common/RHDPDACommon.h"
#include "automaton/common/State.h"
#include "alphabet/Symbol.h"
#include "alphabet/LabeledSymbol.h"
#include "label/Label.h"
-#include "label/LabelSetLabel.h"
-#include "label/LabelPairLabel.h"
-#include "label/ObjectLabel.h"
-#include "object/Object.h"
#include <std/set.hpp>
#include <iostream>
namespace determinize {
-label::Label VPADeterminizer::packToDVPAStateLabel(std::set<std::pair<label::Label, label::Label>>&& data) {
- std::set<label::Label> res;
- for(auto&& subData : std::move(data)) {
- res.insert(label::Label(label::LabelPairLabel(std::move(subData))));
- }
- return label::Label(label::LabelSetLabel(std::move(res)));
-}
-
-std::set<std::pair<label::Label, label::Label>> VPADeterminizer::unpackFromDVPAStateLabel(const label::Label& data) {
- std::set<std::pair<label::Label, label::Label>> res;
- const std::set<label::Label>& labelSet = static_cast<const label::LabelSetLabel&>(data.getData()).getData();
- for (const auto& subData : labelSet) {
- const std::pair<label::Label, label::Label>& labelPair = static_cast<const label::LabelPairLabel&>(subData.getData()).getData();
- res.insert(labelPair);
- }
- return res;
-}
-
-label::Label VPADeterminizer::packToDVPAStackSymbolLabel(std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol>&& data) {
- label::Label res1 = packToDVPAStateLabel(std::move(data.first));
- label::Label res2 = label::Label(label::ObjectLabel(alib::Object(std::move(data.second.getData()))));
- return label::Label(label::LabelPairLabel(std::make_pair(std::move(res1), std::move(res2))));
-}
-
-std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol> VPADeterminizer::unpackFromDVPAStackSymbolLabel(const label::Label& data) {
- const label::Label& labelPairFirst = static_cast<const label::LabelPairLabel&>(data.getData()).getData().first;
- std::set<std::pair<label::Label, label::Label>> res = unpackFromDVPAStateLabel(labelPairFirst);
-
- const label::Label& labelPairSecond = static_cast<const label::LabelPairLabel&>(data.getData()).getData().second;
- const alib::Object& object = static_cast<const label::ObjectLabel&>(labelPairSecond.getData()).getData();
- return std::make_pair(std::move(res), alphabet::Symbol(static_cast<const alphabet::SymbolBase&>(object.getData())));
-}
-
void addRetTransition(const automaton::State& from, const alphabet::Symbol& input, const alphabet::Symbol& dvpdaSymbol, const automaton::State& to, automaton::VisiblyPushdownNPDA& deterministic) {
deterministic.addState(from);
deterministic.addState(to);
@@ -55,7 +19,7 @@ void addRetTransition(const automaton::State& from, const alphabet::Symbol& inpu
}
void retInitial(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const alphabet::Symbol& input, const automaton::VisiblyPushdownNPDA& nondeterministic, automaton::VisiblyPushdownNPDA& deterministic) {
- std::set<std::pair<label::Label, label::Label>> S = VPADeterminizer::unpackFromDVPAStateLabel(state.getName());
+ std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
std::set<std::pair<label::Label, label::Label>> S1;
for(const auto& entry : S) {
@@ -74,12 +38,12 @@ void retInitial(const automaton::State& state, const alphabet::Symbol& pdaSymbol
}
}
- addRetTransition(state, input, pdaSymbol, automaton::State(VPADeterminizer::packToDVPAStateLabel(std::move(S1))), deterministic);
+ addRetTransition(state, input, pdaSymbol, automaton::State(packToStateLabel(std::move(S1))), deterministic);
}
void ret(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const alphabet::Symbol& input, const automaton::VisiblyPushdownNPDA& nondeterministic, automaton::VisiblyPushdownNPDA& deterministic) {
- std::set<std::pair<label::Label, label::Label>> S = VPADeterminizer::unpackFromDVPAStateLabel(state.getName());
- std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol> pdaSymbolUnpack = VPADeterminizer::unpackFromDVPAStackSymbolLabel(static_cast<const alphabet::LabeledSymbol&>(pdaSymbol.getData()).getLabel());
+ std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
+ std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol> pdaSymbolUnpack = unpackFromDVPAStackSymbolLabel(static_cast<const alphabet::LabeledSymbol&>(pdaSymbol.getData()).getLabel());
const std::set<std::pair<label::Label, label::Label>>& S1 = pdaSymbolUnpack.first;
std::set<std::pair<label::Label, label::Label>> update;
@@ -124,7 +88,7 @@ void ret(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const
}
}
- addRetTransition(state, input, pdaSymbol, automaton::State(VPADeterminizer::packToDVPAStateLabel(std::move(S2))), deterministic);
+ addRetTransition(state, input, pdaSymbol, automaton::State(packToStateLabel(std::move(S2))), deterministic);
}
void addCallTransition(const automaton::State& from, const alphabet::Symbol& input, const automaton::State& to, const alphabet::Symbol& dvpdaSymbol, automaton::VisiblyPushdownNPDA& deterministic) {
@@ -135,24 +99,8 @@ void addCallTransition(const automaton::State& from, const alphabet::Symbol& inp
deterministic.addCallTransition(from, input, to, dvpdaSymbol);
}
-std::set<label::Label> retrieveDSubSet(const std::set<std::pair<label::Label, label::Label>>& localOperation) {
- std::set<label::Label> id;
- for(const auto& entry : localOperation) {
- id.insert(entry.second);
- }
- return id;
-}
-
-std::set<std::pair<label::Label, label::Label>> createIdentity(std::set<label::Label>&& states) {
- std::set<std::pair<label::Label, label::Label>> id;
- for(const label::Label& state : states) {
- id.insert(std::make_pair(state, state));
- }
- return id;
-}
-
void call(const automaton::State& state, const alphabet::Symbol& input, const automaton::VisiblyPushdownNPDA& nondeterministic, automaton::VisiblyPushdownNPDA& deterministic) {
- std::set<std::pair<label::Label, label::Label>> S = VPADeterminizer::unpackFromDVPAStateLabel(state.getName());
+ std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
std::set<label::Label> R = retrieveDSubSet(S);
std::set<label::Label> R1;
@@ -170,7 +118,7 @@ void call(const automaton::State& state, const alphabet::Symbol& input, const au
}
}
- addCallTransition(state, input, automaton::State(VPADeterminizer::packToDVPAStateLabel(createIdentity(std::move(R1)))), alphabet::Symbol(alphabet::LabeledSymbol(VPADeterminizer::packToDVPAStackSymbolLabel(std::make_pair(std::move(S), input)))), deterministic);
+ addCallTransition(state, input, automaton::State(packToStateLabel(createIdentity(std::move(R1)))), alphabet::Symbol(alphabet::LabeledSymbol(packToStackSymbolLabel(std::make_pair(std::move(S), input)))), deterministic);
}
void addLocalTransition(const automaton::State& from, const alphabet::Symbol& input, const automaton::State& to, automaton::VisiblyPushdownNPDA& deterministic) {
@@ -181,7 +129,7 @@ void addLocalTransition(const automaton::State& from, const alphabet::Symbol& in
}
void local(const automaton::State& state, const alphabet::Symbol& input, const automaton::VisiblyPushdownNPDA& nondeterministic, automaton::VisiblyPushdownNPDA& deterministic) {
- std::set<std::pair<label::Label, label::Label>> S = VPADeterminizer::unpackFromDVPAStateLabel(state.getName());
+ std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
std::set<std::pair<label::Label, label::Label>> S1;
for(const auto& entry : S) {
@@ -199,96 +147,7 @@ void local(const automaton::State& state, const alphabet::Symbol& input, const a
}
}
- addLocalTransition(state, input, automaton::State(VPADeterminizer::packToDVPAStateLabel(std::move(S1))), deterministic);
-}
-
-const automaton::State* existsDirtyState(const automaton::VisiblyPushdownNPDA& d) {
- for(const automaton::State& state : d.getStates()) {
- const label::Label& stateLabel = state.getName();
-
- for(const auto& transition : d.getCallTransitions()) {
- if(stateLabel != transition.first.first.getName()) continue;
-
- goto continue2;
- }
- return &state;
-
-continue2: while(false); //TODO remove this
- }
- return NULL;
-}
-
-void localClosure(std::set<label::Label>& states, const std::set<label::Label>& oldStates, const automaton::VisiblyPushdownNPDA& d) {
- std::set<label::Label> newStates;
-
- for(const label::Label& state : oldStates) {
- for(const auto& transition : d.getLocalTransitions()) {
- if(transition.second.begin()->getName() != state) continue;
-
- if(!states.count(transition.first.first.getName())) {
- states.insert(transition.first.first.getName());
- newStates.insert(transition.first.first.getName());
- }
- }
-
- for(const auto& transition : d.getReturnTransitions()) {
- if(transition.second.begin()->getName() != state) continue;
-
- const alphabet::Symbol& popSymbol = std::get<2>(transition.first);
- if(popSymbol == d.getBottomOfTheStackSymbol()) continue;
- const label::Label& popSymbolLabel = static_cast<const alphabet::LabeledSymbol&>(popSymbol.getData()).getLabel();
- const label::Label& statePart = static_cast<const label::LabelPairLabel&>(popSymbolLabel.getData()).getData().first;
-
- if(!states.count(statePart)) {
- states.insert(statePart);
- newStates.insert(statePart);
- }
- }
- }
-
- if(newStates.empty()) return;
- localClosure(states, newStates, d);
-}
-
-std::pair<automaton::State, alphabet::Symbol>* existsDirtyStateSymbol(const automaton::VisiblyPushdownNPDA& d) {
- for(const automaton::State& state : d.getStates()) {
- const label::Label& stateLabel = state.getName();
-
- std::set<label::Label> lc { stateLabel };
- localClosure(lc, std::set<label::Label>{stateLabel}, d); //intentional copy
-
- std::set<alphabet::Symbol> topSymbols;
- for(const label::Label& localState : lc) {
- for(const auto& transition : d.getCallTransitions()) {
- for(const auto& to : transition.second) {
- if(localState != to.first.getName()) continue;
-
- topSymbols.insert(to.second);
- }
- }
-
- if(d.getInitialStates().begin()->getName() == localState) {
- topSymbols.insert(d.getBottomOfTheStackSymbol());
- }
- }
-
- for(const auto& transition : d.getReturnTransitions()) {
- if(stateLabel != std::get<0>(transition.first).getName()) continue;
-
- topSymbols.erase(std::get<2>(transition.first));
- }
-
- if(!topSymbols.empty()) return new std::pair<automaton::State, alphabet::Symbol>(automaton::State(stateLabel), *topSymbols.begin());
- }
- return NULL;
-}
-
-std::set<label::Label> retrieveLabels(const std::set<automaton::State>& states) {
- std::set<label::Label> labels;
- for(const automaton::State& state : states) {
- labels.insert(state.getName());
- }
- return labels;
+ addLocalTransition(state, input, automaton::State(packToStateLabel(std::move(S1))), deterministic);
}
automaton::VisiblyPushdownNPDA VPADeterminizer::determinize(const automaton::VisiblyPushdownNPDA& n) {
@@ -297,13 +156,13 @@ automaton::VisiblyPushdownNPDA VPADeterminizer::determinize(const automaton::Vis
d.setLocalInputSymbols(n.getLocalInputAlphabet());
d.setReturnInputSymbols(n.getReturnInputAlphabet());
- label::Label initialLabel = VPADeterminizer::packToDVPAStateLabel(createIdentity(retrieveLabels(n.getInitialStates())));
+ label::Label initialLabel = packToStateLabel(createIdentity(retrieveLabels(n.getInitialStates())));
d.addState(automaton::State(initialLabel));
d.addInitialState(automaton::State(initialLabel));
for(;;) {
- std::pair<automaton::State, alphabet::Symbol>* stateSymbol = existsDirtyStateSymbol(d);
- const automaton::State* state = existsDirtyState(d);
+ std::pair<automaton::State, alphabet::Symbol>* stateSymbol = existsDirtyStateSymbol(d, n);
+ const automaton::State* state = existsDirtyState(d, n);
if(stateSymbol != NULL) {
for(const alphabet::Symbol& symbol : n.getReturnInputAlphabet()) {
if(stateSymbol->second == d.getBottomOfTheStackSymbol()) {
@@ -317,7 +176,7 @@ automaton::VisiblyPushdownNPDA VPADeterminizer::determinize(const automaton::Vis
for(const alphabet::Symbol& symbol : n.getLocalInputAlphabet()) {
local(*state, symbol, n, d);
}
- for(const alphabet::Symbol symbol : n.getCallInputAlphabet()) {
+ for(const alphabet::Symbol& symbol : n.getCallInputAlphabet()) {
call(*state, symbol, n, d);
}
} else {
@@ -327,7 +186,7 @@ automaton::VisiblyPushdownNPDA VPADeterminizer::determinize(const automaton::Vis
std::set<label::Label> finalLabels = retrieveLabels(n.getFinalStates());
for(const automaton::State& state : d.getStates()) {
- const std::set<label::Label> labels = retrieveDSubSet(VPADeterminizer::unpackFromDVPAStateLabel(state.getName()));
+ const std::set<label::Label> labels = retrieveDSubSet(unpackFromStateLabel(state.getName()));
if(!std::empty_intersection(finalLabels, labels)) {
d.addFinalState(state);
diff --git a/alib2algo/src/determinize/vpa/VPADeterminizer.h b/alib2algo/src/determinize/vpa/VPADeterminizer.h
index 0910496ee8..d305786129 100644
--- a/alib2algo/src/determinize/vpa/VPADeterminizer.h
+++ b/alib2algo/src/determinize/vpa/VPADeterminizer.h
@@ -10,13 +10,6 @@ namespace determinize {
*/
class VPADeterminizer {
public:
- static label::Label packToDVPAStateLabel(std::set<std::pair<label::Label, label::Label>>&& data);
-
- static std::set<std::pair<label::Label, label::Label>> unpackFromDVPAStateLabel(const label::Label& data);
-
- static label::Label packToDVPAStackSymbolLabel(std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol>&& data);
-
- static std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol> unpackFromDVPAStackSymbolLabel(const label::Label& data);
/**
* Runs determinization algorithm on nondeterministic vpa given in constructor.
*
--
GitLab