From fabf4c54ba3b4730ff86c07fe10db9505324d35b Mon Sep 17 00:00:00 2001
From: Jan Travnicek <Jan.Travnicek@fit.cvut.cz>
Date: Sun, 28 Sep 2014 20:55:55 +0200
Subject: [PATCH] remove old determinize
---
adeterminize/makefile | 20 --
adeterminize/src/Determinizer.cpp | 10 -
adeterminize/src/Determinizer.h | 29 --
adeterminize/src/adeterminize.cpp | 235 ----------------
adeterminize/src/common/Utils.cpp | 31 ---
adeterminize/src/common/Utils.h | 52 ----
.../src/rhdpda/RhdpdaDeterminizer.cpp | 259 ------------------
adeterminize/src/rhdpda/RhdpdaDeterminizer.h | 139 ----------
.../src/rhdpda/RhdpdaDeterminizer2.cpp | 236 ----------------
adeterminize/src/rhdpda/RhdpdaDeterminizer2.h | 131 ---------
.../src/rhdpda/RhdpdaDeterminizer3.cpp | 235 ----------------
adeterminize/src/rhdpda/RhdpdaDeterminizer3.h | 131 ---------
.../src/rhdpda/RhdpdaDeterminizer4.cpp | 235 ----------------
adeterminize/src/rhdpda/RhdpdaDeterminizer4.h | 135 ---------
adeterminize/src/rhdpda/RhdpdaStructs.h | 156 -----------
adeterminize/src/rhdpda/RhdpdaUtils.cpp | 164 -----------
adeterminize/src/rhdpda/RhdpdaUtils.h | 131 ---------
adeterminize/src/vpa/VpaDeterminizer.cpp | 228 ---------------
adeterminize/src/vpa/VpaDeterminizer.h | 110 --------
adeterminize/src/vpa/VpaDeterminizer2.cpp | 226 ---------------
adeterminize/src/vpa/VpaDeterminizer2.h | 110 --------
adeterminize/src/vpa/VpaStructs.h | 99 -------
adeterminize/src/vpa/VpaUtils.cpp | 144 ----------
adeterminize/src/vpa/VpaUtils.h | 118 --------
24 files changed, 3364 deletions(-)
delete mode 100644 adeterminize/makefile
delete mode 100644 adeterminize/src/Determinizer.cpp
delete mode 100644 adeterminize/src/Determinizer.h
delete mode 100644 adeterminize/src/adeterminize.cpp
delete mode 100644 adeterminize/src/common/Utils.cpp
delete mode 100644 adeterminize/src/common/Utils.h
delete mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer.cpp
delete mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer.h
delete mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer2.cpp
delete mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer2.h
delete mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer3.cpp
delete mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer3.h
delete mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer4.cpp
delete mode 100644 adeterminize/src/rhdpda/RhdpdaDeterminizer4.h
delete mode 100644 adeterminize/src/rhdpda/RhdpdaStructs.h
delete mode 100644 adeterminize/src/rhdpda/RhdpdaUtils.cpp
delete mode 100644 adeterminize/src/rhdpda/RhdpdaUtils.h
delete mode 100644 adeterminize/src/vpa/VpaDeterminizer.cpp
delete mode 100644 adeterminize/src/vpa/VpaDeterminizer.h
delete mode 100644 adeterminize/src/vpa/VpaDeterminizer2.cpp
delete mode 100644 adeterminize/src/vpa/VpaDeterminizer2.h
delete mode 100644 adeterminize/src/vpa/VpaStructs.h
delete mode 100644 adeterminize/src/vpa/VpaUtils.cpp
delete mode 100644 adeterminize/src/vpa/VpaUtils.h
diff --git a/adeterminize/makefile b/adeterminize/makefile
deleted file mode 100644
index 973abf7a9d..0000000000
--- a/adeterminize/makefile
+++ /dev/null
@@ -1,20 +0,0 @@
-CC=g++
-EXECUTABLE=adeterminize
-CCFLAGS= -std=c++11 -O2 -c -Wall -I../alib2/src -I/usr/include/libxml2/
-LDFLAGS= -L../alib/lib2 -lxml2 -lalib2 -Wl,-rpath,.
-
-SOURCES=$(shell find src/ -name *cpp)
-OBJECTS=$(patsubst src/%.cpp, obj/%.o, $(SOURCES))
-
-all: $(SOURCES) bin/$(EXECUTABLE)
-
-bin/$(EXECUTABLE): $(OBJECTS)
- mkdir -p bin
- $(CC) $(OBJECTS) -o $@ $(LDFLAGS)
-
-obj/%.o: src/%.cpp
- mkdir -p $(dir $@)
- $(CC) $(CCFLAGS) $< -o $@
-
-clean:
- $(RM) -r *.o *.d bin obj
diff --git a/adeterminize/src/Determinizer.cpp b/adeterminize/src/Determinizer.cpp
deleted file mode 100644
index b7c632bcb0..0000000000
--- a/adeterminize/src/Determinizer.cpp
+++ /dev/null
@@ -1,10 +0,0 @@
-#include "Determinizer.h"
-
-namespace determinization {
-
-Determinizer::~Determinizer(void)
-{
-
-}
-
-}
diff --git a/adeterminize/src/Determinizer.h b/adeterminize/src/Determinizer.h
deleted file mode 100644
index 84b61b2a71..0000000000
--- a/adeterminize/src/Determinizer.h
+++ /dev/null
@@ -1,29 +0,0 @@
-#ifndef DETERMINIZER_H_
-#define DETERMINIZER_H_
-
-#include "automaton/Automaton.h"
-
-using namespace std;
-using namespace automaton;
-
-namespace determinization {
-
-/**
- * Base class for all classes with determinization algorithms.
- */
-class Determinizer
-{
-
- public:
-
- virtual ~Determinizer();
-
- /**
- * Runs determinization algorithm.
- */
- virtual Automaton* determinize() = 0;
-
-};
-
-}
-#endif
diff --git a/adeterminize/src/adeterminize.cpp b/adeterminize/src/adeterminize.cpp
deleted file mode 100644
index 716ffedde2..0000000000
--- a/adeterminize/src/adeterminize.cpp
+++ /dev/null
@@ -1,235 +0,0 @@
-#include <iostream>
-#include <getopt.h>
-#include <string.h>
-#include <ctype.h>
-
-#include "automaton/UnknownAutomaton.h"
-#include "automaton/Automaton.h"
-#include "automaton/FSM/FSM.h"
-#include "automaton/PDA/PDA.h"
-#include "AutomatonFactory.h"
-#include "AlibException.h"
-
-#include "fsm/FsmDeterminizer.h"
-#include "idpda/IdpdaDeterminizer.h"
-#include "vpa/VpaDeterminizer.h"
-#include "vpa/VpaDeterminizer2.h"
-#include "vpa/VpaDeterminizer3.h"
-#include "rhdpda/RhdpdaDeterminizer.h"
-#include "rhdpda/RhdpdaDeterminizer2.h"
-#include "rhdpda/RhdpdaDeterminizer3.h"
-#include "rhdpda/RhdpdaDeterminizer4.h"
-
-using namespace std;
-using namespace automaton;
-using namespace determinization;
-using namespace alib;
-
-#define VERSION "0.0.1"
-
-#define TYPE_FSM "fsm"
-#define TYPE_IDPDA "idpda"
-#define TYPE_VPA "vpa"
-#define TYPE_RHDPDA "rhdpda"
-
-#define VERSION_1 "1"
-#define VERSION_2 "2"
-#define VERSION_3 "3"
-#define VERSION_4 "4"
-
-
-/**
- * Prints help to standard output.
- */
-void printHelp()
-{
- cout << "adeterminize " << VERSION << endl;
- cout << "Determinize various types of automaton." << endl;
- 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 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;
-}
-
-
-/**
- * Throws exception when input automaton isn't fsm.
- *
- * @param unknownAutomaton input automaton
- * @throws AlibException when input automaton isn't fsm
- */
-void validateInputAutomatonIsFsm(UnknownAutomaton& unknownAutomaton)
-{
- if (!AutomatonFactory::isFSM(unknownAutomaton)) {
- throw AlibException("Input automaton must be final-state machine.");
- }
-}
-
-
-/**
- * Throws exception when input automaton isn't pda.
- *
- * @param unknownAutomaton input automaton
- * @throws AlibException when input automaton isn't pda
- */
-void validateInputAutomatonIsPda(UnknownAutomaton& unknownAutomaton)
-{
- if (!AutomatonFactory::isPDA(unknownAutomaton)) {
- throw AlibException("Input automaton must be pushdown automaton.");
- }
-}
-
-
-/**
- * Validates type of input automaton.
- *
- * @param unknownAutomaton input automaton
- * @throws AlibException when type of automaton isn't known or when automaton isn't of the right type
- */
-void validateAutomatonType(UnknownAutomaton& unknownAutomaton, string type)
-{
- if (type == TYPE_FSM) {
- validateInputAutomatonIsFsm(unknownAutomaton);
- } else if (type == TYPE_IDPDA || type == TYPE_VPA || type == TYPE_RHDPDA) {
- validateInputAutomatonIsPda(unknownAutomaton);
- } else {
- throw AlibException("Unknown type of input automaton. See help.");
- }
-}
-
-
-/**
- * Returns vpa determinizer according to given algorithm version.
- *
- * @param automaton input automaton
- * @param version version of algorithm
- * @return determinizer
- */
-Determinizer* getVpaDeterminizer(Automaton* automaton, string version)
-{
- if (version == VERSION_3) {
- return new vpa::VpaDeterminizer3((PDA*) automaton);
- } else if (version == VERSION_2) {
- return new vpa::VpaDeterminizer2((PDA*) automaton);
- }
- return new vpa::VpaDeterminizer((PDA*) automaton);
-}
-
-
-/**
- * Returns rhdpda determinizer according to given algorithm version.
- *
- * @param automaton input automaton
- * @param version version of algorithm
- * @return determinizer
- */
-Determinizer* getRhdpdaDeterminizer(Automaton* automaton, string version)
-{
- if (version == VERSION_4) {
- return new rhdpda::RhdpdaDeterminizer4((PDA*) automaton);
- } else if (version == VERSION_3) {
- return new rhdpda::RhdpdaDeterminizer3((PDA*) automaton);
- } else if (version == VERSION_2) {
- return new rhdpda::RhdpdaDeterminizer2((PDA*) automaton);
- }
- return new rhdpda::RhdpdaDeterminizer((PDA*) automaton);
-}
-
-
-/**
- * Converts given type to lower case.
- *
- * @param type
- * @return type in lower case
- */
-string getLowerCaseType(string type)
-{
- string lowerCaseType;
- for (const auto& c : type) {
- lowerCaseType.append(1, tolower(c));
- }
- return lowerCaseType;
-}
-
-
-/**
- * Returns determinizer according to given automaton type and algorithm version.
- *
- * @param automaton input automaton
- * @param type type of automaton
- * @param version algorithm version
- * @return determinizer
- */
-Determinizer* getDeterminizer(Automaton* automaton, string type, string version)
-{
- if (type == TYPE_FSM) {
- return new fsm::FsmDeterminizer((FSM*) automaton);
-
- } else if (type == TYPE_IDPDA) {
- return new idpda::IdpdaDeterminizer((PDA*) automaton);
-
- } else if (type == TYPE_VPA) {
- return getVpaDeterminizer(automaton, version);
-
- } else if (type == TYPE_RHDPDA) {
- return getRhdpdaDeterminizer(automaton, version);
- }
-
- return NULL; // should not be reached
-}
-
-
-int main(int argc, char** argv)
-{
- static struct option longOptions[] = {
- {"type", required_argument, NULL, 't'},
- {"algorithm", required_argument, NULL, 'a'},
- {"version", no_argument, NULL, 'v'},
- {"help", no_argument, NULL, 'h'},
- {0, 0, 0, 0}
- };
-
- int longIndex = 0;
- int opt = 0;
- string type;
- string version = "1";
-
- while ((opt = getopt_long(argc, argv, "t:a:vh", longOptions, &longIndex)) != -1) {
- switch(opt) {
- case 't':
- type.assign(optarg, strlen(optarg));
- break;
- case 'a':
- version.assign(optarg, strlen(optarg));
- break;
- case 'v':
- case 'h':
- default:
- printHelp();
- return 0;
- }
- }
-
- type = getLowerCaseType(type);
-
- try {
- string input(istreambuf_iterator<char>(cin), (istreambuf_iterator<char>()));
- UnknownAutomaton unknownAutomaton = AutomatonFactory::fromString(input);
- validateAutomatonType(unknownAutomaton, type);
- Automaton* automaton = AutomatonFactory::buildAutomaton(unknownAutomaton);
- Determinizer* determinizer = getDeterminizer(automaton, type, version);
- Automaton* deterministicAutomaton = determinizer->determinize();
- deterministicAutomaton->toXML(cout);
-
- delete automaton;
- delete deterministicAutomaton;
- delete determinizer;
-
- } catch (AlibException& e) {
- cout << e.what() << endl;
- }
-
- return 0;
-}
diff --git a/adeterminize/src/common/Utils.cpp b/adeterminize/src/common/Utils.cpp
deleted file mode 100644
index a08cdc4a3f..0000000000
--- a/adeterminize/src/common/Utils.cpp
+++ /dev/null
@@ -1,31 +0,0 @@
-#include "Utils.h"
-
-namespace determinization {
-
-
-void Utils::copyInputAlphabet(const Automaton& source, Automaton& dest)
-{
- for (const auto& symbol : source.getInputAlphabet()) {
- dest.addInputSymbol(symbol);
- }
-}
-
-
-bool Utils::containFinalState(const set<State>& states, const Automaton& automaton)
-{
- const set<State>& finalStates = automaton.getFinalStates();
- set<State> intersection;
- set_intersection(finalStates.begin(), finalStates.end(), states.begin(), states.end(),
- inserter(intersection, intersection.begin()));
- return intersection.size() > 0;
-}
-
-
-void Utils::copyStackAlphabet(const PDA& source, PDA& dest) {
- for (const auto& symbol : source.getStackAlphabet()) {
- dest.addStackSymbol(symbol);
- }
-}
-
-
-}
diff --git a/adeterminize/src/common/Utils.h b/adeterminize/src/common/Utils.h
deleted file mode 100644
index bcfe020a3e..0000000000
--- a/adeterminize/src/common/Utils.h
+++ /dev/null
@@ -1,52 +0,0 @@
-#ifndef UTILS_H_
-#define UTILS_H_
-
-#include <set>
-#include <algorithm>
-
-#include "automaton/State.h"
-#include "automaton/Automaton.h"
-#include "automaton/PDA/PDA.h"
-
-using namespace std;
-using namespace automaton;
-
-namespace determinization {
-
-/**
- * Library class with some basic methods that can be used by determinization algorithms.
- */
-class Utils
-{
-
- public:
-
- /**
- * Copies input alphabet of source automaton into given dest automaton.
- *
- * @param source automaton to copy input alphabet from
- * @param dest automaton to copy input alphabet into
- */
- static void copyInputAlphabet(const Automaton& source, Automaton& dest);
-
- /**
- * Returns if given set of states contains at least one final state of given automaton.
- *
- * @param states set of states from given automaton
- * @param automaton
- * @return true, if given set of states contains final state, or false, if not
- */
- static bool containFinalState(const set<State>& states, const Automaton& automaton);
-
- /**
- * Copies stack alphabet of source pda into given dest pda.
- *
- * @param source pushdown automaton to copy stack alphabet from
- * @param dest pushdown automaton to copy stack alphabet into
- */
- static void copyStackAlphabet(const PDA& source, PDA& dest);
-
-};
-
-}
-#endif
diff --git a/adeterminize/src/rhdpda/RhdpdaDeterminizer.cpp b/adeterminize/src/rhdpda/RhdpdaDeterminizer.cpp
deleted file mode 100644
index de716490b9..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaDeterminizer.cpp
+++ /dev/null
@@ -1,259 +0,0 @@
-#include "RhdpdaDeterminizer.h"
-
-namespace determinization {
-namespace rhdpda {
-
-
-void RhdpdaDeterminizer::divideTransitions()
-{
- for (const auto& transition : this->rhdpda->getTransitions()) {
- if (transition.getPush().size() == 2) {
- this->pushTransitions.insert(transition);
- } else if (transition.getPush().size() == 1) {
- this->internalTransitions.insert(transition);
- } else {
- this->popTransitions.insert(transition);
- }
- }
-}
-
-
-void RhdpdaDeterminizer::generateTransitionsForAllPossibleStackSymbols(const TransitionPDA& sampleTransition)
-{
- const State& fromState = sampleTransition.getFrom();
- const State& toState = sampleTransition.getTo();
- const Symbol& inputSymbol = sampleTransition.getInput();
- const list<Symbol>& samplePop = sampleTransition.getPop();
- const list<Symbol>& samplePush = sampleTransition.getPush();
- for (const auto& xS : this->allSComponents) {
- for (const auto& xR : this->allRComponents) {
- for (const auto& xSymbol : this->rhdpda->getInputAlphabet()) {
- string X = this->buildStackSymbolName(xS, xR, xSymbol);
- list<Symbol> pop = samplePop;
- list<Symbol> push = samplePush;
- pop.push_back(X);
- push.push_back(X);
- const TransitionPDA transition(fromState, inputSymbol, toState, pop, push);
- this->rdpda->addTransition(transition);
- }
- }
- }
-}
-
-
-string RhdpdaDeterminizer::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input)
-{
- return RhdpdaUtils::buildStackSymbolName(s, r, input, *this->rdpda);
-}
-
-
-set<StateSymbolPair> RhdpdaDeterminizer::combineStatesWithSymbol(const set<State>& states, const Symbol& symbol)
-{
- return RhdpdaUtils::combineStatesWithSymbol(states, symbol);
-}
-
-
-const SComponent RhdpdaDeterminizer::getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs)
-{
- return RhdpdaUtils::getSComponentWithPairsIdentity(pairs);
-}
-
-
-const State& RhdpdaDeterminizer::getOrCreateState(const SComponent& s, const RComponent& r)
-{
- return RhdpdaUtils::getOrCreateState(s, r, this->states, *this->rdpda);
-}
-
-
-void RhdpdaDeterminizer::initDeterminization()
-{
- this->states.clear();
- this->internalTransitions.clear();
- this->pushTransitions.clear();
- this->popTransitions.clear();
-
- this->allStateSymbolPairs = RhdpdaUtils::buildAllStateSymbolPairs(*this->rhdpda);
- this->allSComponents = RhdpdaUtils::generateAllPossibleSComponents(this->allStateSymbolPairs);
- this->allRComponents = RhdpdaUtils::generateAllPossibleRComponents(this->allStateSymbolPairs);
-
- Utils::copyInputAlphabet(*this->rhdpda, *this->rdpda);
- this->divideTransitions();
-}
-
-
-RhdpdaDeterminizer::RhdpdaDeterminizer(PDA* rhdpda)
-{
- this->rhdpda = rhdpda;
-}
-
-
-Automaton* RhdpdaDeterminizer::determinize()
-{
- const Symbol& BOTTOM_OF_STACK_SYMBOL = RhdpdaUtils::BOTTOM_OF_STACK_SYMBOL;
-
- this->rdpda = new PDA();
- this->initDeterminization();
-
- set<StateSymbolPair> initialSPairs = this->combineStatesWithSymbol(this->rhdpda->getStates(), BOTTOM_OF_STACK_SYMBOL);
- set<StateSymbolPair> initialRPairs = this->combineStatesWithSymbol(this->rhdpda->getInitialStates(), BOTTOM_OF_STACK_SYMBOL);
- const SComponent& initialS = this->getSComponentWithPairsIdentity(initialSPairs);
- const RComponent& initialR(initialRPairs);
- const State& initialState = this->getOrCreateState(initialS, initialR);
- this->rdpda->addInitialState(initialState);
-
- while (true) {
- StateData* unmarkedStateData = RhdpdaUtils::getUnmarkedState(this->states);
- if (unmarkedStateData == NULL) {
- break;
- }
-
- // Internal
- for (const auto& a : this->rhdpda->getInputAlphabet()) {
- SComponent sPrimed;
- SComponent& s = unmarkedStateData->s;
- for (const auto& pairOfPairs : s.pairsOfPairs) {
- const StateSymbolPair& x = pairOfPairs.pair1;
- const State& r = pairOfPairs.pair2.state;
- const Symbol& Y = pairOfPairs.pair2.symbol;
- for (const auto& transition : this->internalTransitions) {
- if (transition.getFrom() == r && transition.getInput() == a && transition.getPop().front() == Y) {
- const State& q = transition.getTo();
- sPrimed.pairsOfPairs.insert(PairOfPairs(x, StateSymbolPair(q, Y)));
- }
- }
- }
- RComponent rPrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& pair : r.pairs) {
- const State& p = pair.state;
- const Symbol& Y = pair.symbol;
- for (const auto& transition : this->internalTransitions) {
- if (transition.getFrom() == p && transition.getInput() == a && transition.getPop().front() == Y) {
- const State& q = transition.getTo();
- rPrimed.pairs.insert(StateSymbolPair(q, Y));
- }
- }
- }
- if (sPrimed.pairsOfPairs.size() > 0 && rPrimed.pairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- const TransitionPDA transition(fromState, a, toState);
- this->generateTransitionsForAllPossibleStackSymbols(transition);
- }
- }
-
- // Push
- for (const auto& a : this->rhdpda->getInputAlphabet()) {
- SComponent sDoublePrimed = this->getSComponentWithPairsIdentity(this->allStateSymbolPairs);
- SComponent& s = unmarkedStateData->s;
- RComponent rDoublePrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& pair : r.pairs) {
- const State& p = pair.state;
- const Symbol& Y = pair.symbol;
- for (const auto& transition : this->pushTransitions) {
- if (transition.getFrom() == p && transition.getInput() == a && transition.getPop().front() == Y) {
- const State& q = transition.getTo();
- const Symbol& Z = transition.getPush().front();
- rDoublePrimed.pairs.insert(StateSymbolPair(q, Z));
- }
- }
- }
- if (rDoublePrimed.pairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(s, r, a);
- list<Symbol> pop = {};
- list<Symbol> push = {Symbol(stackSymbolName)};
- const TransitionPDA transition(fromState, a, toState, pop, push);
- this->generateTransitionsForAllPossibleStackSymbols(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) {
- const Symbol& Y = pushTransition.getPop().front();
- StateSymbolPair pair1(p, Y);
- StateSymbolPair pair2(q, Y);
- update.insert(PairOfPairs(pair1, pair2));
- }
- }
- }
- }
- }
- if (update.size() == 0) {
- continue;
- }
-
- for (const auto& sPrimed : this->allSComponents) {
- for (const auto& rPrimed : this->allRComponents) {
- RComponent rDoublePrimed;
- for (const auto& updateItem : update) {
- const StateSymbolPair& y = updateItem.pair1;
- const StateSymbolPair& x = updateItem.pair2;
- if (rPrimed.pairs.find(y) != rPrimed.pairs.end()) {
- rDoublePrimed.pairs.insert(x);
- }
- }
- SComponent sDoublePrimed;
- for (const auto& updateItem : update) {
- const StateSymbolPair& z = updateItem.pair1;
- const StateSymbolPair& y = updateItem.pair2;
- for (const auto& sPrimedPair : sPrimed.pairsOfPairs) {
- if (sPrimedPair.pair2 == z) {
- const StateSymbolPair& x = sPrimedPair.pair1;
- sDoublePrimed.pairsOfPairs.insert(PairOfPairs(x, y));
- }
- }
- }
- if (sDoublePrimed.pairsOfPairs.size() > 0 && rDoublePrimed.pairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(sPrimed, rPrimed, a);
- list<Symbol> pop = {Symbol(stackSymbolName)};
- list<Symbol> push = {};
- const TransitionPDA transition(fromState, b, toState, pop, push);
- this->rdpda->addTransition(transition);
- }
- }
- }
- }
- }
- }
-
- const set<State>& rhdpdaFinalStates = this->rhdpda->getFinalStates();
- for (const auto& state : this->states) {
- bool isFinalState = false;
- const RComponent& r = state.second.r;
- for (const auto& pair : r.pairs) {
- if (rhdpdaFinalStates.find(pair.state) != rhdpdaFinalStates.end()) {
- isFinalState = true;
- }
- }
- if (isFinalState) {
- this->rdpda->addFinalState(state.second.state);
- }
- }
-
- return this->rdpda;
-}
-
-
-}
-}
diff --git a/adeterminize/src/rhdpda/RhdpdaDeterminizer.h b/adeterminize/src/rhdpda/RhdpdaDeterminizer.h
deleted file mode 100644
index f29e511d4a..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaDeterminizer.h
+++ /dev/null
@@ -1,139 +0,0 @@
-#ifndef RHDPDADETERMINZER_H_
-#define RHDPDADETERMINZER_H_
-
-#include <string>
-#include <set>
-#include <map>
-#include <vector>
-
-#include "automaton/PDA/PDA.h"
-#include "automaton/Transition.h"
-#include "automaton/exception/AutomatonException.h"
-#include "alphabet/Symbol.h"
-
-#include "../common/Utils.h"
-#include "../Determinizer.h"
-#include "RhdpdaUtils.h"
-#include "RhdpdaStructs.h"
-
-using namespace std;
-using namespace automaton;
-using namespace alphabet;
-
-namespace determinization {
-namespace rhdpda {
-
-/**
- * Class for running basic determinization algorithm on rhdpda.
- */
-class RhdpdaDeterminizer : public Determinizer
-{
-
- private:
-
- /** Real-time height-deterministic pushdown automaton */
- PDA* rhdpda;
-
- /** Real-time deterministic pushdown automaton */
- PDA* rdpda;
-
- /** Map of states of deterministic pda, where key is the name of state and value is data about this state */
- map<string, StateData> states;
-
- /** Set of internal transitions from rhdpda */
- set<TransitionPDA> internalTransitions;
-
- /** Set of push transitions from rhdpda */
- set<TransitionPDA> pushTransitions;
-
- /** Set of pop transitions from rhdpda */
- set<TransitionPDA> popTransitions;
-
- /** Set of all possible pairs of states and stack symbols */
- set<StateSymbolPair> allStateSymbolPairs;
-
- /** Vector with all possible S components of deterministic pda */
- vector<SComponent> allSComponents;
-
- /** Vector with all possible R components of deterministic pda */
- vector<RComponent> allRComponents;
-
- /**
- * Divides transitions of rhdpda into internal, push and pop transitions.
- *
- * @return void
- */
- void divideTransitions();
-
- /**
- * Adds transitions into determinsitic pda with values from given sample transition and with symbol X
- * on the end of push and pop symbols, where X is any stack symbol.
- *
- * @param sampleTransition
- * @return void
- */
- void generateTransitionsForAllPossibleStackSymbols(const TransitionPDA& sampleTransition);
-
- /**
- * Returns name of stack symbol of deterministic pda which is created from given S and R component and input symbol.
- * This method also ensures that this stack symbol is already added into deterministic pda.
- *
- * @param s S component of stack symbol
- * @param r R component of stack symbol
- * @param input input symbol
- * @return name of stack symbol
- */
- string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input);
-
- /**
- * Returns state and symbol pairs that are created by combining state from given set of states and given symbol.
- *
- * @param states
- * @param symbol
- * @return state and symbol pairs that are created by combining given states and symbol
- */
- set<StateSymbolPair> combineStatesWithSymbol(const set<State>& states, const Symbol& symbol);
-
- /**
- * Returns S component that contains pairs where both elements are same. These pairs are created from given set
- * of state and symbol pairs.
- *
- * @param pairs set of state and symbol pairs from which to create identity pairs
- * @return pairs where both elements are same
- */
- const SComponent getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs);
-
- /**
- * Returns existing state from states map, if there is one with same name, or creates new one and adds it into
- * states map and deterministic pda.
- *
- * @param s S component of state
- * @param r R component of state
- * @return state of deterministic pda
- */
- const State& getOrCreateState(const SComponent& s, const RComponent& r);
-
- /**
- * Runs some initializiation stuff before determinization algorithm.
- */
- void initDeterminization();
-
- public:
-
- /**
- * @param rhdpda real-time height-deterministic pushdown automaton given for determinization
- */
- RhdpdaDeterminizer(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/RhdpdaDeterminizer2.cpp b/adeterminize/src/rhdpda/RhdpdaDeterminizer2.cpp
deleted file mode 100644
index 158cb2818a..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaDeterminizer2.cpp
+++ /dev/null
@@ -1,236 +0,0 @@
-#include "RhdpdaDeterminizer2.h"
-
-namespace determinization {
-namespace rhdpda {
-
-
-void RhdpdaDeterminizer2::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 RhdpdaDeterminizer2::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input)
-{
- return RhdpdaUtils::buildStackSymbolName(s, r, input, *this->rdpda);
-}
-
-
-set<StateSymbolPair> RhdpdaDeterminizer2::combineStatesWithSymbol(const set<State>& states, const Symbol& symbol)
-{
- return RhdpdaUtils::combineStatesWithSymbol(states, symbol);
-}
-
-
-const SComponent RhdpdaDeterminizer2::getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs)
-{
- return RhdpdaUtils::getSComponentWithPairsIdentity(pairs);
-}
-
-
-const State& RhdpdaDeterminizer2::getOrCreateState(const SComponent& s, const RComponent& r)
-{
- return RhdpdaUtils::getOrCreateState(s, r, this->states, *this->rdpda);
-}
-
-
-void RhdpdaDeterminizer2::initDeterminization()
-{
- this->states.clear();
- this->internalTransitions.clear();
- this->pushTransitions.clear();
- this->popTransitions.clear();
-
- this->allStateSymbolPairs = RhdpdaUtils::buildAllStateSymbolPairs(*this->rhdpda);
- this->allSComponents = RhdpdaUtils::generateAllPossibleSComponents(this->allStateSymbolPairs);
- this->allRComponents = RhdpdaUtils::generateAllPossibleRComponents(this->allStateSymbolPairs);
-
- Utils::copyInputAlphabet(*this->rhdpda, *this->rdpda);
- this->divideTransitions();
-}
-
-
-RhdpdaDeterminizer2::RhdpdaDeterminizer2(PDA* rhdpda)
-{
- this->rhdpda = rhdpda;
-}
-
-
-Automaton* RhdpdaDeterminizer2::determinize()
-{
- const Symbol& BOTTOM_OF_STACK_SYMBOL = RhdpdaUtils::BOTTOM_OF_STACK_SYMBOL;
-
- this->rdpda = new PDA();
- this->initDeterminization();
-
- set<StateSymbolPair> initialSPairs = this->combineStatesWithSymbol(this->rhdpda->getStates(), BOTTOM_OF_STACK_SYMBOL);
- set<StateSymbolPair> initialRPairs = this->combineStatesWithSymbol(this->rhdpda->getInitialStates(), BOTTOM_OF_STACK_SYMBOL);
- const SComponent& initialS = this->getSComponentWithPairsIdentity(initialSPairs);
- const RComponent& initialR(initialRPairs);
- const State& initialState = this->getOrCreateState(initialS, initialR);
- this->rdpda->addInitialState(initialState);
-
- while (true) {
- StateData* unmarkedStateData = RhdpdaUtils::getUnmarkedState(this->states);
- if (unmarkedStateData == NULL) {
- break;
- }
-
- // Internal
- for (const auto& a : this->rhdpda->getInputAlphabet()) {
- SComponent sPrimed;
- SComponent& s = unmarkedStateData->s;
- for (const auto& pairOfPairs : s.pairsOfPairs) {
- const StateSymbolPair& x = pairOfPairs.pair1;
- const State& r = pairOfPairs.pair2.state;
- const Symbol& Y = pairOfPairs.pair2.symbol;
- for (const auto& transition : this->internalTransitions) {
- if (transition.getFrom() == r && transition.getInput() == a) {
- const State& q = transition.getTo();
- sPrimed.pairsOfPairs.insert(PairOfPairs(x, StateSymbolPair(q, Y)));
- }
- }
- }
- RComponent rPrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& pair : r.pairs) {
- const State& p = pair.state;
- const Symbol& Y = pair.symbol;
- for (const auto& transition : this->internalTransitions) {
- if (transition.getFrom() == p && transition.getInput() == a) {
- const State& q = transition.getTo();
- rPrimed.pairs.insert(StateSymbolPair(q, Y));
- }
- }
- }
- if (sPrimed.pairsOfPairs.size() > 0 && rPrimed.pairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- const TransitionPDA transition(fromState, a, toState);
- this->rdpda->addTransition(transition);
- }
- }
-
- // Push
- for (const auto& a : this->rhdpda->getInputAlphabet()) {
- SComponent sDoublePrimed = this->getSComponentWithPairsIdentity(this->allStateSymbolPairs);
- SComponent& s = unmarkedStateData->s;
- RComponent rDoublePrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& pair : r.pairs) {
- const State& p = pair.state;
- for (const auto& transition : this->pushTransitions) {
- if (transition.getFrom() == p && transition.getInput() == a) {
- const State& q = transition.getTo();
- const Symbol& Z = transition.getPush().front();
- rDoublePrimed.pairs.insert(StateSymbolPair(q, Z));
- }
- }
- }
- if (rDoublePrimed.pairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(s, r, a);
- list<Symbol> pop = {};
- list<Symbol> push = {Symbol(stackSymbolName)};
- const TransitionPDA transition(fromState, a, toState, pop, push);
- this->rdpda->addTransition(transition);
- }
- }
-
- // Pop
- for (const auto& a : this->rhdpda->getInputAlphabet()) {
- for (const auto& b : this->rhdpda->getInputAlphabet()) {
- SComponent& s = unmarkedStateData->s;
-
- set<StatesPair> 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) {
- update.insert(StatesPair(p, q));
- }
- }
- }
- }
- }
- if (update.size() == 0) {
- continue;
- }
-
- for (const auto& sPrimed : this->allSComponents) {
- for (const auto& rPrimed : this->allRComponents) {
- RComponent rDoublePrimed;
- for (const auto& updateItem : update) {
- const State& p = updateItem.state1;
- const State& q = updateItem.state2;
- for (const auto& rPrimedPair : rPrimed.pairs) {
- if (rPrimedPair.state == p) {
- const Symbol& Y = rPrimedPair.symbol;
- rDoublePrimed.pairs.insert(StateSymbolPair(q, Y));
- }
- }
- }
- SComponent sDoublePrimed;
- for (const auto& updateItem : update) {
- const State& p = updateItem.state1;
- const State& q = updateItem.state2;
- for (const auto& sPrimedPair : sPrimed.pairsOfPairs) {
- if (sPrimedPair.pair2.state == p) {
- const StateSymbolPair& x = sPrimedPair.pair1;
- const Symbol& Y = sPrimedPair.pair2.symbol;
- sDoublePrimed.pairsOfPairs.insert(PairOfPairs(x, StateSymbolPair(q, Y)));
- }
- }
- }
- if (sDoublePrimed.pairsOfPairs.size() > 0 && rDoublePrimed.pairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(sPrimed, rPrimed, a);
- list<Symbol> pop = {Symbol(stackSymbolName)};
- list<Symbol> push = {};
- const TransitionPDA transition(fromState, b, toState, pop, push);
- this->rdpda->addTransition(transition);
- }
- }
- }
- }
- }
- }
-
- const set<State>& rhdpdaFinalStates = this->rhdpda->getFinalStates();
- for (const auto& state : this->states) {
- bool isFinalState = false;
- const RComponent& r = state.second.r;
- for (const auto& pair : r.pairs) {
- if (rhdpdaFinalStates.find(pair.state) != rhdpdaFinalStates.end()) {
- isFinalState = true;
- }
- }
- if (isFinalState) {
- this->rdpda->addFinalState(state.second.state);
- }
- }
-
- return this->rdpda;
-}
-
-
-}
-}
diff --git a/adeterminize/src/rhdpda/RhdpdaDeterminizer2.h b/adeterminize/src/rhdpda/RhdpdaDeterminizer2.h
deleted file mode 100644
index de63f096a7..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaDeterminizer2.h
+++ /dev/null
@@ -1,131 +0,0 @@
-#ifndef RHDPDADETERMINZER2_H_
-#define RHDPDADETERMINZER2_H_
-
-#include <string>
-#include <set>
-#include <map>
-#include <vector>
-
-#include "automaton/PDA/PDA.h"
-#include "automaton/Transition.h"
-#include "automaton/exception/AutomatonException.h"
-#include "alphabet/Symbol.h"
-
-#include "../common/Utils.h"
-#include "../Determinizer.h"
-#include "RhdpdaUtils.h"
-#include "RhdpdaStructs.h"
-
-using namespace std;
-using namespace automaton;
-using namespace alphabet;
-using namespace determinization;
-
-namespace determinization {
-namespace rhdpda {
-
-/**
- * Class for running second version of determinization algorithm on rhdpda.
- */
-class RhdpdaDeterminizer2 : public Determinizer
-{
-
- private:
-
- /** Real-time height-deterministic pushdown automaton */
- PDA* rhdpda;
-
- /** Real-time deterministic pushdown automaton */
- PDA* rdpda;
-
- /** Map of states of deterministic pda, where key is the name of state and value is data about this state */
- map<string, StateData> states;
-
- /** Set of internal transitions from rhdpda */
- set<TransitionPDA> internalTransitions;
-
- /** Set of push transitions from rhdpda */
- set<TransitionPDA> pushTransitions;
-
- /** Set of pop transitions from rhdpda */
- set<TransitionPDA> popTransitions;
-
- /** Set of all possible pairs of states and stack symbols */
- set<StateSymbolPair> allStateSymbolPairs;
-
- /** Vector with all possible S components of deterministic pda */
- vector<SComponent> allSComponents;
-
- /** Vector with all possible R components of deterministic pda */
- vector<RComponent> allRComponents;
-
- /**
- * Divides transitions of rhdpda into internal, push and pop transitions.
- *
- * @return void
- */
- void divideTransitions();
-
- /**
- * Returns name of stack symbol of deterministic pda which is created from given S and R component and input symbol.
- * This method also ensures that this stack symbol is already added into deterministic pda.
- *
- * @param s S component of stack symbol
- * @param r R component of stack symbol
- * @param input input symbol
- * @return name of stack symbol
- */
- string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input);
-
- /**
- * Returns state and symbol pairs that are created by combining state from given set of states and given symbol.
- *
- * @param states
- * @param symbol
- * @return state and symbol pairs that are created by combining given states and symbol
- */
- set<StateSymbolPair> combineStatesWithSymbol(const set<State>& states, const Symbol& symbol);
-
- /**
- * Returns S component that contains pairs where both elements are same. These pairs are created from given set
- * of state and symbol pairs.
- *
- * @param pairs set of state and symbol pairs from which to create identity pairs
- * @return pairs where both elements are same
- */
- const SComponent getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs);
-
- /**
- * Returns existing state from states map, if there is one with same name, or creates new one and adds it into
- * states map and deterministic pda.
- *
- * @param s S component of state
- * @param r R component of state
- * @return state of deterministic pda
- */
- const State& getOrCreateState(const SComponent& s, const RComponent& r);
-
- /**
- * Runs some initializiation stuff before determinization algorithm.
- */
- void initDeterminization();
-
- public:
-
- /**
- * @param rhdpda real-time height-deterministic pushdown automaton given for determinization
- */
- RhdpdaDeterminizer2(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/RhdpdaDeterminizer3.cpp b/adeterminize/src/rhdpda/RhdpdaDeterminizer3.cpp
deleted file mode 100644
index 024f367df0..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaDeterminizer3.cpp
+++ /dev/null
@@ -1,235 +0,0 @@
-#include "RhdpdaDeterminizer3.h"
-
-namespace determinization {
-namespace rhdpda {
-
-
-void RhdpdaDeterminizer3::divideTransitions()
-{
- for (const auto& transition : this->rhdpda->getTransitions()) {
- if (transition.getPush().size() == 1) {
- this->pushTransitions.insert(transition);
- } else if (transition.getPop().size() == 1) {
- this->popTransitions.insert(transition);
- } else {
- this->internalTransitions.insert(transition);
- }
- }
-}
-
-
-string RhdpdaDeterminizer3::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input)
-{
- return RhdpdaUtils::buildStackSymbolName(s, r, input, *this->rdpda);
-}
-
-
-set<StateSymbolPair> RhdpdaDeterminizer3::combineStatesWithSymbol(const set<State>& states, const Symbol& symbol)
-{
- return RhdpdaUtils::combineStatesWithSymbol(states, symbol);
-}
-
-
-const SComponent RhdpdaDeterminizer3::getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs)
-{
- return RhdpdaUtils::getSComponentWithPairsIdentity(pairs);
-}
-
-
-const State& RhdpdaDeterminizer3::getOrCreateState(const SComponent& s, const RComponent& r)
-{
- return RhdpdaUtils::getOrCreateState(s, r, this->states, *this->rdpda);
-}
-
-
-void RhdpdaDeterminizer3::initDeterminization()
-{
- this->states.clear();
- this->internalTransitions.clear();
- this->pushTransitions.clear();
- this->popTransitions.clear();
-
- this->allStateSymbolPairs = RhdpdaUtils::buildAllStateSymbolPairs(*this->rhdpda);
- this->allSComponents = RhdpdaUtils::generateAllPossibleSComponents(this->allStateSymbolPairs);
- this->allRComponents = RhdpdaUtils::generateAllPossibleRComponents(this->allStateSymbolPairs);
-
- Utils::copyInputAlphabet(*this->rhdpda, *this->rdpda);
- this->divideTransitions();
-}
-
-
-RhdpdaDeterminizer3::RhdpdaDeterminizer3(PDA* rhdpda)
-{
- this->rhdpda = rhdpda;
-}
-
-
-Automaton* RhdpdaDeterminizer3::determinize()
-{
- const Symbol& BOTTOM_OF_STACK_SYMBOL = RhdpdaUtils::BOTTOM_OF_STACK_SYMBOL;
-
- this->rdpda = new PDA();
- this->initDeterminization();
-
- set<StateSymbolPair> initialPairs = this->combineStatesWithSymbol(this->rhdpda->getInitialStates(), BOTTOM_OF_STACK_SYMBOL);
- const SComponent& initialS = this->getSComponentWithPairsIdentity(initialPairs);
- const RComponent& initialR(initialPairs);
- const State& initialState = this->getOrCreateState(initialS, initialR);
- this->rdpda->addInitialState(initialState);
-
- while (true) {
- StateData* unmarkedStateData = RhdpdaUtils::getUnmarkedState(this->states);
- if (unmarkedStateData == NULL) {
- break;
- }
-
- // Internal
- for (const auto& a : this->rhdpda->getInputAlphabet()) {
- SComponent sPrimed;
- SComponent& s = unmarkedStateData->s;
- for (const auto& pairOfPairs : s.pairsOfPairs) {
- const StateSymbolPair& x = pairOfPairs.pair1;
- const State& r = pairOfPairs.pair2.state;
- const Symbol& Y = pairOfPairs.pair2.symbol;
- for (const auto& transition : this->internalTransitions) {
- if (transition.getFrom() == r && transition.getInput() == a) {
- const State& q = transition.getTo();
- sPrimed.pairsOfPairs.insert(PairOfPairs(x, StateSymbolPair(q, Y)));
- }
- }
- }
- RComponent rPrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& pair : r.pairs) {
- const State& p = pair.state;
- const Symbol& Y = pair.symbol;
- for (const auto& transition : this->internalTransitions) {
- if (transition.getFrom() == p && transition.getInput() == a) {
- const State& q = transition.getTo();
- rPrimed.pairs.insert(StateSymbolPair(q, Y));
- }
- }
- }
- if (sPrimed.pairsOfPairs.size() > 0 && rPrimed.pairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- const TransitionPDA transition(fromState, a, toState);
- this->rdpda->addTransition(transition);
- }
- }
-
- // Push
- for (const auto& a : this->rhdpda->getInputAlphabet()) {
- RComponent rDoublePrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& pair : r.pairs) {
- const State& p = pair.state;
- for (const auto& transition : this->pushTransitions) {
- if (transition.getFrom() == p && transition.getInput() == a) {
- const State& q = transition.getTo();
- const Symbol& Z = transition.getPush().front();
- rDoublePrimed.pairs.insert(StateSymbolPair(q, Z));
- }
- }
- }
- SComponent sDoublePrimed = this->getSComponentWithPairsIdentity(rDoublePrimed.pairs);
- SComponent& s = unmarkedStateData->s;
- if (rDoublePrimed.pairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(s, r, a);
- list<Symbol> pop = {};
- list<Symbol> push = {Symbol(stackSymbolName)};
- const TransitionPDA transition(fromState, a, toState, pop, push);
- this->rdpda->addTransition(transition);
- }
- }
-
- // Pop
- for (const auto& a : this->rhdpda->getInputAlphabet()) {
- for (const auto& b : this->rhdpda->getInputAlphabet()) {
- SComponent& s = unmarkedStateData->s;
-
- set<StatesPair> 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) {
- update.insert(StatesPair(p, q));
- }
- }
- }
- }
- }
- if (update.size() == 0) {
- continue;
- }
-
- for (const auto& sPrimed : this->allSComponents) {
- for (const auto& rPrimed : this->allRComponents) {
- RComponent rDoublePrimed;
- for (const auto& updateItem : update) {
- const State& p = updateItem.state1;
- const State& q = updateItem.state2;
- for (const auto& rPrimedPair : rPrimed.pairs) {
- if (rPrimedPair.state == p) {
- const Symbol& Y = rPrimedPair.symbol;
- rDoublePrimed.pairs.insert(StateSymbolPair(q, Y));
- }
- }
- }
- SComponent sDoublePrimed;
- for (const auto& updateItem : update) {
- const State& p = updateItem.state1;
- const State& q = updateItem.state2;
- for (const auto& sPrimedPair : sPrimed.pairsOfPairs) {
- if (sPrimedPair.pair2.state == p) {
- const StateSymbolPair& x = sPrimedPair.pair1;
- const Symbol& Y = sPrimedPair.pair2.symbol;
- sDoublePrimed.pairsOfPairs.insert(PairOfPairs(x, StateSymbolPair(q, Y)));
- }
- }
- }
- if (sDoublePrimed.pairsOfPairs.size() > 0 && rDoublePrimed.pairs.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(sPrimed, rPrimed, a);
- list<Symbol> pop = {Symbol(stackSymbolName)};
- list<Symbol> push = {};
- const TransitionPDA transition(fromState, b, toState, pop, push);
- this->rdpda->addTransition(transition);
- }
- }
- }
- }
- }
- }
-
- const set<State>& rhdpdaFinalStates = this->rhdpda->getFinalStates();
- for (const auto& state : this->states) {
- bool isFinalState = false;
- const RComponent& r = state.second.r;
- for (const auto& pair : r.pairs) {
- if (rhdpdaFinalStates.find(pair.state) != rhdpdaFinalStates.end()) {
- isFinalState = true;
- }
- }
- if (isFinalState) {
- this->rdpda->addFinalState(state.second.state);
- }
- }
-
- return this->rdpda;
-}
-
-
-}
-}
diff --git a/adeterminize/src/rhdpda/RhdpdaDeterminizer3.h b/adeterminize/src/rhdpda/RhdpdaDeterminizer3.h
deleted file mode 100644
index b5c6bad6db..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaDeterminizer3.h
+++ /dev/null
@@ -1,131 +0,0 @@
-#ifndef RHDPDADETERMINZER3_H_
-#define RHDPDADETERMINZER3_H_
-
-#include <string>
-#include <set>
-#include <map>
-#include <vector>
-
-#include "automaton/PDA/PDA.h"
-#include "automaton/Transition.h"
-#include "automaton/exception/AutomatonException.h"
-#include "alphabet/Symbol.h"
-
-#include "../common/Utils.h"
-#include "../Determinizer.h"
-#include "RhdpdaUtils.h"
-#include "RhdpdaStructs.h"
-
-using namespace std;
-using namespace automaton;
-using namespace alphabet;
-using namespace determinization;
-
-namespace determinization {
-namespace rhdpda {
-
-/**
- * Class for running third version of determinization algorithm on rhdpda.
- */
-class RhdpdaDeterminizer3 : public Determinizer
-{
-
- private:
-
- /** Real-time height-deterministic pushdown automaton */
- PDA* rhdpda;
-
- /** Real-time deterministic pushdown automaton */
- PDA* rdpda;
-
- /** Map of states of deterministic pda, where key is the name of state and value is data about this state */
- map<string, StateData> states;
-
- /** Set of internal transitions from rhdpda */
- set<TransitionPDA> internalTransitions;
-
- /** Set of push transitions from rhdpda */
- set<TransitionPDA> pushTransitions;
-
- /** Set of pop transitions from rhdpda */
- set<TransitionPDA> popTransitions;
-
- /** Set of all possible pairs of states and stack symbols */
- set<StateSymbolPair> allStateSymbolPairs;
-
- /** Vector with all possible S components of deterministic pda */
- vector<SComponent> allSComponents;
-
- /** Vector with all possible R components of deterministic pda */
- vector<RComponent> allRComponents;
-
- /**
- * Divides transitions of rhdpda into internal, push and pop transitions.
- *
- * @return void
- */
- void divideTransitions();
-
- /**
- * Returns name of stack symbol of deterministic pda which is created from given S and R component and input symbol.
- * This method also ensures that this stack symbol is already added into deterministic pda.
- *
- * @param s S component of stack symbol
- * @param r R component of stack symbol
- * @param input input symbol
- * @return name of stack symbol
- */
- string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input);
-
- /**
- * Returns state and symbol pairs that are created by combining state from given set of states and given symbol.
- *
- * @param states
- * @param symbol
- * @return state and symbol pairs that are created by combining given states and symbol
- */
- set<StateSymbolPair> combineStatesWithSymbol(const set<State>& states, const Symbol& symbol);
-
- /**
- * Returns S component that contains pairs where both elements are same. These pairs are created from given set
- * of state and symbol pairs.
- *
- * @param pairs set of state and symbol pairs from which to create identity pairs
- * @return pairs where both elements are same
- */
- const SComponent getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs);
-
- /**
- * Returns existing state from states map, if there is one with same name, or creates new one and adds it into
- * states map and deterministic pda.
- *
- * @param s S component of state
- * @param r R component of state
- * @return state of deterministic pda
- */
- const State& getOrCreateState(const SComponent& s, const RComponent& r);
-
- /**
- * Runs some initializiation stuff before determinization algorithm.
- */
- void initDeterminization();
-
- public:
-
- /**
- * @param rhdpda real-time height-deterministic pushdown automaton given for determinization
- */
- RhdpdaDeterminizer3(PDA* rhdpda);
-
- /**
- * Runs determinization algorithm on rhdpda given in constructor.
- *
- * @return real-time deterministic pushdown automaton
- */
- Automaton* determinize();
-
-};
-
-}
-}
-#endif
diff --git a/adeterminize/src/rhdpda/RhdpdaDeterminizer4.cpp b/adeterminize/src/rhdpda/RhdpdaDeterminizer4.cpp
deleted file mode 100644
index 1fddc484fa..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaDeterminizer4.cpp
+++ /dev/null
@@ -1,235 +0,0 @@
-#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<StatesPair> 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) {
- update.insert(StatesPair(p, q));
- }
- }
- }
- }
- }
- if (update.size() == 0) {
- continue;
- }
- for (const auto& sPrimed : this->allSComponents) {
- SComponent sDoublePrimed;
- for (const auto& updateItem : update) {
- const State& p = updateItem.state1;
- const State& q = updateItem.state2;
- 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
deleted file mode 100644
index 1df0da7bb4..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaDeterminizer4.h
+++ /dev/null
@@ -1,135 +0,0 @@
-#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
deleted file mode 100644
index 02ba833868..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaStructs.h
+++ /dev/null
@@ -1,156 +0,0 @@
-#ifndef RHDPDASTRUCTS_H_
-#define RHDPDASTRUCTS_H_
-
-#include <set>
-
-using namespace automaton;
-
-namespace determinization {
-namespace rhdpda {
-
-
-/**
- * Struct fot storing pair which consists of state and symbol.
- */
-struct StateSymbolPair
-{
- State state;
- Symbol symbol;
-
- StateSymbolPair(const State& state, const Symbol& symbol)
- : state(state),
- symbol(symbol) {}
-
- bool operator < (const StateSymbolPair& other) const
- {
- return (state < other.state) || ((state == other.state) && (symbol < other.symbol));
- }
-
- bool operator == (const StateSymbolPair& other) const
- {
- return (state == other.state) && (symbol == other.symbol);
- }
-
- bool operator != (const StateSymbolPair& other) const
- {
- return (state != other.state) || (symbol != other.symbol);
- }
-};
-
-
-/**
- * Struct for storing two pairs of state and symbol.
- */
-struct PairOfPairs
-{
- StateSymbolPair pair1;
- StateSymbolPair pair2;
-
- PairOfPairs(const StateSymbolPair& pair1, const StateSymbolPair& pair2)
- : pair1(pair1),
- pair2(pair2) {}
-
- bool operator < (const PairOfPairs& other) const
- {
- return (pair1 < other.pair1) || ((pair1 == other.pair1) && (pair2 < other.pair2));
- }
-
- bool operator == (const PairOfPairs& other) const
- {
- return (pair1 == other.pair1) && (pair2 == other.pair2);
- }
-
- bool operator != (const PairOfPairs& other) const
- {
- return (pair1 != other.pair1) || (pair2 != other.pair2);
- }
-};
-
-
-/**
- * Struct for storing S component of state from deterministic pda.
- */
-struct SComponent
-{
- set<PairOfPairs> pairsOfPairs;
- SComponent() {}
- SComponent(const set<PairOfPairs>& pairsOfPairs)
- : pairsOfPairs(pairsOfPairs) {}
-};
-
-
-/**
- * Struct for storing R component of state from deterministic pda.
- */
-struct RComponent
-{
- set<StateSymbolPair> pairs;
- RComponent() {}
- RComponent(const set<StateSymbolPair>& pairs)
- : pairs(pairs) {}
-};
-
-
-/**
- * Struct for storing data about state from deterministic pda.
- */
-struct StateData
-{
-
- /** State of deterministic pda */
- State state;
-
- /** S component of this state */
- SComponent s;
-
- /** R component of this state */
- RComponent r;
-
- /** Indicates if this state is already marked by determinization algorithm or not */
- bool isMarked;
-
- StateData(const State& state, const SComponent& s, const RComponent& r)
- : state(state),
- s(s),
- r(r),
- isMarked(false) {}
-
- StateData(const State& state, const SComponent& s)
- : state(state),
- s(s),
- isMarked(false) {}
-};
-
-
-/**
- * Struct fot storing pair of two states.
- */
-struct StatesPair
-{
- State state1;
- State state2;
-
- StatesPair(const State& state1, const State& state2)
- : state1(state1),
- state2(state2) {}
-
- bool operator < (const StatesPair& other) const
- {
- return (state1 < other.state1) || ((state1 == other.state1) && (state2 < other.state2));
- }
-
- bool operator == (const StatesPair& other) const
- {
- return (state1 == other.state1) && (state2 == other.state2);
- }
-
- bool operator != (const StatesPair& other) const
- {
- return (state1 != other.state1) || (state2 != other.state2);
- }
-};
-
-
-}
-}
-#endif
diff --git a/adeterminize/src/rhdpda/RhdpdaUtils.cpp b/adeterminize/src/rhdpda/RhdpdaUtils.cpp
deleted file mode 100644
index e241b84fd5..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaUtils.cpp
+++ /dev/null
@@ -1,164 +0,0 @@
-#include "RhdpdaUtils.h"
-
-namespace determinization {
-namespace rhdpda {
-
-
-const Symbol RhdpdaUtils::BOTTOM_OF_STACK_SYMBOL("_");
-
-
-string RhdpdaUtils::buildPairName(const StateSymbolPair& pair)
-{
- return "('" + pair.state.getName() + "', '" + pair.symbol.getSymbol() + "')";;
-}
-
-
-string RhdpdaUtils::buildStateName(const SComponent& s, const RComponent& r)
-{
- string name = "{";
- for (const auto& pairOfPairs : s.pairsOfPairs) {
- if (&pairOfPairs != &(*begin(s.pairsOfPairs))) {
- name += ", ";
- }
- name += "(" + buildPairName(pairOfPairs.pair1) + ", " + buildPairName(pairOfPairs.pair2) + ")";
- }
- name += "}, {";
- for (const auto& pair : r.pairs) {
- if (&pair != &(*begin(r.pairs))) {
- name += ", ";
- }
- name += buildPairName(pair);
- }
- return name + "}";
-}
-
-
-const State& RhdpdaUtils::getOrCreateState(const SComponent& s, const RComponent& r, map<string, StateData>& states,
- PDA& rdpda)
-{
- string stateName = buildStateName(s, r);
-
- map<string, StateData>::iterator statesIter = states.find(stateName);
- if (statesIter != states.end()) {
- return statesIter->second.state;
- }
-
- State state(stateName);
- StateData stateData(state, s, r);
- StateData& insertedData = states.insert(pair<string, StateData>(stateName, stateData)).first->second;
- rdpda.addState(state);
- return insertedData.state;
-}
-
-
-const SComponent RhdpdaUtils::getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs)
-{
- set<PairOfPairs> pairsOfPairs;
- for (const auto& pair : pairs) {
- pairsOfPairs.insert(PairOfPairs(pair, pair));
- }
- return SComponent(pairsOfPairs);
-}
-
-
-string RhdpdaUtils::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input, PDA& rdpda)
-{
- string name = "(" + buildStateName(s, r) + ")";
- name += ", " + input.getSymbol();
- try {
- rdpda.addStackSymbol(name);
- } catch (AutomatonException e) {
- /* Stack symbol already exists */
- }
- return name;
-}
-
-
-vector<SComponent> RhdpdaUtils::generateAllPossibleSComponents(set<StateSymbolPair>& pairs)
-{
- // Generate all possible pairs of pairs
- vector<PairOfPairs> possiblePairsOfPairs;
- for (const auto& pair1 : pairs) {
- for (const auto& pair2 : pairs) {
- possiblePairsOfPairs.push_back(PairOfPairs(pair1, pair2));
- }
- }
-
- // Generate all possible s components
- vector<SComponent> possibleS;
- long int possibleSSize = pow(2, possiblePairsOfPairs.size());
- for (long int i = 0; i < possibleSSize; i++) {
- set<PairOfPairs> pairsOfPairsSet;
- long int mask = 1;
- for (const auto& pairOfPairs : possiblePairsOfPairs) {
- if ((i & mask) != 0) {
- pairsOfPairsSet.insert(pairOfPairs);
- }
- mask <<= 1;
- }
- possibleS.push_back(SComponent(pairsOfPairsSet));
- }
-
- return possibleS;
-}
-
-
-vector<RComponent> RhdpdaUtils::generateAllPossibleRComponents(set<StateSymbolPair>& pairs)
-{
- // Generate all possible r components
- vector<RComponent> possibleR;
- long int possibleRSize = pow(2, pairs.size());
- for (long int i = 0; i < possibleRSize; i++) {
- set<StateSymbolPair> pairsSet;
- long int mask = 1;
- for (const auto& pair : pairs) {
- if ((i & mask) != 0) {
- pairsSet.insert(pair);
- }
- mask <<= 1;
- }
- possibleR.push_back(RComponent(pairsSet));
- }
-
- return possibleR;
-}
-
-
-StateData* RhdpdaUtils::getUnmarkedState(map<string, StateData>& states)
-{
- StateData* unmarkedStateData = NULL;
- for (auto& stateIter : states) {
- if (!stateIter.second.isMarked) {
- unmarkedStateData = &stateIter.second;
- unmarkedStateData->isMarked = true;
- return unmarkedStateData;
- }
- }
- return NULL;
-}
-
-
-set<StateSymbolPair> RhdpdaUtils::combineStatesWithSymbol(const set<State>& states, const Symbol& symbol)
-{
- set<StateSymbolPair> pairs;
- for (const auto& state : states) {
- pairs.insert(StateSymbolPair(state, symbol));
- }
- return pairs;
-}
-
-
-set<StateSymbolPair> RhdpdaUtils::buildAllStateSymbolPairs(PDA& rhdpda)
-{
- set<StateSymbolPair> allStateSymbolPairs;
- for (const auto& state : rhdpda.getStates()) {
- for (const auto& symbol : rhdpda.getStackAlphabet()) {
- allStateSymbolPairs.insert(StateSymbolPair(state, symbol));
- }
- }
- return allStateSymbolPairs;
-}
-
-
-}
-}
diff --git a/adeterminize/src/rhdpda/RhdpdaUtils.h b/adeterminize/src/rhdpda/RhdpdaUtils.h
deleted file mode 100644
index 570362912f..0000000000
--- a/adeterminize/src/rhdpda/RhdpdaUtils.h
+++ /dev/null
@@ -1,131 +0,0 @@
-#ifndef RHDPDAUTILS_H_
-#define RHDPDAUTILS_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 "RhdpdaStructs.h"
-
-using namespace std;
-using namespace automaton;
-using namespace alphabet;
-
-namespace determinization {
-namespace rhdpda {
-
-/**
- * Library class with some methods that can be used by all rhdpda determinization algorithms.
- */
-class RhdpdaUtils
-{
- public:
-
- /** Symbol which represents bottom of stack */
- static const Symbol BOTTOM_OF_STACK_SYMBOL;
-
- /**
- * Returns string representation of given state and symbol pair.
- *
- * @param pair
- * @return name of pair
- */
- static string buildPairName(const StateSymbolPair& pair);
-
- /**
- * Returns name of state of deterministic pda which is created from given S and R component.
- *
- * @param s S component of state
- * @param r R component of state
- * @return name of state
- */
- static string buildStateName(const SComponent& s, const RComponent& r);
-
- /**
- * Returns existing state from states map, if there is one with same name, or creates new one and adds it into
- * given states map and given pda.
- *
- * @param s S component of state
- * @param r R component of state
- * @param states map of existing states, where key is the name of state and value is data about this state
- * @param rdpda deterministic pda that contains given map of states
- * @return state of deterministic pda
- */
- static const State& getOrCreateState(const SComponent& s, const RComponent& r, map<string, StateData>& states,
- PDA& rdpda);
-
- /**
- * 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
- */
- static const SComponent getSComponentWithPairsIdentity(const set<StateSymbolPair>& pairs);
-
- /**
- * 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 given deterministic pda.
- *
- * @param s S component of stack symbol
- * @param r R component of stack symbol
- * @param input input symbol
- * @param rdpda deterministic pda
- * @return name of stack symbol
- */
- static string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input, PDA& rdpda);
-
- /**
- * Returns all possible S components of deterministic pda.
- *
- * @param pairs all possible pairs of state and symbol
- * @return all possible S components
- */
- static vector<SComponent> generateAllPossibleSComponents(set<StateSymbolPair>& pairs);
-
- /**
- * Returns all possible R components of deterministic pda.
- *
- * @param pairs all possible pairs of state and symbol
- * @return all possible R components
- */
- static vector<RComponent> generateAllPossibleRComponents(set<StateSymbolPair>& pairs);
-
- /**
- * Returns state data about first state in given states map that isn't marked yet. Returns NULL if all states
- * are already marked.
- *
- * @param states map of all states in deterministic pda
- * @return state data about first unmarked state
- */
- static StateData* getUnmarkedState(map<string, StateData>& states);
-
- /**
- * 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
- */
- static set<StateSymbolPair> combineStatesWithSymbol(const set<State>& states, const Symbol& symbol);
-
- /**
- * Returns all possible state and symbol pairs created with states and symbols from given rhdpda.
- *
- * @param rhdpda real-time height-deterministic pda
- * @return all possible state and symbol pairs
- */
- static set<StateSymbolPair> buildAllStateSymbolPairs(PDA& rhdpda);
-
-};
-
-}
-}
-#endif
diff --git a/adeterminize/src/vpa/VpaDeterminizer.cpp b/adeterminize/src/vpa/VpaDeterminizer.cpp
deleted file mode 100644
index 86242ccd59..0000000000
--- a/adeterminize/src/vpa/VpaDeterminizer.cpp
+++ /dev/null
@@ -1,228 +0,0 @@
-#include "VpaDeterminizer.h"
-
-namespace determinization {
-namespace vpa {
-
-
-void VpaDeterminizer::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->allRComponents = VpaUtils::generateAllRComponents(this->nvpa->getStates());
- this->dvpa->addStackSymbol(VpaUtils::BOTTOM_OF_STACK_SYMBOL);
-}
-
-
-const State& VpaDeterminizer::getOrCreateState(const SComponent& s, const RComponent& r)
-{
- return VpaUtils::getOrCreateState(s, r, this->states, *this->dvpa);
-}
-
-
-const SComponent VpaDeterminizer::getSComponentWithStatesIdentity(const set<State>& states)
-{
- return VpaUtils::getSComponentWithStatesIdentity(states);
-}
-
-
-string VpaDeterminizer::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input)
-{
- return VpaUtils::buildStackSymbolName(s, r, input, *this->dvpa);
-}
-
-
-VpaDeterminizer::VpaDeterminizer(PDA* nvpa)
-{
- this->nvpa = nvpa;
-}
-
-
-Automaton* VpaDeterminizer::determinize()
-{
- this->dvpa = new PDA();
- this->initDeterminization();
-
- const SComponent& initialS = this->getSComponentWithStatesIdentity(this->nvpa->getStates());
- const RComponent& initialR(this->nvpa->getInitialStates());
- const State& initialState = this->getOrCreateState(initialS, initialR);
- this->dvpa->addInitialState(initialState);
-
- while (true) {
- StateData* unmarkedStateData = VpaUtils::getUnmarkedState(this->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));
- }
- }
- }
- RComponent rPrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& q : r.states) {
- for (const auto& transition : this->nvpa->getTransitions()) {
- if (transition.getFrom() == q && transition.getInput() == internalSymbol) {
- const State& qPrimed = transition.getTo();
- rPrimed.states.insert(qPrimed);
- }
- }
- }
- if (sPrimed.statesPairs.size() > 0 && rPrimed.states.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- const TransitionPDA transition(fromState, internalSymbol, toState);
- this->dvpa->addTransition(transition);
- }
- }
-
- // Call symbols
- for (const auto& callSymbol : callSymbols) {
- RComponent rPrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& q : r.states) {
- 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) {
- SComponent& s = unmarkedStateData->s;
- const SComponent& sPrimed = this->getSComponentWithStatesIdentity(this->nvpa->getStates());
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- string stackSymbolName = this->buildStackSymbolName(s, r, callSymbol);
- list<Symbol> pop = {};
- list<Symbol> push = {stackSymbolName};
- const TransitionPDA transition(fromState, callSymbol, toState, pop, push);
- this->dvpa->addTransition(transition);
- }
- }
-
- // Return symbols
- for (const auto& returnSymbol : returnSymbols) {
- SComponent& s = unmarkedStateData->s;
- RComponent& r = unmarkedStateData->r;
-
- // 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));
- }
- }
- }
- RComponent rPrimed;
- for (const auto& q : r.states) {
- for (const auto& transition : this->nvpa->getTransitions()) {
- if (transition.getFrom() == q && transition.getInput() == returnSymbol &&
- transition.getPop() == bottomOfStack) {
- const State& qPrimed = transition.getTo();
- rPrimed.states.insert(qPrimed);
- }
- }
- }
- if (sPrimed.statesPairs.size() > 0 && rPrimed.states.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- 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;
- if (r.states.find(q2) != r.states.end()) {
- 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) {
- for (const auto& rPrimed : this->allRComponents) {
- RComponent rDoublePrimed;
- for (const auto& updateItem : update) {
- const State& q = updateItem.state1;
- const State& qPrimed = updateItem.state2;
- if (rPrimed.states.find(q) != rPrimed.states.end()) {
- rDoublePrimed.states.insert(qPrimed);
- }
- }
- 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 && rDoublePrimed.states.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(sPrimed, rPrimed, 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;
- if (Utils::containFinalState(stateData.r.states, *this->nvpa)) {
- this->dvpa->addFinalState(stateData.state);
- }
- }
-
- return this->dvpa;
-}
-
-
-}
-}
diff --git a/adeterminize/src/vpa/VpaDeterminizer.h b/adeterminize/src/vpa/VpaDeterminizer.h
deleted file mode 100644
index 4bb5434d3b..0000000000
--- a/adeterminize/src/vpa/VpaDeterminizer.h
+++ /dev/null
@@ -1,110 +0,0 @@
-#ifndef VPADETERMINIZER_H_
-#define VPADETERMINIZER_H_
-
-#include <string>
-#include <set>
-#include <map>
-#include <vector>
-
-#include "automaton/PDA/PDA.h"
-#include "automaton/Transition.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;
-using namespace determinization;
-
-namespace determinization {
-namespace vpa {
-
-/**
- * Class for running basic determinization algorithm on vpa.
- */
-class VpaDeterminizer : 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;
-
- /** Vector with all possible R components of deterministic vpa */
- vector<RComponent> allRComponents;
-
- /**
- * Runs some initializiation stuff before determinization algorithm.
- */
- void initDeterminization();
-
- /**
- * 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
- * @param r R component of state
- * @return state of deterministic vpa
- */
- const State& getOrCreateState(const SComponent& s, const RComponent& r);
-
- /**
- * 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);
-
- /**
- * Returns name of stack symbol of deterministic vpa 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 vpa.
- *
- * @param s S component of stack symbol
- * @param r R component of stack symbol
- * @param input input symbol
- * @return name of stack symbol
- */
- string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input);
-
- public:
-
- /**
- * @param nvpa nondeterministic visibly pushdown automaton given for determinization
- */
- VpaDeterminizer(PDA* nvpa);
-
- /**
- * Runs determinization algorithm on nondeterministic vpa given in constructor.
- *
- * @return deterministic visibly pushdown automaton
- */
- Automaton* determinize();
-
-};
-
-}
-}
-#endif
diff --git a/adeterminize/src/vpa/VpaDeterminizer2.cpp b/adeterminize/src/vpa/VpaDeterminizer2.cpp
deleted file mode 100644
index b48bdc8da7..0000000000
--- a/adeterminize/src/vpa/VpaDeterminizer2.cpp
+++ /dev/null
@@ -1,226 +0,0 @@
-#include "VpaDeterminizer2.h"
-
-namespace determinization {
-namespace vpa {
-
-
-void VpaDeterminizer2::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->allRComponents = VpaUtils::generateAllRComponents(this->nvpa->getStates());
- this->dvpa->addStackSymbol(VpaUtils::BOTTOM_OF_STACK_SYMBOL);
-}
-
-
-const State& VpaDeterminizer2::getOrCreateState(const SComponent& s, const RComponent& r)
-{
- return VpaUtils::getOrCreateState(s, r, this->states, *this->dvpa);
-}
-
-
-const SComponent VpaDeterminizer2::getSComponentWithStatesIdentity(const set<State>& states)
-{
- return VpaUtils::getSComponentWithStatesIdentity(states);
-}
-
-
-string VpaDeterminizer2::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input)
-{
- return VpaUtils::buildStackSymbolName(s, r, input, *this->dvpa);
-}
-
-
-VpaDeterminizer2::VpaDeterminizer2(PDA* nvpa)
-{
- this->nvpa = nvpa;
-}
-
-
-Automaton* VpaDeterminizer2::determinize()
-{
- this->dvpa = new PDA();
- this->initDeterminization();
-
- const SComponent& initialS = this->getSComponentWithStatesIdentity(this->nvpa->getInitialStates());
- const RComponent& initialR(this->nvpa->getInitialStates());
- const State& initialState = this->getOrCreateState(initialS, initialR);
- this->dvpa->addInitialState(initialState);
-
- while (true) {
- StateData* unmarkedStateData = VpaUtils::getUnmarkedState(this->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));
- }
- }
- }
- RComponent rPrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& q : r.states) {
- for (const auto& transition : this->nvpa->getTransitions()) {
- if (transition.getFrom() == q && transition.getInput() == internalSymbol) {
- const State& qPrimed = transition.getTo();
- rPrimed.states.insert(qPrimed);
- }
- }
- }
- if (sPrimed.statesPairs.size() > 0 && rPrimed.states.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- const TransitionPDA transition(fromState, internalSymbol, toState);
- this->dvpa->addTransition(transition);
- }
- }
-
- // Call symbols
- for (const auto& callSymbol : callSymbols) {
- RComponent rPrimed;
- RComponent& r = unmarkedStateData->r;
- for (const auto& q : r.states) {
- 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) {
- SComponent& s = unmarkedStateData->s;
- const SComponent& sPrimed = this->getSComponentWithStatesIdentity(rPrimed.states);
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- string stackSymbolName = this->buildStackSymbolName(s, r, 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;
- RComponent& r = unmarkedStateData->r;
-
- // 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));
- }
- }
- }
- RComponent rPrimed;
- for (const auto& q : r.states) {
- for (const auto& transition : this->nvpa->getTransitions()) {
- if (transition.getFrom() == q && transition.getInput() == returnSymbol &&
- transition.getPop() == bottomOfStack) {
- const State& qPrimed = transition.getTo();
- rPrimed.states.insert(qPrimed);
- }
- }
- }
- if (sPrimed.statesPairs.size() > 0 && rPrimed.states.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sPrimed, rPrimed);
- 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) {
- for (const auto& rPrimed : this->allRComponents) {
- RComponent rDoublePrimed;
- for (const auto& updateItem : update) {
- const State& q = updateItem.state1;
- const State& qPrimed = updateItem.state2;
- if (rPrimed.states.find(q) != rPrimed.states.end()) {
- rDoublePrimed.states.insert(qPrimed);
- }
- }
- 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 && rDoublePrimed.states.size() > 0) {
- const State& fromState = unmarkedStateData->state;
- const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
- string stackSymbolName = this->buildStackSymbolName(sPrimed, rPrimed, 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;
- if (Utils::containFinalState(stateData.r.states, *this->nvpa)) {
- this->dvpa->addFinalState(stateData.state);
- }
- }
-
- return this->dvpa;
-}
-
-
-}
-}
diff --git a/adeterminize/src/vpa/VpaDeterminizer2.h b/adeterminize/src/vpa/VpaDeterminizer2.h
deleted file mode 100644
index 324b90d1c0..0000000000
--- a/adeterminize/src/vpa/VpaDeterminizer2.h
+++ /dev/null
@@ -1,110 +0,0 @@
-#ifndef VPADETERMINIZER2_H_
-#define VPADETERMINIZER2_H_
-
-#include <string>
-#include <set>
-#include <map>
-#include <vector>
-
-#include "automaton/PDA/PDA.h"
-#include "automaton/Transition.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;
-using namespace determinization;
-
-namespace determinization {
-namespace vpa {
-
-/**
- * Class for running second version of determinization algorithm on vpa.
- */
-class VpaDeterminizer2 : 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;
-
- /** Vector with all possible R components of deterministic vpa */
- vector<RComponent> allRComponents;
-
- /**
- * Runs some initializiation stuff before determinization algorithm.
- */
- void initDeterminization();
-
- /**
- * 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
- * @param r R component of state
- * @return state of deterministic vpa
- */
- const State& getOrCreateState(const SComponent& s, const RComponent& r);
-
- /**
- * 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);
-
- /**
- * Returns name of stack symbol of deterministic vpa 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 vpa.
- *
- * @param s S component of stack symbol
- * @param r R component of stack symbol
- * @param input input symbol
- * @return name of stack symbol
- */
- string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input);
-
- public:
-
- /**
- * @param nvpa nondeterministic visibly pushdown automaton given for determinization
- */
- VpaDeterminizer2(PDA* nvpa);
-
- /**
- * Runs determinization algorithm on nondeterministic vpa given in constructor.
- *
- * @return deterministic visibly pushdown automaton
- */
- Automaton* determinize();
-
-};
-
-}
-}
-#endif
diff --git a/adeterminize/src/vpa/VpaStructs.h b/adeterminize/src/vpa/VpaStructs.h
deleted file mode 100644
index 2f9953c6c7..0000000000
--- a/adeterminize/src/vpa/VpaStructs.h
+++ /dev/null
@@ -1,99 +0,0 @@
-#ifndef VPASTRUCTS_H_
-#define VPASTRUCTS_H_
-
-#include <set>
-
-using namespace automaton;
-
-namespace determinization {
-namespace vpa {
-
-
-/**
- * Struct fot storing pair of two states from vpa.
- */
-struct StatesPair
-{
- State state1;
- State state2;
-
- StatesPair(const State& state1, const State& state2)
- : state1(state1),
- state2(state2) {}
-
- bool operator < (const StatesPair& other) const
- {
- return (state1 < other.state1) || ((state1 == other.state1) && (state2 < other.state2));
- }
-
- bool operator == (const StatesPair& other) const
- {
- return (state1 == other.state1) && (state2 == other.state2);
- }
-
- bool operator != (const StatesPair& other) const
- {
- return (state1 != other.state1) || (state2 != other.state2);
- }
-};
-
-
-/**
- * Struct for storing S component of state from deterministic vpa. S component consists of set of states pairs.
- */
-struct SComponent
-{
- set<StatesPair> statesPairs;
- SComponent() {}
- SComponent(const set<StatesPair>& statesPairs)
- : statesPairs(statesPairs) {}
-};
-
-
-/**
- * Struct for storing R component of state from deterministic vpa. R component consists of set of states.
- */
-struct RComponent
-{
- set<State> states;
- RComponent() {}
- RComponent(const set<State>& states)
- : states(states) {}
-};
-
-
-/**
- * Struct for storing data about state from deterministic vpa.
- */
-struct StateData
-{
-
- /** State of deterministic vpa */
- State state;
-
- /** S component of this state */
- SComponent s;
-
- /** R component of this state */
- RComponent r;
-
- /** Indicates if this state is already marked by determinization algorithm or not */
- bool isMarked;
-
- StateData(const State& state, const SComponent& s, const RComponent& r)
- : state(state),
- s(s),
- r(r),
- isMarked(false) {}
-
- StateData(const State& state, const SComponent& s)
- : state(state),
- s(s),
- isMarked(false) {}
-
-};
-
-
-}
-}
-#endif
diff --git a/adeterminize/src/vpa/VpaUtils.cpp b/adeterminize/src/vpa/VpaUtils.cpp
deleted file mode 100644
index 6feb6039c2..0000000000
--- a/adeterminize/src/vpa/VpaUtils.cpp
+++ /dev/null
@@ -1,144 +0,0 @@
-#include "VpaUtils.h"
-
-namespace determinization {
-namespace vpa {
-
-
-const Symbol VpaUtils::BOTTOM_OF_STACK_SYMBOL("⊥");
-
-
-string VpaUtils::buildStateName(const SComponent& s, const RComponent& r) {
- string name = "{";
- for (const auto& statesPair : s.statesPairs) {
- if (&statesPair != &(*begin(s.statesPairs))) {
- name += ", ";
- }
- name += "('" + statesPair.state1.getName() + "', '" + statesPair.state2.getName() + "')";
- }
- name += "}, {";
- for (const auto& state : r.states) {
- if (&state != &(*begin(r.states))) {
- name += ", ";
- }
- name += "'" + state.getName() + "'";
- }
- name += "}";
- return name;
-}
-
-
-const State& VpaUtils::getOrCreateState(const SComponent& s, const RComponent& r, map<string, StateData>& states, PDA& dvpa) {
- string stateName = buildStateName(s, r);
-
- map<string, StateData>::iterator statesIter = states.find(stateName);
- if (statesIter != states.end()) {
- return statesIter->second.state;
- }
-
- State state(stateName);
- StateData stateData(state, s, r);
- StateData& insertedData = states.insert(pair<string, StateData>(stateName, stateData)).first->second;
- dvpa.addState(state);
- return insertedData.state;
-}
-
-
-const SComponent VpaUtils::getSComponentWithStatesIdentity(const set<State>& states) {
- set<StatesPair> statesPairs;
- for (const auto& state : states) {
- statesPairs.insert(StatesPair(state, state));
- }
- return SComponent(statesPairs);
-}
-
-
-void VpaUtils::divideInputAlphabet(PDA& vpa, set<Symbol>& internalSymbols, set<Symbol>& callSymbols, set<Symbol>& returnSymbols) {
- for (const auto& input : vpa.getInputAlphabet()) {
- for (const auto& transition : vpa.getTransitions()) {
- if (transition.getInput() == input) {
- if (transition.getPush().size() != 0) {
- callSymbols.insert(input);
- } else if (transition.getPop().size() != 0) {
- returnSymbols.insert(input);
- } else {
- internalSymbols.insert(input);
- }
- break;
- }
- }
- }
-}
-
-
-string VpaUtils::buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input, PDA& dvpa) {
- string name = "(" + buildStateName(s, r) + ")";
- name += ", " + input.getSymbol();
- try {
- dvpa.addStackSymbol(name);
- } catch (AutomatonException e) {
- /* Stack symbol already exists */
- }
- return name;
-}
-
-
-vector<SComponent> VpaUtils::generateAllSComponents(const set<State>& states)
-{
- vector<StatesPair> possibleStatesPairs;
- for (const auto& state1 : states) {
- for (const auto& state2 : states) {
- possibleStatesPairs.push_back(StatesPair(state1, state2));
- }
- }
- vector<SComponent> possibleS;
- long int possibleSSize = pow(2, possibleStatesPairs.size());
- for (long int i = 0; i < possibleSSize; i++) {
- set<StatesPair> statesPairsSet;
- long int mask = 1;
- for (const auto& statesPair : possibleStatesPairs) {
- if ((i & mask) != 0) {
- statesPairsSet.insert(statesPair);
- }
- mask <<= 1;
- }
- possibleS.push_back(SComponent(statesPairsSet));
- }
- return possibleS;
-}
-
-
-vector<RComponent> VpaUtils::generateAllRComponents(const set<State>& states)
-{
- vector<RComponent> possibleR;
- long int possibleRSize = pow(2, states.size());
- for (long int i = 0; i < possibleRSize; i++) {
- set<State> statesSet;
- long int mask = 1;
- for (const auto& state : states) {
- if ((i & mask) != 0) {
- statesSet.insert(state);
- }
- mask <<= 1;
- }
- possibleR.push_back(RComponent(statesSet));
- }
- return possibleR;
-}
-
-
-StateData* VpaUtils::getUnmarkedState(map<string, StateData>& states) {
- StateData* unmarkedStateData = NULL;
- for (auto& stateIter : states) {
- StateData& stateData = stateIter.second;
- if (!stateData.isMarked) {
- unmarkedStateData = &stateData;
- unmarkedStateData->isMarked = true;
- return unmarkedStateData;
- }
- }
- return NULL;
-}
-
-
-}
-}
diff --git a/adeterminize/src/vpa/VpaUtils.h b/adeterminize/src/vpa/VpaUtils.h
deleted file mode 100644
index e95440e993..0000000000
--- a/adeterminize/src/vpa/VpaUtils.h
+++ /dev/null
@@ -1,118 +0,0 @@
-#ifndef VPANUTILS_H_
-#define VPANUTILS_H_
-
-#include <math.h>
-#include <string>
-#include <set>
-#include <map>
-#include <vector>
-
-#include "automaton/State.h"
-#include "automaton/PDA/PDA.h"
-#include "automaton/Transition.h"
-#include "automaton/exception/AutomatonException.h"
-#include "alphabet/Symbol.h"
-
-#include "VpaStructs.h"
-
-using namespace automaton;
-using namespace alphabet;
-
-namespace determinization {
-namespace vpa {
-
-/**
- * Library class with some methods that can be used by all vpa determinization algorithms.
- */
-class VpaUtils
-{
- public:
-
- /** Symbol which represents bottom of stack */
- static const Symbol BOTTOM_OF_STACK_SYMBOL;
-
- /**
- * Returns name of state of deterministic vpa which is created from given S and R component.
- *
- * @param s S component of state
- * @param r R component of state
- * @return name of state
- */
- static string buildStateName(const SComponent& s, const RComponent& r);
-
- /**
- * Returns existing state from states map, if there is one with same name, or creates new one and adds it into
- * given states map and given vpa.
- *
- * @param s S component of state
- * @param r R component of state
- * @param states map of existing states, where key is the name of state and value is data about this state
- * @param dvpa deterministic vpa that contains given map of states
- * @return state of deterministic vpa
- */
- static const State& getOrCreateState(const SComponent& s, const RComponent& r, map<string, StateData>& states,
- PDA& dvpa);
-
- /**
- * 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
- */
- static const SComponent getSComponentWithStatesIdentity(const set<State>& states);
-
- /**
- * Divides input alphabet of given pda into internal, call and return symbols.
- *
- * @param vpa vpa with input alphabet for dividing
- * @param internalSymbols output parameter with internal symbols
- * @param callSymbols output parameter with call symbols
- * @param returnSymbols output parameter with return symbols
- * @return void
- */
- static void divideInputAlphabet(PDA& vpa, set<Symbol>& internalSymbols, set<Symbol>& callSymbols,
- set<Symbol>& returnSymbols);
-
- /**
- * Returns name of stack symbol of deterministic vpa which is created from given S and R component and input symbol.
- * This method also ensures that this stack symbol is already added into given deterministic vpa.
- *
- * @param s S component of stack symbol
- * @param r R component of stack symbol
- * @param input input symbol
- * @param vpa deterministic vpa
- * @return name of stack symbol
- */
- static string buildStackSymbolName(const SComponent& s, const RComponent& r, const Symbol& input, PDA& dvpa);
-
- /**
- * Returns all possible S components of deterministic vpa.
- *
- * @param states all states of nondeterministic vpa
- * @return all possible S components
- */
- static vector<SComponent> generateAllSComponents(const set<State>& states);
-
- /**
- * Returns all possible R components of deterministic vpa.
- *
- * @param states all states of nondeterministic vpa
- * @return all possible R components
- */
- static vector<RComponent> generateAllRComponents(const set<State>& states);
-
- /**
- * Returns state data about first state in given states map that isn't marked yet. Returns NULL if all states
- * are already marked.
- *
- * @param states map of all states in vpa
- * @return state data about first unmarked state
- */
- static StateData* getUnmarkedState(map<string, StateData>& states);
-
-};
-
-
-}
-}
-#endif
--
GitLab