diff --git a/adeterminize.vpa/src/VPADeterminizer.cpp b/adeterminize.vpa/src/VPADeterminizer.cpp
index 2fac2f4515b38f80d1ca4c39d802c1ef5338def2..62c916db74edde4aca65cb5ee806262516cac227 100644
--- a/adeterminize.vpa/src/VPADeterminizer.cpp
+++ b/adeterminize.vpa/src/VPADeterminizer.cpp
@@ -29,7 +29,7 @@ string VPADeterminizer::buildStateName(const SComponent& s, const RComponent& r)
 
 const State& VPADeterminizer::getOrCreateState(const SComponent& s, const RComponent& r) {
     string stateName = this->buildStateName(s, r);
-    
+
     map<string, StateData>::iterator statesIter = this->states.find(stateName);
     if (statesIter != this->states.end()) {
         return statesIter->second.state;
@@ -88,7 +88,7 @@ string VPADeterminizer::buildStackSymbolName(const SComponent& s, const RCompone
 void VPADeterminizer::buildStackAlphabet() {
     const set<State>& states = this->nondeterministicVPA->getStates();
     
-    // Generate all possible s items
+    // Generate all possible states pairs
     vector<StatesPair> possibleStatesPairs;
     for (set<State>::iterator state1 = states.begin(); state1 != states.end(); state1++) {
         for (set<State>::iterator state2 = states.begin(); state2 != states.end(); state2++) {
@@ -133,12 +133,17 @@ void VPADeterminizer::buildStackAlphabet() {
     for (vector<SComponent>::iterator s = possibleS.begin(); s != possibleS.end(); s++) {
         for (vector<RComponent>::iterator r = possibleR.begin(); r != possibleR.end(); r++) {
             this->partialStackAlphabet.push_back(PartialStackData(*s, *r));
-            for (set<Symbol>::iterator input = alphabet.begin(); input != alphabet.end(); input++) {
-                string stackSymbolName = this->buildStackSymbolName(*s, *r, *input);
+            for (set<Symbol>::iterator callSymbol = this->callSymbols.begin();
+                    callSymbol != this->callSymbols.end();
+                    callSymbol++) {
+                string stackSymbolName = this->buildStackSymbolName(*s, *r, *callSymbol);
                 this->deterministicVPA->addStackSymbol(Symbol(stackSymbolName));
             }
         }
     }
+
+    // Add bottom of stack symbol
+    this->deterministicVPA->addStackSymbol(BOTTOM_OF_STACK_SYMBOL);
 }
 
 
@@ -181,33 +186,35 @@ PDA* VPADeterminizer::determinize() {
         for (set<Symbol>::iterator internalSymbol = this->internalSymbols.begin();
                 internalSymbol != this->internalSymbols.end();
                 internalSymbol++) {
-            SComponent s;
-            SComponent& oldS = unmarkedStateData->s;
-            for (set<StatesPair>::iterator statesPair = oldS.statesPairs.begin();
-                    statesPair != oldS.statesPairs.end();
+            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() == statesPair->state2 && transition->getInput() == *internalSymbol) {
-                        s.statesPairs.insert(StatesPair(statesPair->state1, transition->getTo()));
+                    if (transition->getFrom() == qDoublePrimed && transition->getInput() == *internalSymbol) {
+                        const State& qPrimed = transition->getTo();
+                        sPrimed.statesPairs.insert(StatesPair(q, qPrimed));
                     }
                 }
             }
-            RComponent r;
-            RComponent& oldR = unmarkedStateData->r;
-            for (set<State>::iterator state = oldR.states.begin();
-                    state != oldR.states.end();
-                    state++) {
+            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() == *state && transition->getInput() == *internalSymbol) {
-                        r.states.insert(transition->getTo());
+                    if (transition->getFrom() == *q && transition->getInput() == *internalSymbol) {
+                        const State& qPrimed = transition->getTo();
+                        rPrimed.states.insert(qPrimed);
                     }
                 }
             }
-            const State& toState = this->getOrCreateState(s, r);
+            const State& toState = this->getOrCreateState(sPrimed, rPrimed);
             const TransitionPDA transition(unmarkedStateData->state, *internalSymbol, toState);
             this->deterministicVPA->addTransition(transition);
         }
@@ -216,21 +223,21 @@ PDA* VPADeterminizer::determinize() {
         for (set<Symbol>::iterator callSymbol = this->callSymbols.begin();
                 callSymbol != this->callSymbols.end();
                 callSymbol++) {
-            RComponent r;
-            RComponent& oldR = unmarkedStateData->r;
-            for (set<State>::iterator state = oldR.states.begin();
-                    state != oldR.states.end();
-                    state++) {
+            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() == *state && transition->getInput() == *callSymbol) {
-                        r.states.insert(transition->getTo());
+                    if (transition->getFrom() == *q && transition->getInput() == *callSymbol) {
+                        const State& qPrimed = transition->getTo();
+                        rPrimed.states.insert(qPrimed);
                     }
                 }
             }
-            const State& toState = this->getOrCreateState(this->getSComponentWithStatesIdentity(), r);
-            string stackSymbolName = this->buildStackSymbolName(unmarkedStateData->s, unmarkedStateData->r, *callSymbol);
+            SComponent& s = unmarkedStateData->s;
+            const State& toState = this->getOrCreateState(this->getSComponentWithStatesIdentity(), rPrimed);
+            string stackSymbolName = this->buildStackSymbolName(s, r, *callSymbol);
             list<Symbol> pop;
             list<Symbol> push(1, Symbol(stackSymbolName));
             const TransitionPDA transition(unmarkedStateData->state, *callSymbol, toState, pop, push);
@@ -241,66 +248,68 @@ PDA* VPADeterminizer::determinize() {
         for (set<Symbol>::iterator returnSymbol = this->returnSymbols.begin();
                 returnSymbol != this->returnSymbols.end();
                 returnSymbol++) {
-            SComponent& oldS = unmarkedStateData->s;
-            RComponent& oldR = unmarkedStateData->r;
+            SComponent& s = unmarkedStateData->s;
+            RComponent& r = unmarkedStateData->r;
             
             // Empty stack
             list<Symbol> bottomOfStack(1, BOTTOM_OF_STACK_SYMBOL);
-            SComponent s;
-            for (set<StatesPair>::iterator statesPair = oldS.statesPairs.begin();
-                    statesPair != oldS.statesPairs.end();
+            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() == statesPair->state2 && transition->getInput() == *returnSymbol &&
+                    if (transition->getFrom() == qDoublePrimed && transition->getInput() == *returnSymbol &&
                             transition->getPop() == bottomOfStack) {
-                        s.statesPairs.insert(StatesPair(statesPair->state1, transition->getTo()));
+                        const State& qPrimed = transition->getTo();
+                        sPrimed.statesPairs.insert(StatesPair(q, qPrimed));
                     }
                 }
             }
-            RComponent r;
-            for (set<State>::iterator state = oldR.states.begin();
-                    state != oldR.states.end();
-                    state++) {
+            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() == *state && transition->getInput() == *returnSymbol &&
+                    if (transition->getFrom() == *q && transition->getInput() == *returnSymbol &&
                             transition->getPop() == bottomOfStack) {
-                        r.states.insert(transition->getTo());
+                        const State& qPrimed = transition->getTo();
+                        rPrimed.states.insert(qPrimed);
                     }
                 }
             }
-            if (r.states.size() != 0 || s.statesPairs.size() != 0) {
-                const State& toState = this->getOrCreateState(s, r);
-                list<Symbol> pop(1, BOTTOM_OF_STACK_SYMBOL);
-                list<Symbol> push;
-                const TransitionPDA transition(unmarkedStateData->state, *returnSymbol, toState, pop, push);
-                this->deterministicVPA->addTransition(transition);
-            }
+            const State& toState = this->getOrCreateState(sPrimed, rPrimed);
+            list<Symbol> pop(1, BOTTOM_OF_STACK_SYMBOL);
+            list<Symbol> push;
+            const TransitionPDA transition(unmarkedStateData->state, *returnSymbol, toState, pop, push);
+            this->deterministicVPA->addTransition(transition);
             
             // Otherwise
             for (set<Symbol>::iterator callSymbol = this->callSymbols.begin();
                     callSymbol != this->callSymbols.end();
                     callSymbol++) {
                 set<StatesPair> update;
-                for (set<StatesPair>::iterator oldSStatesPair = oldS.statesPairs.begin();
-                        oldSStatesPair != oldS.statesPairs.end();
-                        oldSStatesPair++) {
-                    if (oldR.states.find(oldSStatesPair->state2) != oldR.states.end()) {
-                        const State& state1 = oldSStatesPair->state1;
-                        const State& state2 = oldSStatesPair->state2;
+                for (set<StatesPair>::iterator sPair = s.statesPairs.begin();
+                        sPair != s.statesPairs.end();
+                        sPair++) {
+                    const State& q1 = sPair->state1;
+                    const State& q2 = sPair->state2;
+                    if (r.states.find(q2) != r.states.end()) {
                         for (set<TransitionPDA>::iterator transitionPush = transitions.begin();
                                 transitionPush != transitions.end();
                                 transitionPush++) {
                             for (set<TransitionPDA>::iterator transitionPop = transitions.begin();
                                     transitionPop != transitions.end();
                                     transitionPop++) {
-                                if (transitionPush->getInput() == *callSymbol && transitionPush->getTo() == state1 &&
-                                        transitionPop->getInput() == *returnSymbol && transitionPop->getFrom() == state2 &&
+                                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(transitionPush->getFrom(), transitionPop->getTo()));
+                                    update.insert(StatesPair(q, qPrimed));
                                 }
                             }
                         }
@@ -309,36 +318,41 @@ PDA* VPADeterminizer::determinize() {
                 if (update.size() == 0) {
                     continue;
                 }
-                
+
                 for (vector<PartialStackData>::iterator partialStackSymbol = this->partialStackAlphabet.begin();
                         partialStackSymbol != this->partialStackAlphabet.end();
                         partialStackSymbol++) {
-                    SComponent& stackS = partialStackSymbol->s;
-                    RComponent& stackR = partialStackSymbol->r;
-                    
-                    RComponent r;
-                    SComponent s;
+                    SComponent& sPrimed = partialStackSymbol->s;
+                    RComponent& rPrimed = partialStackSymbol->r;
+
+                    RComponent rDoublePrimed;
                     for (set<StatesPair>::iterator updateItem = update.begin();
                             updateItem != update.end();
                             updateItem++) {
-                        if (stackR.states.find(updateItem->state1) != stackR.states.end()) {
-                            r.states.insert(updateItem->state2);
+                        const State& q = updateItem->state1;
+                        const State& qPrimed = updateItem->state2;
+                        if (rPrimed.states.find(q) != rPrimed.states.end()) {
+                            rDoublePrimed.states.insert(qPrimed);
                         }
-                        for (set<StatesPair>::iterator stackSStatesPair = stackS.statesPairs.begin();
-                                stackSStatesPair != stackS.statesPairs.end();
-                                stackSStatesPair++) {
-                            if (stackSStatesPair->state2 == updateItem->state1) {
-                                s.statesPairs.insert(StatesPair(stackSStatesPair->state1, updateItem->state2));
+                    }
+                    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));
                             }
                         }
                     }
-                    
-                    if (r.states.size() == 0 && s.statesPairs.size() == 0) {
-                        continue;
-                    }
-                    
-                    const State& toState = this->getOrCreateState(s, r);
-                    string stackSymbolName = this->buildStackSymbolName(stackS, stackR, *callSymbol);
+
+                    const State& toState = this->getOrCreateState(sDoublePrimed, rDoublePrimed);
+                    string stackSymbolName = this->buildStackSymbolName(sPrimed, rPrimed, *callSymbol);
                     list<Symbol> pop(1, Symbol(stackSymbolName));
                     list<Symbol> push;
                     const TransitionPDA transition(unmarkedStateData->state, *returnSymbol, toState, pop, push);