/*
 * IDPDADeterminizer.cpp
 *
 *  Created on: 16. 1. 2014
 *	  Author: Jan Vesely
 */

#include "common/NFACommon.h"

#include <automaton/PDA/InputDrivenNPDA.h>
#include <deque>
#include <algorithm>

namespace automaton {

namespace determinize {

automaton::DPDA Determinize::determinize(const automaton::InputDrivenNPDA& nfa) {
	// 1, 4
	automaton::State initialState(createDFAState({nfa.getInitialState()}));
	automaton::DPDA res(initialState, nfa.getInitialSymbol());
	res.setInputSymbols(nfa.getInputAlphabet());
	res.setStackSymbols(nfa.getStackAlphabet());
	
	// 2
	std::deque<automaton::State> todo;
	todo.push_back(initialState);
	
	do {
		// 3a, c
		automaton::State state = todo.front();
		todo.pop_front();

		// 3b
		for (const auto& input : nfa.getInputAlphabet()) {
			std::set<automaton::State> targetIDPDAStates;
			for(const auto& nfaState : recreateNFAStates(state)) {
				auto iter = nfa.getTransitions().find(std::make_pair(nfaState, input));
				if(iter != nfa.getTransitions().end()) {
					targetIDPDAStates.insert(iter->second.begin(), iter->second.end());
				}
			}
			automaton::State dfaState = createDFAState(targetIDPDAStates);

			// 4
			bool existed = !res.addState(dfaState);

			// 3b
			const auto& pushdownOperation = nfa.getPushdownStoreOperations().find(input)->second;
			res.addTransition(state, input, pushdownOperation.first, dfaState, pushdownOperation.second);

			if(!existed) todo.push_back(dfaState);
		}
	} while(!todo.empty());
	
	// 5
	for (const auto& dfaState : res.getStates()) {
		std::set<automaton::State> nfaStates = recreateNFAStates(dfaState);
		if(std::any_of(nfaStates.begin(), nfaStates.end(), [&](const automaton::State& nfaState) { return nfa.getFinalStates().count(nfaState); })) {
			res.addFinalState(dfaState);
		}
	}
	
	return res;
}

} /* namespace determinize */

} /* namespace automaton */