From 9dcfba2a8abf7eadd891ff9ea51df08c03e63522 Mon Sep 17 00:00:00 2001
From: Jan Travnicek <Jan.Travnicek@fit.cvut.cz>
Date: Sat, 20 Sep 2014 13:17:33 +0200
Subject: [PATCH] untested vpa determinisation
---
adeterminize/src/vpa/VpaDeterminizer3.cpp | 229 ------------
adeterminize/src/vpa/VpaDeterminizer3.h | 113 ------
adeterminize2/src/adeterminize.cpp | 20 +-
.../src/determinize/vpa/VPADeterminizer.cpp | 330 ++++++++++++++++++
.../src/determinize/vpa/VPADeterminizer.h | 31 ++
.../test-src/determinize/determinizeTest.cpp | 12 +-
.../src/automaton/AutomatonFromXMLParser.cpp | 8 +-
.../src/automaton/AutomatonToXMLComposer.cpp | 6 +-
examples2/automaton/NIDPDA0.xml | 88 +++++
examples2/automaton/NIDPDA1.xml | 154 ++++++++
10 files changed, 631 insertions(+), 360 deletions(-)
delete mode 100644 adeterminize/src/vpa/VpaDeterminizer3.cpp
delete mode 100644 adeterminize/src/vpa/VpaDeterminizer3.h
create mode 100644 alib2algo/src/determinize/vpa/VPADeterminizer.cpp
create mode 100644 alib2algo/src/determinize/vpa/VPADeterminizer.h
create mode 100644 examples2/automaton/NIDPDA0.xml
create mode 100644 examples2/automaton/NIDPDA1.xml
diff --git a/adeterminize/src/vpa/VpaDeterminizer3.cpp b/adeterminize/src/vpa/VpaDeterminizer3.cpp
deleted file mode 100644
index 3d6fa598fa..0000000000
--- a/adeterminize/src/vpa/VpaDeterminizer3.cpp
+++ /dev/null
@@ -1,229 +0,0 @@
-#include "VpaDeterminizer3.h"
-
-namespace determinization {
-namespace vpa {
-
-
-string VpaDeterminizer3::buildStateName(const SComponent& s)
-{
- string name = "{";
- for (const auto& statesPair : s.statesPairs) {
- if (&statesPair != &(*begin(s.statesPairs))) {
- name += ", ";
- }
- name += "('" + statesPair.state1.getName() + "', '" + statesPair.state2.getName() + "')";
- }
- name += "}";
- return name;
-}
-
-
-string VpaDeterminizer3::buildStackSymbolName(const SComponent& s, const Symbol& input)
-{
- string name = "(" + this->buildStateName(s) + ")";
- name += ", " + input.getSymbol();
- try {
- this->dvpa->addStackSymbol(name);
- } catch (AutomatonException e) {
- /* Stack symbol already exists */
- }
- return name;
-}
-
-
-const State& VpaDeterminizer3::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->dvpa->addState(state);
- return insertedData.state;
-}
-
-
-const SComponent VpaDeterminizer3::getSComponentWithStatesIdentity(const set<State>& states)
-{
- return VpaUtils::getSComponentWithStatesIdentity(states);
-}
-
-
-void VpaDeterminizer3::initDeterminization()
-{
- this->states.clear();
- this->internalSymbols.clear();
- this->callSymbols.clear();
- this->returnSymbols.clear();
- Utils::copyInputAlphabet(*this->nvpa, *this->dvpa);
- VpaUtils::divideInputAlphabet(*this->nvpa, this->internalSymbols, this->callSymbols, this->returnSymbols);
- this->allSComponents = VpaUtils::generateAllSComponents(this->nvpa->getStates());
- this->dvpa->addStackSymbol(VpaUtils::BOTTOM_OF_STACK_SYMBOL);
-}
-
-
-VpaDeterminizer3::VpaDeterminizer3(PDA* nvpa)
-{
- this->nvpa = nvpa;
-}
-
-
-Automaton* VpaDeterminizer3::determinize()
-{
- this->dvpa = new PDA();
- this->initDeterminization();
-
- const SComponent& initialS = this->getSComponentWithStatesIdentity(this->nvpa->getInitialStates());
- const State& initialState = this->getOrCreateState(initialS);
- this->dvpa->addInitialState(initialState);
-
- while (true) {
- StateData* unmarkedStateData = VpaUtils::getUnmarkedState(states);
- if (unmarkedStateData == NULL) {
- break;
- }
-
- // Internal symbols
- for (const auto& internalSymbol : internalSymbols) {
- SComponent sPrimed;
- SComponent& s = unmarkedStateData->s;
- for (const auto& statesPair : s.statesPairs) {
- const State& q = statesPair.state1;
- const State& qDoublePrimed = statesPair.state2;
- for (const auto& transition : this->nvpa->getTransitions()) {
- if (transition.getFrom() == qDoublePrimed && transition.getInput() == internalSymbol) {
- const State& qPrimed = transition.getTo();
- sPrimed.statesPairs.insert(StatesPair(q, qPrimed));
- }
- }
- }
- if (sPrimed.statesPairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed);
- const TransitionPDA transition(fromState, internalSymbol, toState);
- this->dvpa->addTransition(transition);
- }
- }
-
- // Call symbols
- for (const auto& callSymbol : callSymbols) {
- RComponent rPrimed;
- SComponent& s = unmarkedStateData->s;
- for (const auto& statesPair : s.statesPairs) {
- const State& q = statesPair.state2;
- for (const auto& transition : this->nvpa->getTransitions()) {
- if (transition.getFrom() == q && transition.getInput() == callSymbol) {
- const State& qPrimed = transition.getTo();
- rPrimed.states.insert(qPrimed);
- }
- }
- }
- if (rPrimed.states.size() > 0) {
- const SComponent& sPrimed = this->getSComponentWithStatesIdentity(rPrimed.states);
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed);
- string stackSymbolName = this->buildStackSymbolName(s, callSymbol);
- list<Symbol> pop = {};
- list<Symbol> push = {Symbol(stackSymbolName)};
- const TransitionPDA transition(fromState, callSymbol, toState, pop, push);
- this->dvpa->addTransition(transition);
- }
- }
-
- // Return symbols
- for (const auto& returnSymbol : returnSymbols) {
- SComponent& s = unmarkedStateData->s;
-
- // Empty stack
- list<Symbol> bottomOfStack = {VpaUtils::BOTTOM_OF_STACK_SYMBOL};
- SComponent sPrimed;
- for (const auto& statesPair : s.statesPairs) {
- const State& q = statesPair.state1;
- const State& qDoublePrimed = statesPair.state2;
- for (const auto& transition : this->nvpa->getTransitions()) {
- if (transition.getFrom() == qDoublePrimed && transition.getInput() == returnSymbol &&
- transition.getPop() == bottomOfStack) {
- const State& qPrimed = transition.getTo();
- sPrimed.statesPairs.insert(StatesPair(q, qPrimed));
- }
- }
- }
- if (sPrimed.statesPairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed);
- list<Symbol> pop = {VpaUtils::BOTTOM_OF_STACK_SYMBOL};
- list<Symbol> push = {};
- const TransitionPDA transition(fromState, returnSymbol, toState, pop, push);
- this->dvpa->addTransition(transition);
- }
-
- // Otherwise
- for (const auto& callSymbol : callSymbols) {
- set<StatesPair> update;
- for (const auto& sPair : s.statesPairs) {
- const State& q1 = sPair.state1;
- const State& q2 = sPair.state2;
- for (const auto& transitionPush : this->nvpa->getTransitions()) {
- for (const auto& transitionPop : this->nvpa->getTransitions()) {
- const State& q = transitionPush.getFrom();
- const State& qPrimed = transitionPop.getTo();
- if (transitionPush.getInput() == callSymbol && transitionPush.getTo() == q1 &&
- transitionPop.getInput() == returnSymbol && transitionPop.getFrom() == q2 &&
- transitionPush.getPush() == transitionPop.getPop()) {
- update.insert(StatesPair(q, qPrimed));
- }
- }
- }
- }
- if (update.size() == 0) {
- continue;
- }
- for (const auto& sPrimed : this->allSComponents) {
- SComponent sDoublePrimed;
- for (const auto& updateItem : update) {
- const State& q3 = updateItem.state1;
- const State& qPrimed = updateItem.state2;
- for (const auto& sPrimedPair : sPrimed.statesPairs) {
- if (sPrimedPair.state2 == q3) {
- const State& q = sPrimedPair.state1;
- sDoublePrimed.statesPairs.insert(StatesPair(q, qPrimed));
- }
- }
- }
- if (sDoublePrimed.statesPairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(sPrimed, callSymbol);
- list<Symbol> pop = {Symbol(stackSymbolName)};
- list<Symbol> push = {};
- const TransitionPDA transition(fromState, returnSymbol, toState, pop, push);
- this->dvpa->addTransition(transition);
- }
- }
- }
- }
- }
-
- // Final states
- for (const auto& stateIter : states) {
- const StateData& stateData = stateIter.second;
- set<State> secondStates;
- for (const auto& sPair : stateData.s.statesPairs) {
- secondStates.insert(sPair.state2);
- }
- if (Utils::containFinalState(secondStates, *this->nvpa)) {
- this->dvpa->addFinalState(stateData.state);
- }
- }
-
- return this->dvpa;
-}
-
-
-}
-}
diff --git a/adeterminize/src/vpa/VpaDeterminizer3.h b/adeterminize/src/vpa/VpaDeterminizer3.h
deleted file mode 100644
index 38202fdd30..0000000000
--- a/adeterminize/src/vpa/VpaDeterminizer3.h
+++ /dev/null
@@ -1,113 +0,0 @@
-#ifndef VPADETERMINIZER3_H_
-#define VPADETERMINIZER3_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 "VpaUtils.h"
-#include "VpaStructs.h"
-
-using namespace std;
-using namespace automaton;
-using namespace alphabet;
-
-namespace determinization {
-namespace vpa {
-
-/**
- * Class for running third version of determinization algorithm on vpa.
- */
-class VpaDeterminizer3 : public Determinizer
-{
-
- private:
-
- /** Nondeterministic visibly pushdown automaton */
- PDA* nvpa;
-
- /** Deterministic visibly pushdown automaton */
- PDA* dvpa;
-
- /** Map of states of deterministic vpa, where key is the name of state and value is data about this state */
- map<string, StateData> states;
-
- /** Set of internal input symbols from nondeterministic automaton */
- set<Symbol> internalSymbols;
-
- /** Set of call input symbols from nondeterministic automaton */
- set<Symbol> callSymbols;
-
- /** Set of return input symbols from nondeterministic automaton */
- set<Symbol> returnSymbols;
-
- /** Vector with all possible S components of deterministic vpa */
- vector<SComponent> allSComponents;
-
- /**
- * Returns name of state of deterministic vpa which is created from given S component.
- *
- * @param s S component of state
- * @return name of state
- */
- string buildStateName(const SComponent& s);
-
- /**
- * Returns name of stack symbol of deterministic vpa which is created from given S component and input symbol.
- * This method also ensures that this stack symbol is already added into deterministic vpa.
- *
- * @param s S component of stack symbol
- * @param input input symbol
- * @return name of stack symbol
- */
- string buildStackSymbolName(const SComponent& s, const Symbol& input);
-
- /**
- * 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 vpa.
- *
- * @param s S component of state
- * @return state of deterministic vpa
- */
- const State& getOrCreateState(const SComponent& s);
-
- /**
- * Returns S component that contains pairs where states are same.
- *
- * @param states set of states from which to create pairs
- * @return pairs where states are same
- */
- const SComponent getSComponentWithStatesIdentity(const set<State>& states);
-
- /**
- * Runs some initializiation stuff before determinization algorithm.
- */
- void initDeterminization();
-
- public:
-
- /**
- * @param nvpa nondeterministic visibly pushdown automaton given for determinization
- */
- VpaDeterminizer3(PDA* nvpa);
-
- /**
- * Runs determinization algorithm on nondeterministic vpa given in constructor.
- *
- * @return deterministic visibly pushdown automaton
- */
- Automaton* determinize();
-
-};
-
-}
-}
-#endif
diff --git a/adeterminize2/src/adeterminize.cpp b/adeterminize2/src/adeterminize.cpp
index 7f11fe1488..780b1ceb7a 100644
--- a/adeterminize2/src/adeterminize.cpp
+++ b/adeterminize2/src/adeterminize.cpp
@@ -11,7 +11,8 @@
#include "exception/AlibException.h"
#include "determinize/nfa/NFADeterminizer.h"
-//#include "idpda/IdpdaDeterminizer.h"
+#include "determinize/idpda/IDPDADeterminizer.h"
+#include "determinize/vpa/VPADeterminizer.h"
//#include "vpa/VpaDeterminizer.h"
//#include "vpa/VpaDeterminizer2.h"
//#include "vpa/VpaDeterminizer3.h"
@@ -113,14 +114,19 @@ int main(int argc, char** argv) {
} else {
throw exception::AlibException("Unsupported formalism");
}
- }
-
-/* } else if (type == TYPE_IDPDA) {
- return new idpda::IdpdaDeterminizer((PDA*) automaton);
+ } else if (type == TYPE_IDPDA) {
+ automaton::InputDrivenNPDA npda = alib::DataFactory::fromTokens<automaton::InputDrivenNPDA>(tokens);
+ automaton::DPDA dpda = determinize::IDPDADeterminizer::determinize(npda);
+ alib::DataFactory::toStdout(dpda);
+ return 0;
} else if (type == TYPE_VPA) {
- return getVpaDeterminizer(automaton, version);
-
+ automaton::VisiblyPushdownNPDA npda = alib::DataFactory::fromTokens<automaton::VisiblyPushdownNPDA>(tokens);
+ automaton::VisiblyPushdownNPDA dpda = determinize::VPADeterminizer::determinize(npda);
+ alib::DataFactory::toStdout(dpda);
+ return 0;
+ }
+/*
} else if (type == TYPE_RHDPDA) {
return getRhdpdaDeterminizer(automaton, version);
}*/
diff --git a/alib2algo/src/determinize/vpa/VPADeterminizer.cpp b/alib2algo/src/determinize/vpa/VPADeterminizer.cpp
new file mode 100644
index 0000000000..a676e490c9
--- /dev/null
+++ b/alib2algo/src/determinize/vpa/VPADeterminizer.cpp
@@ -0,0 +1,330 @@
+#include "VPADeterminizer.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"
+
+namespace determinize {
+
+label::Label VPADeterminizer::packToDVPAStateLabel(const std::set<std::pair<label::Label, label::Label>>& data) {
+ std::set<label::Label> res;
+ for(const auto& subData : data) {
+ res.insert(label::Label(label::LabelPairLabel(subData)));
+ }
+ return label::Label(label::LabelSetLabel(res));
+}
+
+std::set<std::pair<label::Label, label::Label>> VPADeterminizer::unpackFromDVPAStateLabel(const label::Label& data) {
+ std::set<std::pair<label::Label, label::Label>> res;
+ for (const auto& subData : static_cast<const label::LabelSetLabel&>(data.getData()).getData()) {
+ res.insert(static_cast<const label::LabelPairLabel&>(subData.getData()).getData());
+ }
+ return res;
+}
+
+label::Label VPADeterminizer::packToDVPAStackSymbolLabel(const std::pair<std::set<std::pair<label::Label, label::Label>>, label::Label>& data) {
+ std::set<label::Label> res;
+ for(const auto& subData : data.first) {
+ res.insert(label::Label(label::LabelPairLabel(subData)));
+ }
+ return label::Label(label::LabelPairLabel(std::make_pair(label::Label(label::LabelSetLabel(res)), data.second)));
+}
+
+std::pair<std::set<std::pair<label::Label, label::Label>>, label::Label> VPADeterminizer::unpackFromDVPAStackSymbolLabel(const label::Label& data) {
+ std::set<std::pair<label::Label, label::Label>> res;
+ for (const auto& subData : static_cast<const label::LabelSetLabel&>(static_cast<const label::LabelPairLabel&>(data.getData()).getData().first.getData()).getData()) {
+ res.insert(static_cast<const label::LabelPairLabel&>(subData.getData()).getData());
+ }
+ return std::make_pair(res, static_cast<const label::LabelPairLabel&>(data.getData()).getData().second);
+}
+
+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);
+ deterministic.addStackSymbol(dvpdaSymbol);
+
+ deterministic.addTransition(from, input, dvpdaSymbol, to);
+}
+
+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>> 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(VPADeterminizer::packToDVPAStateLabel(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>>, label::Label> pdaSymbolUnpack = VPADeterminizer::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;
+
+ for(const auto& transition : nondeterministic.getCallTransitions()) {
+ if(pdaSymbolUnpack.second != static_cast<const alphabet::LabeledSymbol&>(std::get<1>(transition.first).getData()).getLabel()) 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(VPADeterminizer::packToDVPAStateLabel(S2)), deterministic);
+}
+
+void addCallTransition(const automaton::State& from, const alphabet::Symbol& input, const automaton::State& to, const alphabet::Symbol& dvpdaSymbol, automaton::VisiblyPushdownNPDA& deterministic) {
+ deterministic.addState(from);
+ deterministic.addState(to);
+ deterministic.addStackSymbol(dvpdaSymbol);
+
+ deterministic.addTransition(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<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);
+ }
+ }
+ }
+
+ const label::Label& inputLabel = static_cast<const alphabet::LabeledSymbol&>(input.getData()).getLabel();
+
+ addCallTransition(state, input, automaton::State(VPADeterminizer::packToDVPAStateLabel(createIdentity(R1))), alphabet::Symbol(alphabet::LabeledSymbol(VPADeterminizer::packToDVPAStackSymbolLabel(std::make_pair(S, inputLabel)))), deterministic);
+}
+
+void addLocalTransition(const automaton::State& from, const alphabet::Symbol& input, const automaton::State& to, automaton::VisiblyPushdownNPDA& deterministic) {
+ deterministic.addState(from);
+ deterministic.addState(to);
+
+ deterministic.addTransition(from, input, to);
+}
+
+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>> 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(VPADeterminizer::packToDVPAStateLabel(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);
+ }
+ return NULL;
+}
+
+std::set<label::Label> localClosure(std::set<label::Label> states, const automaton::VisiblyPushdownNPDA& d) {
+ std::set<label::Label> newStates;
+
+ for(const label::Label& state : states) {
+ for(const auto& transition : d.getLocalTransitions()) {
+ if(!transition.second.count(automaton::State(state))) continue;
+
+ newStates.insert(transition.first.first.getName());
+ }
+
+ for(const auto& transition : d.getReturnTransitions()) {
+ if(!transition.second.count(automaton::State(state))) continue;
+
+ const alphabet::Symbol& popSymbol = std::get<2>(transition.first);
+ 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;
+ newStates.insert(statePart);
+ }
+ }
+ if(states == newStates) return states;
+ return localClosure(newStates, d);
+}
+
+std::pair<label::Label, 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 = localClosure(std::set<label::Label> {stateLabel}, d);
+ 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().count(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<label::Label, alphabet::Symbol>(stateLabel, *topSymbols.begin());
+ }
+ return NULL;
+}
+
+std::set<label::Label> retrieveLabels(std::set<automaton::State> states) {
+ std::set<label::Label> labels;
+ for(const automaton::State& state : states) {
+ labels.insert(state.getName());
+ }
+ return labels;
+}
+
+automaton::VisiblyPushdownNPDA VPADeterminizer::determinize(const automaton::VisiblyPushdownNPDA& n) {
+ automaton::VisiblyPushdownNPDA d(n.getBottomOfTheStackSymbol());
+ d.setCallInputSymbols(n.getCallInputAlphabet());
+ d.setLocalInputSymbols(n.getLocalInputAlphabet());
+ d.setReturnInputSymbols(n.getReturnInputAlphabet());
+
+ label::Label initialLabel = VPADeterminizer::packToDVPAStateLabel(createIdentity(retrieveLabels(n.getInitialStates())));
+ d.addState(automaton::State(initialLabel));
+ d.addInitialState(automaton::State(initialLabel));
+
+ for(;;) {
+ std::pair<label::Label, alphabet::Symbol>* stateSymbol = existsDirtyStateSymbol(d);
+ const automaton::State* state = existsDirtyState(d);
+ if(stateSymbol != NULL) {
+ for(alphabet::Symbol symbol : n.getReturnInputAlphabet()) {
+ 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...
+ } else if(state != NULL) {
+ for(alphabet::Symbol symbol : n.getLocalInputAlphabet()) {
+ local(*state, symbol, n, d);
+ }
+ for(alphabet::Symbol symbol : n.getCallInputAlphabet()) {
+ call(*state, symbol, n, d);
+ }
+ } else {
+ break;
+ }
+ }
+
+ std::set<label::Label> fin = retrieveLabels(n.getFinalStates());
+
+ for(automaton::State state : d.getStates()) {
+ std::set<label::Label> labels = retrieveDSubSet(VPADeterminizer::unpackFromDVPAStateLabel(state.getName()));
+ std::set<label::Label> finalLabels(fin);
+
+ finalLabels.erase(labels.begin(), labels.end());
+
+ if(!finalLabels.empty()) {
+ d.addFinalState(state);
+ }
+ }
+
+ return d;
+}
+
+}
diff --git a/alib2algo/src/determinize/vpa/VPADeterminizer.h b/alib2algo/src/determinize/vpa/VPADeterminizer.h
new file mode 100644
index 0000000000..a3b7a62346
--- /dev/null
+++ b/alib2algo/src/determinize/vpa/VPADeterminizer.h
@@ -0,0 +1,31 @@
+#ifndef VPADETERMINIZER_H_
+#define VPADETERMINIZER_H_
+
+#include "automaton/PDA/VisiblyPushdownNPDA.h"
+
+namespace determinize {
+
+/**
+ * Class for running basic determinization algorithm on vpa.
+ */
+class VPADeterminizer {
+public:
+ static label::Label packToDVPAStateLabel(const 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(const std::pair<std::set<std::pair<label::Label, label::Label>>, label::Label>& data);
+
+ static std::pair<std::set<std::pair<label::Label, label::Label>>, label::Label> unpackFromDVPAStackSymbolLabel(const label::Label& data);
+ /**
+ * Runs determinization algorithm on nondeterministic vpa given in constructor.
+ *
+ * @return deterministic visibly pushdown automaton
+ */
+ static automaton::VisiblyPushdownNPDA determinize(const automaton::VisiblyPushdownNPDA& nondeterministic);
+
+};
+
+} /* namespace determinize */
+
+#endif /* VPADETERMINIZER_h_ */
diff --git a/alib2algo/test-src/determinize/determinizeTest.cpp b/alib2algo/test-src/determinize/determinizeTest.cpp
index 0e7891b6ef..6f7187a560 100644
--- a/alib2algo/test-src/determinize/determinizeTest.cpp
+++ b/alib2algo/test-src/determinize/determinizeTest.cpp
@@ -10,6 +10,8 @@
#include "determinize/nfa/NFADeterminizer.h"
#include "determinize/idpda/IDPDADeterminizer.h"
+#include "factory/DataFactory.hpp"
+
#define CPPUNIT_IMPLY(x, y) CPPUNIT_ASSERT(!(x) || (y))
CPPUNIT_TEST_SUITE_REGISTRATION( determinizeTest );
@@ -28,13 +30,13 @@ void determinizeTest::testDeterminizeNFA() {
automaton.addState(automaton::State(3));
automaton.addInputSymbol(alphabet::symbolFrom("a"));
automaton.addInputSymbol(alphabet::symbolFrom("b"));
-
+
automaton.addTransition(automaton::State(1), alphabet::symbolFrom("a"), automaton::State(2));
automaton.addTransition(automaton::State(2), alphabet::symbolFrom("b"), automaton::State(1));
automaton.addInitialState(automaton::State(1));
automaton.addFinalState(automaton::State(3));
-
+
automaton::DFA determinized = determinize::NFADeterminizer::determinize(automaton);
CPPUNIT_ASSERT(determinized.getStates().size() == 3);
@@ -46,7 +48,7 @@ void determinizeTest::testDeterminizeIDPDA() {
automaton.addInputSymbol(alphabet::symbolFrom("a"));
automaton.addInputSymbol(alphabet::symbolFrom("b"));
-
+
automaton.setPushdownStoreOperation(alphabet::symbolFrom("a"), std::vector<alphabet::Symbol>{}, std::vector<alphabet::Symbol> {});
automaton.setPushdownStoreOperation(alphabet::symbolFrom("b"), std::vector<alphabet::Symbol>{}, std::vector<alphabet::Symbol> {});
@@ -58,7 +60,9 @@ void determinizeTest::testDeterminizeIDPDA() {
automaton.addInitialState(automaton::State(1));
automaton.addFinalState(automaton::State(3));
-
+
+ alib::DataFactory::toStdout(automaton);
+
automaton::DPDA determinized = determinize::IDPDADeterminizer::determinize(automaton);
CPPUNIT_ASSERT(determinized.getStates().size() == 3);
diff --git a/alib2data/src/automaton/AutomatonFromXMLParser.cpp b/alib2data/src/automaton/AutomatonFromXMLParser.cpp
index 052eb7def6..d781b89b51 100644
--- a/alib2data/src/automaton/AutomatonFromXMLParser.cpp
+++ b/alib2data/src/automaton/AutomatonFromXMLParser.cpp
@@ -48,10 +48,10 @@ Automaton AutomatonFromXMLParser::parseAutomaton(std::list<sax::Token>& input, c
return Automaton(parseSinglePopDPDA(input));
} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "InputDrivenNPDA")) {
if(!features.count(FEATURES::INPUT_DRIVEN_NPDA)) throw exception::AlibException();
- return Automaton(parseNPDA(input));
+ return Automaton(parseInputDrivenNPDA(input));
} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "VisiblyPushdownNPDA")) {
if(!features.count(FEATURES::VISIBLY_PUSHDOWN_NPDA)) throw exception::AlibException();
- return Automaton(parseSinglePopNPDA(input));
+ return Automaton(parseVisiblyPushdownNPDA(input));
} else if(isToken(input, sax::Token::TokenType::START_ELEMENT, "NPDA")) {
if(!features.count(FEATURES::NPDA)) throw exception::AlibException();
return Automaton(parseNPDA(input));
@@ -66,7 +66,7 @@ Automaton AutomatonFromXMLParser::parseAutomaton(std::list<sax::Token>& input, c
}
bool AutomatonFromXMLParser::first(std::list<sax::Token>& input) const {
- if(isToken(input, sax::Token::TokenType::START_ELEMENT, "automaton") || isToken(input, sax::Token::TokenType::START_ELEMENT, "EpsilonNFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "NFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "DFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "CompactNFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "ExtendedNFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "DPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "SinglePopDPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "NPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "SinglePopNPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "OneTapeDTM")) {
+ if(isToken(input, sax::Token::TokenType::START_ELEMENT, "automaton") || isToken(input, sax::Token::TokenType::START_ELEMENT, "EpsilonNFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "NFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "DFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "CompactNFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "ExtendedNFA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "DPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "SinglePopDPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "InputDrivenNPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "VisiblyPushdownNPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "NPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "SinglePopNPDA") || isToken(input, sax::Token::TokenType::START_ELEMENT, "OneTapeDTM")) {
return true;
} else {
return false;
@@ -532,7 +532,7 @@ void AutomatonFromXMLParser::parseInputToPushdownStoreOperation(std::list<sax::T
while (isTokenType(input, sax::Token::TokenType::START_ELEMENT)) {
popToken(input, sax::Token::TokenType::START_ELEMENT, "operation");
- alphabet::Symbol inputSymbol = parseTransitionInputSymbol(input);
+ alphabet::Symbol inputSymbol(alib::api<alphabet::Symbol>::parse(input));
std::vector<alphabet::Symbol> pop = parseTransitionPop(input);
std::vector<alphabet::Symbol> push = parseTransitionPush(input);
diff --git a/alib2data/src/automaton/AutomatonToXMLComposer.cpp b/alib2data/src/automaton/AutomatonToXMLComposer.cpp
index 941eaf6548..c30d83139e 100644
--- a/alib2data/src/automaton/AutomatonToXMLComposer.cpp
+++ b/alib2data/src/automaton/AutomatonToXMLComposer.cpp
@@ -118,7 +118,7 @@ void AutomatonToXMLComposer::composeBottomOfTheStackSymbol(std::list<sax::Token>
void AutomatonToXMLComposer::composeInputToPushdownStoreOperation(std::list<sax::Token>& out, const automaton::InputDrivenNPDA& automaton) const {
- out.push_back(sax::Token("inputToPushdownStoreOperation", sax::Token::TokenType::START_ELEMENT));
+ out.push_back(sax::Token("inputToPushdownStoreOperations", sax::Token::TokenType::START_ELEMENT));
for(const auto& pushdownStoreOperation : automaton.getPushdownStoreOperations()) {
out.push_back(sax::Token("operation", sax::Token::TokenType::START_ELEMENT));
@@ -129,7 +129,7 @@ void AutomatonToXMLComposer::composeInputToPushdownStoreOperation(std::list<sax:
out.push_back(sax::Token("operation", sax::Token::TokenType::END_ELEMENT));
}
- out.push_back(sax::Token("inputToPushdownStoreOperation", sax::Token::TokenType::END_ELEMENT));
+ out.push_back(sax::Token("inputToPushdownStoreOperations", sax::Token::TokenType::END_ELEMENT));
}
void AutomatonToXMLComposer::composeTransitions(std::list<sax::Token>& out, const UnknownAutomaton& automaton) const {
@@ -644,8 +644,8 @@ std::list<sax::Token> AutomatonToXMLComposer::compose(const InputDrivenNPDA& aut
composeInputAlphabet(out, automaton.getInputAlphabet());
composeStackAlphabet(out, automaton.getStackAlphabet());
composeInitialStates(out, automaton.getInitialStates());
- composeFinalStates(out, automaton.getFinalStates());
composeInitialStackSymbol(out, automaton.getInitialSymbol());
+ composeFinalStates(out, automaton.getFinalStates());
composeInputToPushdownStoreOperation(out, automaton);
composeTransitions(out, automaton);
diff --git a/examples2/automaton/NIDPDA0.xml b/examples2/automaton/NIDPDA0.xml
new file mode 100644
index 0000000000..941e5baeb0
--- /dev/null
+++ b/examples2/automaton/NIDPDA0.xml
@@ -0,0 +1,88 @@
+<InputDrivenNPDA>
+ <states>
+ <IntegerLabel>1</IntegerLabel>
+ <IntegerLabel>2</IntegerLabel>
+ <IntegerLabel>3</IntegerLabel>
+ </states>
+ <inputAlphabet>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ </inputAlphabet>
+ <stackAlphabet>
+ <LabeledSymbol>
+ <CharacterLabel>S</CharacterLabel>
+ </LabeledSymbol>
+ </stackAlphabet>
+ <initialStates>
+ <IntegerLabel>1</IntegerLabel>
+ </initialStates>
+ <initialStackSymbol>
+ <LabeledSymbol>
+ <CharacterLabel>S</CharacterLabel>
+ </LabeledSymbol>
+ </initialStackSymbol>
+ <finalStates>
+ <IntegerLabel>3</IntegerLabel>
+ </finalStates>
+ <inputToPushdownStoreOperations>
+ <operation>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ <pop/>
+ <push/>
+ </operation>
+ <operation>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ <pop/>
+ <push/>
+ </operation>
+ </inputToPushdownStoreOperations>
+ <transitions>
+ <transition>
+ <from>
+ <IntegerLabel>1</IntegerLabel>
+ </from>
+ <input>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ </input>
+ <to>
+ <IntegerLabel>2</IntegerLabel>
+ </to>
+ </transition>
+ <transition>
+ <from>
+ <IntegerLabel>2</IntegerLabel>
+ </from>
+ <input>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ </input>
+ <to>
+ <IntegerLabel>1</IntegerLabel>
+ </to>
+ </transition>
+ <transition>
+ <from>
+ <IntegerLabel>2</IntegerLabel>
+ </from>
+ <input>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ </input>
+ <to>
+ <IntegerLabel>3</IntegerLabel>
+ </to>
+ </transition>
+ </transitions>
+</InputDrivenNPDA>
diff --git a/examples2/automaton/NIDPDA1.xml b/examples2/automaton/NIDPDA1.xml
new file mode 100644
index 0000000000..6be4da5419
--- /dev/null
+++ b/examples2/automaton/NIDPDA1.xml
@@ -0,0 +1,154 @@
+<InputDrivenNPDA>
+ <states>
+ <IntegerLabel>0</IntegerLabel>
+ <IntegerLabel>1</IntegerLabel>
+ <IntegerLabel>2</IntegerLabel>
+ <IntegerLabel>3</IntegerLabel>
+ </states>
+ <inputAlphabet>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ <LabeledSymbol>
+ <StringLabel>c</StringLabel>
+ </LabeledSymbol>
+ <LabeledSymbol>
+ <StringLabel>d</StringLabel>
+ </LabeledSymbol>
+ </inputAlphabet>
+ <stackAlphabet>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ </stackAlphabet>
+ <initialStates>
+ <IntegerLabel>0</IntegerLabel>
+ </initialStates>
+ <initialStackSymbol>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ </initialStackSymbol>
+ <finalStates>
+ <IntegerLabel>3</IntegerLabel>
+ </finalStates>
+ <inputToPushdownStoreOperations>
+ <operation>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ <pop/>
+ <push>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ </push>
+ </operation>
+ <operation>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ <pop/>
+ <push>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ </push>
+ </operation>
+ <operation>
+ <LabeledSymbol>
+ <StringLabel>c</StringLabel>
+ </LabeledSymbol>
+ <pop>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ </pop>
+ <push/>
+ </operation>
+ <operation>
+ <LabeledSymbol>
+ <StringLabel>d</StringLabel>
+ </LabeledSymbol>
+ <pop>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ </pop>
+ <push/>
+ </operation>
+ </inputToPushdownStoreOperations>
+ <transitions>
+ <transition>
+ <from>
+ <IntegerLabel>0</IntegerLabel>
+ </from>
+ <input>
+ <LabeledSymbol>
+ <StringLabel>a</StringLabel>
+ </LabeledSymbol>
+ </input>
+ <to>
+ <IntegerLabel>1</IntegerLabel>
+ </to>
+ </transition>
+ <transition>
+ <from>
+ <IntegerLabel>1</IntegerLabel>
+ </from>
+ <input>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ </input>
+ <to>
+ <IntegerLabel>1</IntegerLabel>
+ </to>
+ </transition>
+ <transition>
+ <from>
+ <IntegerLabel>1</IntegerLabel>
+ </from>
+ <input>
+ <LabeledSymbol>
+ <StringLabel>b</StringLabel>
+ </LabeledSymbol>
+ </input>
+ <to>
+ <IntegerLabel>2</IntegerLabel>
+ </to>
+ </transition>
+ <transition>
+ <from>
+ <IntegerLabel>2</IntegerLabel>
+ </from>
+ <input>
+ <LabeledSymbol>
+ <StringLabel>c</StringLabel>
+ </LabeledSymbol>
+ </input>
+ <to>
+ <IntegerLabel>2</IntegerLabel>
+ </to>
+ </transition>
+ <transition>
+ <from>
+ <IntegerLabel>2</IntegerLabel>
+ </from>
+ <input>
+ <LabeledSymbol>
+ <StringLabel>d</StringLabel>
+ </LabeledSymbol>
+ </input>
+ <to>
+ <IntegerLabel>3</IntegerLabel>
+ </to>
+ </transition>
+ </transitions>
+</InputDrivenNPDA>
--
GitLab