/*
 * NFADeterminizer.h
 *
 *  Created on: 16. 1. 2014
 *	  Author: Jan Vesely
 */

#ifndef DETERMINIZE_H_
#define DETERMINIZE_H_

#include <set>

#include <automaton/common/State.h>
#include <automaton/Automaton.h>
#include <automaton/FSM/DFA.h>
#include <automaton/PDA/DPDA.h>
#include <automaton/PDA/VisiblyPushdownDPDA.h>
#include <automaton/PDA/RealTimeHeightDeterministicDPDA.h>

#include <exception/AlibException.h>

namespace automaton {

namespace determinize {

/**
 * Class for running determinization algorithm on fsm.
 */
class Determinize : public automaton::VisitableAutomatonBase::const_visitor_type {
private:
	void Visit(void*, const automaton::EpsilonNFA& automaton) const;
	void Visit(void*, const automaton::MultiInitialStateNFA& automaton) const;
	void Visit(void*, const automaton::NFA& automaton) const;
	void Visit(void*, const automaton::DFA& automaton) const;
	void Visit(void*, const automaton::ExtendedNFA& automaton) const;
	void Visit(void*, const automaton::CompactNFA& automaton) const;
	void Visit(void*, const automaton::DPDA& automaton) const;
	void Visit(void*, const automaton::SinglePopDPDA& automaton) const;
	void Visit(void*, const automaton::InputDrivenNPDA& automaton) const;
	void Visit(void*, const automaton::VisiblyPushdownDPDA& automaton) const;
	void Visit(void*, const automaton::VisiblyPushdownNPDA& automaton) const;
	void Visit(void*, const automaton::RealTimeHeightDeterministicDPDA& automaton) const;
	void Visit(void*, const automaton::RealTimeHeightDeterministicNPDA& automaton) const;
	void Visit(void*, const automaton::NPDA& automaton) const;
	void Visit(void*, const automaton::SinglePopNPDA& automaton) const;
	void Visit(void*, const automaton::OneTapeDTM& automaton) const;

	static const Determinize DETERMINIZE;

public:

	/**
	 * @param nfsm nondeterministic final-state machine given for determinization
	 * @return DFA
	 * Runs determinization algorithm on nondeterministic fsm given in constructor.
	 */
	static automaton::Automaton determinize(const automaton::Automaton& nfa);

	static automaton::DFA determinize(const automaton::NFA& nfa);
	static automaton::DFA determinize(const automaton::MultiInitialStateNFA& nfa);
	static automaton::VisiblyPushdownDPDA determinize(const automaton::VisiblyPushdownNPDA& nondeterministic);
	static automaton::DPDA determinize(const automaton::InputDrivenNPDA& nfa);
	static automaton::RealTimeHeightDeterministicDPDA determinize(const automaton::RealTimeHeightDeterministicNPDA& nondeterministic);
};

} /* namespace determinize */

} /* namespace automaton */

#endif /* DETERMINIZE_H_ */