From 4405f5b61b7c017fa380c6c403e975c3e899e405 Mon Sep 17 00:00:00 2001
From: Jan Vesely <janvesely@janvesely.net>
Date: Sat, 18 Jan 2014 18:34:14 +0100
Subject: [PATCH] add vpa determinization with optimizied s-component

---
 adeterminize.vpa2/src/VPADeterminizer2.cpp  | 225 ++++++++++++++++++++
 adeterminize.vpa2/src/VPADeterminizer2.h    |  28 +++
 adeterminize.vpa2/src/adeterminize.vpa2.cpp |  34 +++
 3 files changed, 287 insertions(+)
 create mode 100644 adeterminize.vpa2/src/VPADeterminizer2.cpp
 create mode 100644 adeterminize.vpa2/src/VPADeterminizer2.h
 create mode 100644 adeterminize.vpa2/src/adeterminize.vpa2.cpp

diff --git a/adeterminize.vpa2/src/VPADeterminizer2.cpp b/adeterminize.vpa2/src/VPADeterminizer2.cpp
new file mode 100644
index 0000000000..a6df6c9b2a
--- /dev/null
+++ b/adeterminize.vpa2/src/VPADeterminizer2.cpp
@@ -0,0 +1,225 @@
+#include "VPADeterminizer2.h"
+
+namespace determinization {
+
+
+PDA VPADeterminizer2::determinize(PDA& nondeterministicVPA) {
+    PDA deterministicVPA;
+    map<string, StateData> states;
+    set<Symbol> internalSymbols;
+    set<Symbol> callSymbols;
+    set<Symbol> returnSymbols;
+
+    DeterminizationUtils::copyInputAlphabet(nondeterministicVPA, deterministicVPA);
+    VPADeterminizationUtils::divideInputAlphabet(nondeterministicVPA, internalSymbols, callSymbols, returnSymbols);
+    vector<PartialStackData> partialStackAlphabet = VPADeterminizationUtils::buildStackAlphabet(nondeterministicVPA,
+        deterministicVPA, callSymbols);
+    
+    const SComponent& initialS = VPADeterminizationUtils::getSComponentWithStatesIdentity(
+        nondeterministicVPA.getInitialStates());
+    const RComponent& initialR(nondeterministicVPA.getInitialStates());
+    const State& initialState = VPADeterminizationUtils::getOrCreateState(initialS, initialR, states, deterministicVPA);
+    deterministicVPA.addInitialState(initialState);
+    
+    set<TransitionPDA> transitions = nondeterministicVPA.getTransitions();
+    
+    while (true) {
+        StateData* unmarkedStateData = VPADeterminizationUtils::getUnmarkedState(states);
+        if (unmarkedStateData == NULL) {
+            break;
+        }
+        
+        // Internal symbols
+        for (set<Symbol>::iterator internalSymbol = internalSymbols.begin();
+                internalSymbol != internalSymbols.end();
+                internalSymbol++) {
+            SComponent sPrimed;
+            SComponent& s = unmarkedStateData->s;
+            for (set<StatesPair>::iterator statesPair = s.statesPairs.begin();
+                    statesPair != s.statesPairs.end();
+                    statesPair++) {
+                const State& q = statesPair->state1;
+                const State& qDoublePrimed = statesPair->state2;
+                for (set<TransitionPDA>::iterator transition = transitions.begin();
+                        transition != transitions.end();
+                        transition++) {
+                    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 (set<State>::iterator q = r.states.begin(); q != r.states.end(); q++) {
+                for (set<TransitionPDA>::iterator transition = transitions.begin();
+                        transition != transitions.end();
+                        transition++) {
+                    if (transition->getFrom() == *q && transition->getInput() == *internalSymbol) {
+                        const State& qPrimed = transition->getTo();
+                        rPrimed.states.insert(qPrimed);
+                    }
+                }
+            }
+            const State& fromState = unmarkedStateData->state;
+            const State& toState = VPADeterminizationUtils::getOrCreateState(sPrimed, rPrimed, states, deterministicVPA);
+            const TransitionPDA transition(fromState, *internalSymbol, toState);
+            deterministicVPA.addTransition(transition);
+        }
+        
+        // Call symbols
+        for (set<Symbol>::iterator callSymbol = callSymbols.begin();
+                callSymbol != callSymbols.end();
+                callSymbol++) {
+            RComponent rPrimed;
+            RComponent& r = unmarkedStateData->r;
+            for (set<State>::iterator q = r.states.begin(); q != r.states.end(); q++) {
+                for (set<TransitionPDA>::iterator transition = transitions.begin();
+                        transition != transitions.end();
+                        transition++) {
+                    if (transition->getFrom() == *q && transition->getInput() == *callSymbol) {
+                        const State& qPrimed = transition->getTo();
+                        rPrimed.states.insert(qPrimed);
+                    }
+                }
+            }
+            SComponent& s = unmarkedStateData->s;
+            const SComponent& sPrimed = VPADeterminizationUtils::getSComponentWithStatesIdentity(rPrimed.states);
+            const State& fromState = unmarkedStateData->state;
+            const State& toState = VPADeterminizationUtils::getOrCreateState(sPrimed, rPrimed, states, deterministicVPA);
+            string stackSymbolName = VPADeterminizationUtils::buildStackSymbolName(s, r, *callSymbol);
+            list<Symbol> pop;
+            list<Symbol> push(1, Symbol(stackSymbolName));
+            const TransitionPDA transition(fromState, *callSymbol, toState, pop, push);
+            deterministicVPA.addTransition(transition);
+        }
+        
+        // Return symbols
+        for (set<Symbol>::iterator returnSymbol = returnSymbols.begin();
+                returnSymbol != returnSymbols.end();
+                returnSymbol++) {
+            SComponent& s = unmarkedStateData->s;
+            RComponent& r = unmarkedStateData->r;
+            
+            // Empty stack
+            list<Symbol> bottomOfStack(1, VPADeterminizationUtils::BOTTOM_OF_STACK_SYMBOL);
+            SComponent sPrimed;
+            for (set<StatesPair>::iterator statesPair = s.statesPairs.begin();
+                    statesPair != s.statesPairs.end();
+                    statesPair++) {
+                const State& q = statesPair->state1;
+                const State& qDoublePrimed = statesPair->state2;
+                for (set<TransitionPDA>::iterator transition = transitions.begin();
+                        transition != transitions.end();
+                        transition++) {
+                    if (transition->getFrom() == qDoublePrimed && transition->getInput() == *returnSymbol &&
+                            transition->getPop() == bottomOfStack) {
+                        const State& qPrimed = transition->getTo();
+                        sPrimed.statesPairs.insert(StatesPair(q, qPrimed));
+                    }
+                }
+            }
+            RComponent rPrimed;
+            for (set<State>::iterator q = r.states.begin(); q != r.states.end(); q++) {
+                for (set<TransitionPDA>::iterator transition = transitions.begin();
+                        transition != transitions.end();
+                        transition++) {
+                    if (transition->getFrom() == *q && transition->getInput() == *returnSymbol &&
+                            transition->getPop() == bottomOfStack) {
+                        const State& qPrimed = transition->getTo();
+                        rPrimed.states.insert(qPrimed);
+                    }
+                }
+            }
+            const State& fromState = unmarkedStateData->state;
+            const State& toState = VPADeterminizationUtils::getOrCreateState(sPrimed, rPrimed, states, deterministicVPA);
+            list<Symbol> pop(1, VPADeterminizationUtils::BOTTOM_OF_STACK_SYMBOL);
+            list<Symbol> push;
+            const TransitionPDA transition(fromState, *returnSymbol, toState, pop, push);
+            deterministicVPA.addTransition(transition);
+            
+            // Otherwise
+            for (set<Symbol>::iterator callSymbol = callSymbols.begin(); callSymbol != callSymbols.end(); callSymbol++) {
+                set<StatesPair> update;
+                for (set<StatesPair>::iterator sPair = s.statesPairs.begin();
+                        sPair != s.statesPairs.end();
+                        sPair++) {
+                    const State& q1 = sPair->state1;
+                    const State& q2 = sPair->state2;
+                    for (set<TransitionPDA>::iterator transitionPush = transitions.begin();
+                            transitionPush != transitions.end();
+                            transitionPush++) {
+                        for (set<TransitionPDA>::iterator transitionPop = transitions.begin();
+                                transitionPop != transitions.end();
+                                transitionPop++) {
+                            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 (vector<PartialStackData>::iterator partialStackSymbol = partialStackAlphabet.begin();
+                        partialStackSymbol != partialStackAlphabet.end();
+                        partialStackSymbol++) {
+                    SComponent& sPrimed = partialStackSymbol->s;
+                    RComponent& rPrimed = partialStackSymbol->r;
+
+                    RComponent rDoublePrimed;
+                    for (set<StatesPair>::iterator updateItem = update.begin();
+                            updateItem != update.end();
+                            updateItem++) {
+                        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 (set<StatesPair>::iterator updateItem = update.begin();
+                            updateItem != update.end();
+                            updateItem++) {
+                        const State& q3 = updateItem->state1;
+                        const State& qPrimed = updateItem->state2;
+                        for (set<StatesPair>::iterator sPrimedPair = sPrimed.statesPairs.begin();
+                                sPrimedPair != sPrimed.statesPairs.end();
+                                sPrimedPair++) {
+                            if (sPrimedPair->state2 == q3) {
+                                const State& q = sPrimedPair->state1;
+                                sDoublePrimed.statesPairs.insert(StatesPair(q, qPrimed));
+                            }
+                        }
+                    }
+
+                    const State& fromState = unmarkedStateData->state;
+                    const State& toState = VPADeterminizationUtils::getOrCreateState(sDoublePrimed, rDoublePrimed,
+                        states, deterministicVPA);
+                    string stackSymbolName = VPADeterminizationUtils::buildStackSymbolName(sPrimed, rPrimed, *callSymbol);
+                    list<Symbol> pop(1, Symbol(stackSymbolName));
+                    list<Symbol> push;
+                    const TransitionPDA transition(fromState, *returnSymbol, toState, pop, push);
+                    deterministicVPA.addTransition(transition);
+                }
+            }
+        }
+    }
+    
+    // Final states
+    for (map<string, StateData>::iterator stateIter = states.begin(); stateIter != states.end(); stateIter++) {
+        const StateData& stateData = stateIter->second;
+        if (DeterminizationUtils::containSomeFinalStateOfAutomaton(stateData.r.states, nondeterministicVPA)) {
+            deterministicVPA.addFinalState(stateData.state);
+        }
+    }
+    
+    return deterministicVPA;
+}
+
+} /* namespace determinization */
diff --git a/adeterminize.vpa2/src/VPADeterminizer2.h b/adeterminize.vpa2/src/VPADeterminizer2.h
new file mode 100644
index 0000000000..73fc867c67
--- /dev/null
+++ b/adeterminize.vpa2/src/VPADeterminizer2.h
@@ -0,0 +1,28 @@
+#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 "DeterminizationUtils.h"
+#include "VPADeterminizationUtils.h"
+#include "VPADeterminizationStructs.h"
+
+using namespace std;
+using namespace automaton;
+using namespace alphabet;
+
+namespace determinization {
+
+class VPADeterminizer2 {
+public:
+    static PDA determinize(PDA& automaton);
+};
+
+} /* namespace determinization */
+#endif /* VPADETERMINIZER2_H_ */
\ No newline at end of file
diff --git a/adeterminize.vpa2/src/adeterminize.vpa2.cpp b/adeterminize.vpa2/src/adeterminize.vpa2.cpp
new file mode 100644
index 0000000000..fb31cc10b4
--- /dev/null
+++ b/adeterminize.vpa2/src/adeterminize.vpa2.cpp
@@ -0,0 +1,34 @@
+#include <iostream>
+#include <set>
+
+#include "automaton/UnknownAutomaton.h"
+#include "AutomatonFactory.h"
+#include "AlibException.h"
+#include "VPADeterminizer2.h"
+
+
+using namespace std;
+using namespace automaton;
+using namespace determinization;
+using namespace alib;
+
+
+int main(int argc, char** argv) {
+    UnknownAutomaton automaton;
+    
+    try {
+        string input(istreambuf_iterator<char>(cin), (istreambuf_iterator<char>()));
+        automaton = AutomatonFactory::fromString(input);
+        
+        Automaton* knownAutomaton = AutomatonFactory::buildAutomaton(automaton);
+        // TODO check that automaton is VPA
+        PDA deterministicVPA = VPADeterminizer2::determinize(*((PDA*) knownAutomaton));
+        deterministicVPA.toXML(cout);
+        
+        delete knownAutomaton;
+        
+    } catch (AlibException& e) {
+        cout << e.what() << endl;
+        return 0;
+    }
+}
\ No newline at end of file
-- 
GitLab