/*
 * NFADeterminizer.cpp
 *
 *  Created on: 16. 1. 2014
 *	  Author: Jan Travnicek
 */

#include "common/RHDPDACommon.h"

#include <automaton/PDA/VisiblyPushdownNPDA.h>
#include <set>

namespace automaton {

namespace determinize {

void addRetTransition(const DefaultStateType& from, const DefaultSymbolType& input, const DefaultSymbolType& dvpdaSymbol, const DefaultStateType& to, automaton::VisiblyPushdownDPDA < > & deterministic) {
	deterministic.addState(from);
	deterministic.addState(to);
	deterministic.addPushdownStoreSymbol(dvpdaSymbol);

	deterministic.addReturnTransition(from, input, dvpdaSymbol, to);
}

void retInitial(const DefaultStateType& state, const DefaultSymbolType& pdaSymbol, const DefaultSymbolType& input, const automaton::VisiblyPushdownNPDA < > & nondeterministic, automaton::VisiblyPushdownDPDA < > & deterministic) {
	const ext::set<std::pair<DefaultStateType, DefaultStateType>> & S = unpackFromStateLabel(state);

	ext::set<std::pair<DefaultStateType, DefaultStateType>> S1;
	for(const auto& entry : S) {
		const DefaultStateType& q = entry.first;
		const DefaultStateType& q2 = entry.second;

		for(const auto& transition : nondeterministic.getReturnTransitions()) {
			if(q2 != std::get<0>(transition.first)) continue;
			if(input != std::get<1>(transition.first)) continue;
			if(nondeterministic.getBottomOfTheStackSymbol() != std::get<2>(transition.first)) continue;

			for(const auto& to : transition.second) {
				const DefaultStateType& q1 = to;
				S1.insert(std::make_pair(q, q1));
			}
		}
	}

	addRetTransition(state, input, pdaSymbol, DefaultStateType(packToStateLabel(std::move(S1))), deterministic);
}

void ret(const DefaultStateType& state, const DefaultSymbolType& pdaSymbol, const DefaultSymbolType& input, const automaton::VisiblyPushdownNPDA < > & nondeterministic, automaton::VisiblyPushdownDPDA < > & deterministic) {
	const ext::set<std::pair<DefaultStateType, DefaultStateType>> & S = unpackFromStateLabel(state);
	const std::pair<DefaultStateType, DefaultSymbolType> & pdaSymbolUnpack = unpackFromDVPAStackSymbol(pdaSymbol);
	const ext::set<std::pair<DefaultStateType, DefaultStateType>>& S1 = unpackFromStateLabel ( pdaSymbolUnpack.first );

	ext::set<std::pair<DefaultStateType, DefaultStateType>> update;

	for(const auto& transition : nondeterministic.getCallTransitions()) {
		if(pdaSymbolUnpack.second != std::get<1>(transition.first)) continue;

		const DefaultStateType& q = std::get<0>(transition.first);
		for(const auto& to : transition.second) {
			const DefaultStateType& q1 = to.first;
			const DefaultSymbolType& gamma = to.second;

			for(const auto& entry : S) {
				if(q1 != entry.first) continue;
				const DefaultStateType& q2 = entry.second;

				for(const auto& transition2 : nondeterministic.getReturnTransitions()) {
					if(q2 != std::get<0>(transition2.first)) continue;
					if(input != std::get<1>(transition2.first)) continue;
					if(gamma != std::get<2>(transition2.first)) continue;

					for(const auto& to2 : transition2.second) {
						const DefaultStateType& qI = to2;

						update.insert(std::make_pair(q, qI));
					}
				}
			}
		}
	}

	ext::set<std::pair<DefaultStateType, DefaultStateType>> S2;
	for(const auto& entry : S1) {
		const DefaultStateType& q = entry.first;
		const DefaultStateType& q3 = entry.second;
		for(const auto& entry2 : update) {
			if(q3 != entry2.first) continue;

			const DefaultStateType& qI = entry2.second;

			S2.insert(std::make_pair(q, qI));
		}
	}

	addRetTransition(state, input, pdaSymbol, DefaultStateType(packToStateLabel(std::move(S2))), deterministic);
}

void addCallTransition(const DefaultStateType& from, const DefaultSymbolType& input, const DefaultStateType& to, const DefaultSymbolType& dvpdaSymbol, automaton::VisiblyPushdownDPDA < > & deterministic) {
	deterministic.addState(from);
	deterministic.addState(to);
	deterministic.addPushdownStoreSymbol(dvpdaSymbol);

	deterministic.addCallTransition(from, input, to, dvpdaSymbol);
}

void call(const DefaultStateType& state, const DefaultSymbolType& input, const automaton::VisiblyPushdownNPDA < > & nondeterministic, automaton::VisiblyPushdownDPDA < > & deterministic) {
	const ext::set<std::pair<DefaultStateType, DefaultStateType>> & S = unpackFromStateLabel(state);

	ext::set<DefaultStateType> R = retrieveDSubSet(S);
	ext::set<DefaultStateType> R1;

	for(const DefaultStateType& q : R) {
		for(const auto& transition : nondeterministic.getCallTransitions()) {
			if(q != transition.first.first) continue;
			if(input != transition.first.second) continue;

			for(const auto& to : transition.second) {
				const DefaultStateType& q1 = to.first;

				R1.insert(q1);
			}
		}
	}

	addCallTransition(state, input, DefaultStateType(packToStateLabel(createIdentity(std::move(R1)))), packToStackSymbolLabel(std::make_pair(state, input)), deterministic);
}

void addLocalTransition(const DefaultStateType& from, const DefaultSymbolType& input, const DefaultStateType& to, automaton::VisiblyPushdownDPDA < > & deterministic) {
	deterministic.addState(from);
	deterministic.addState(to);

	deterministic.addLocalTransition(from, input, to);
}

void local(const DefaultStateType& state, const DefaultSymbolType& input, const automaton::VisiblyPushdownNPDA < > & nondeterministic, automaton::VisiblyPushdownDPDA < > & deterministic) {
	const ext::set<std::pair<DefaultStateType, DefaultStateType>> & S = unpackFromStateLabel(state);
	ext::set<std::pair<DefaultStateType, DefaultStateType>> S1;

	for(const auto& entry : S) {
		const DefaultStateType & q = entry.first;
		const DefaultStateType & q2 = entry.second;
		for(const auto& transition : nondeterministic.getLocalTransitions()) {
			if(q2 != transition.first.first) continue;
			if(input != transition.first.second) continue;

			for(const auto& to : transition.second) {
				const DefaultStateType & q1 = to;

				S1.insert(std::make_pair(q, q1));
			}
		}
	}

	addLocalTransition(state, input, DefaultStateType(packToStateLabel(std::move(S1))), deterministic);
}

automaton::VisiblyPushdownDPDA < > Determinize::determinize(const automaton::VisiblyPushdownNPDA < > & n) {
	DefaultStateType initialLabel = packToStateLabel(createIdentity(n.getInitialStates()));

	automaton::VisiblyPushdownDPDA < > d(initialLabel, n.getBottomOfTheStackSymbol());
	d.setCallInputAlphabet(n.getCallInputAlphabet());
	d.setLocalInputAlphabet(n.getLocalInputAlphabet());
	d.setReturnInputAlphabet(n.getReturnInputAlphabet());

	ext::set<DefaultStateType> rubbishStates = {DefaultStateType(packToStateLabel({}))};
	ext::map<ext::tuple<DefaultStateType, DefaultSymbolType, DefaultSymbolType>, DefaultStateType> rubbishReturnTransitions;
	ext::map<std::pair<DefaultStateType, DefaultSymbolType>, std::pair<DefaultStateType, DefaultSymbolType> > rubbishCallTransitions;
	ext::map<std::pair<DefaultStateType, DefaultSymbolType>, DefaultStateType> rubbishLocalTransitions;

	for(;;) {
		ext::set<std::pair<DefaultStateType, DefaultSymbolType>> stateSymbols = existsDirtyStateSymbol(d, rubbishStates, rubbishCallTransitions, rubbishReturnTransitions, n);
		ext::set<DefaultStateType> states = existsDirtyState(d, rubbishStates, rubbishCallTransitions, rubbishLocalTransitions, n);

		if(stateSymbols.empty() && states.empty()) break;

		for(const auto& stateSymbol: stateSymbols) {
			for(const DefaultSymbolType& symbol : n.getReturnInputAlphabet()) {
				if(stateSymbol.second == d.getBottomOfTheStackSymbol()) {
					retInitial(stateSymbol.first, stateSymbol.second, symbol, n, d);
				} else {
					ret(stateSymbol.first, stateSymbol.second, symbol, n, d);
				}
			}
		}

		for(const auto& state : states) {
			for(const DefaultSymbolType& symbol : n.getLocalInputAlphabet()) {
				local(state, symbol, n, d);
			}
			for(const DefaultSymbolType& symbol : n.getCallInputAlphabet()) {
				call(state, symbol, n, d);
			}
		}
	}

	const ext::set<DefaultStateType>& finalLabels = n.getFinalStates();
	for(const DefaultStateType& state : d.getStates()) {
		const ext::set<DefaultStateType> labels = retrieveDSubSet(unpackFromStateLabel(state));

		if(!ext::excludes(finalLabels.begin(), finalLabels.end(), labels.begin(), labels.end())) {
			d.addFinalState(state);
		}
	}

	return d;
}

auto DeterminizeVisiblyPushdownNPDA = registration::OverloadRegister < Determinize, automaton::VisiblyPushdownDPDA < >, automaton::VisiblyPushdownNPDA < > > ( Determinize::determinize );
auto DeterminizeVisiblyPushdownNPDA2 = registration::AbstractRegister < Determinize, automaton::VisiblyPushdownDPDA < >, const automaton::VisiblyPushdownNPDA < > & > ( Determinize::determinize );

} /* namespace determinize */

} /* namespace automaton */