DeterminizeVPAPart.cxx

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

#include "common/RHDPDACommon.h"

#include <automaton/PDA/VisiblyPushdownNPDA.h>
#include "automaton/common/State.h"
#include "alphabet/Symbol.h"
#include "alphabet/LabeledSymbol.h"
#include "label/Label.h"
#include <set>

namespace automaton {

namespace determinize {

void addRetTransition(const automaton::State& from, const alphabet::Symbol& input, const alphabet::Symbol& dvpdaSymbol, const automaton::State& to, automaton::VisiblyPushdownDPDA& deterministic) {
	deterministic.addState(from);
	deterministic.addState(to);
	deterministic.addStackSymbol(dvpdaSymbol);

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

void retInitial(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const alphabet::Symbol& input, const automaton::VisiblyPushdownNPDA& nondeterministic, automaton::VisiblyPushdownDPDA& deterministic) {
	std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());

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

		for(const auto& transition : nondeterministic.getReturnTransitions()) {
			if(q2 != std::get<0>(transition.first).getName()) 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 label::Label& q1 = to.getName();
				S1.insert(std::make_pair(q, q1));
			}
		}
	}

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

void ret(const automaton::State& state, const alphabet::Symbol& pdaSymbol, const alphabet::Symbol& input, const automaton::VisiblyPushdownNPDA& nondeterministic, automaton::VisiblyPushdownDPDA& deterministic) {
	std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
	std::pair<std::set<std::pair<label::Label, label::Label>>, alphabet::Symbol> pdaSymbolUnpack = unpackFromDVPAStackSymbol(pdaSymbol);
	const std::set<std::pair<label::Label, label::Label>>& S1 = pdaSymbolUnpack.first;

	std::set<std::pair<label::Label, label::Label>> update;

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

		const label::Label& q = std::get<0>(transition.first).getName();
		for(const auto& to : transition.second) {
			const label::Label q1 = to.first.getName();
			const alphabet::Symbol& gamma = to.second;

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

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

					for(const auto& to2 : transition2.second) {
						const label::Label& qI = to2.getName();

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

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

			const label::Label& qI = entry2.second;

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

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

void addCallTransition(const automaton::State& from, const alphabet::Symbol& input, const automaton::State& to, const alphabet::Symbol& dvpdaSymbol, automaton::VisiblyPushdownDPDA& deterministic) {
	deterministic.addState(from);
	deterministic.addState(to);
	deterministic.addStackSymbol(dvpdaSymbol);

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

void call(const automaton::State& state, const alphabet::Symbol& input, const automaton::VisiblyPushdownNPDA& nondeterministic, automaton::VisiblyPushdownDPDA& deterministic) {
	std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());

	std::set<label::Label> R = retrieveDSubSet(S);
	std::set<label::Label> R1;

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

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

				R1.insert(q1);
			}
		}
	}

	addCallTransition(state, input, automaton::State(packToStateLabel(createIdentity(std::move(R1)))), alphabet::Symbol(alphabet::LabeledSymbol(packToStackSymbolLabel(std::make_pair(std::move(S), input)))), deterministic);
}

void addLocalTransition(const automaton::State& from, const alphabet::Symbol& input, const automaton::State& to, automaton::VisiblyPushdownDPDA& deterministic) {
	deterministic.addState(from);
	deterministic.addState(to);

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

void local(const automaton::State& state, const alphabet::Symbol& input, const automaton::VisiblyPushdownNPDA& nondeterministic, automaton::VisiblyPushdownDPDA& deterministic) {
	std::set<std::pair<label::Label, label::Label>> S = unpackFromStateLabel(state.getName());
	std::set<std::pair<label::Label, label::Label>> S1;

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

			for(const auto& to : transition.second) {
				label::Label q1 = to.getName();

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

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

automaton::VisiblyPushdownDPDA Determinize::determinize(const automaton::VisiblyPushdownNPDA& n) {
	label::Label initialLabel = packToStateLabel(createIdentity(retrieveLabels(n.getInitialStates())));

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

	std::set<automaton::State> rubbishStates = {automaton::State(packToStateLabel({}))};
	std::map<std::tuple<State, alphabet::Symbol, alphabet::Symbol>, State> rubbishReturnTransitions;
	std::map<std::pair<State, alphabet::Symbol>, std::pair<State, alphabet::Symbol> > rubbishCallTransitions;
	std::map<std::pair<State, alphabet::Symbol>, State> rubbishLocalTransitions;

	for(;;) {
		std::set<std::pair<automaton::State, alphabet::Symbol>> stateSymbols = existsDirtyStateSymbol(d, rubbishStates, rubbishCallTransitions, rubbishReturnTransitions, n);
		std::set<automaton::State> states = existsDirtyState(d, rubbishStates, rubbishCallTransitions, rubbishLocalTransitions, n);

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

		for(const auto& stateSymbol: stateSymbols) {
			for(const alphabet::Symbol& 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 alphabet::Symbol& symbol : n.getLocalInputAlphabet()) {
				local(state, symbol, n, d);
			}
			for(const alphabet::Symbol& symbol : n.getCallInputAlphabet()) {
				call(state, symbol, n, d);
			}
		}
	}

	std::set<label::Label> finalLabels = retrieveLabels(n.getFinalStates());
	for(const automaton::State& state : d.getStates()) {
		const std::set<label::Label> labels = retrieveDSubSet(unpackFromStateLabel(state.getName()));

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

	return d;
}

auto DeterminizeVisiblyPushdownNPDA = Determinize::RegistratorWrapper<automaton::VisiblyPushdownDPDA, automaton::VisiblyPushdownNPDA>(Determinize::getInstance(), Determinize::determinize);

} /* namespace determinize */

} /* namespace automaton */