/*
 * INPUT_DRIVEN_DPDA.h
 *
 *  Created on: Mar 25, 2013
 *      Author: Jan Travnicek
 */

#ifndef INPUT_DRIVEN_DPDA_H_
#define INPUT_DRIVEN_DPDA_H_

#include <map>
#include <vector>
#include <ostream>
#include <sstream>
#include <algorithm>

#include <core/components.hpp>
#include <sax/FromXMLParserHelper.h>
#include <object/UniqueObject.h>

#include "../AutomatonBase.h"
#include "../AutomatonFeatures.h"
#include "../AutomatonException.h"
#include "../common/AutomatonFromXMLParser.h"
#include "../common/AutomatonToXMLComposer.h"

namespace automaton {

class InputAlphabet;
class PushdownStoreAlphabet;
class InitialSymbol;
class States;
class FinalStates;
class InitialState;

/**
 * Represents Finite Automaton.
 * Can store nondeterministic finite automaton without epsilon transitions.
 */
template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
class InputDrivenDPDA : public AutomatonBase, public std::Components < InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >, InputSymbolType, std::tuple < InputAlphabet >, std::tuple < >, PushdownStoreSymbolType, std::tuple < PushdownStoreAlphabet >, std::tuple < InitialSymbol >, StateType, std::tuple < States, FinalStates >, std::tuple < InitialState > > {
protected:
	std::map < std::pair < StateType, InputSymbolType >, StateType > transitions;
	std::map < InputSymbolType, std::pair < std::vector < PushdownStoreSymbolType >, std::vector < PushdownStoreSymbolType > > > inputSymbolToPushdownStoreOperation;

	void checkPushdownStoreOperation ( const InputSymbolType & input, const std::vector < PushdownStoreSymbolType > & pop, const std::vector < PushdownStoreSymbolType > & push );

public:
	explicit InputDrivenDPDA ( std::set < StateType > states, std::set < InputSymbolType > inputAlphabet, std::set < PushdownStoreSymbolType > pushdownStoreSymbol, StateType initialState, PushdownStoreSymbolType initialPushdownSymbol, std::set < StateType > finalStates );
	explicit InputDrivenDPDA ( StateType initialState, PushdownStoreSymbolType initialPushdownSymbol );

	virtual AutomatonBase * clone ( ) const;

	virtual AutomatonBase * plunder ( ) &&;

	const StateType & getInitialState ( ) const {
		return this->template accessElement < InitialState > ( ).get ( );
	}

	bool setInitialState ( StateType state ) {
		return this->template accessElement < InitialState > ( ).set ( std::move ( state ) );
	}

	const std::set < StateType > & getStates ( ) const {
		return this->template accessComponent < States > ( ).get ( );
	}

	bool addState ( StateType state ) {
		return this->template accessComponent < States > ( ).add ( std::move ( state ) );
	}

	void setStates ( std::set < StateType > states ) {
		this->template accessComponent < States > ( ).set ( std::move ( states ) );
	}

	void removeState ( const StateType & state ) {
		this->template accessComponent < States > ( ).remove ( state );
	}

	const std::set < StateType > & getFinalStates ( ) const {
		return this->template accessComponent < FinalStates > ( ).get ( );
	}

	bool addFinalState ( StateType state ) {
		return this->template accessComponent < FinalStates > ( ).add ( std::move ( state ) );
	}

	void setFinalStates ( std::set < StateType > states ) {
		this->template accessComponent < FinalStates > ( ).set ( std::move ( states ) );
	}

	void removeFinalState ( const StateType & state ) {
		this->template accessComponent < FinalStates > ( ).remove ( state );
	}

	const std::set < PushdownStoreSymbolType > & getPushdownStoreAlphabet ( ) const {
		return this->template accessComponent < PushdownStoreAlphabet > ( ).get ( );
	}

	bool addPushdownStoreSymbol ( PushdownStoreSymbolType symbol ) {
		return this->template accessComponent < PushdownStoreAlphabet > ( ).add ( std::move ( symbol ) );
	}

	void addPushdownStoreSymbols ( std::set < PushdownStoreSymbolType > symbols ) {
		this->template accessComponent < PushdownStoreAlphabet > ( ).add ( std::move ( symbols ) );
	}

	void setPushdownStoreAlphabet ( std::set < PushdownStoreSymbolType > symbols ) {
		this->template accessComponent < PushdownStoreAlphabet > ( ).set ( std::move ( symbols ) );
	}

	void removePushdownStoreSymbol ( const PushdownStoreSymbolType & symbol ) {
		this->template accessComponent < PushdownStoreAlphabet > ( ).remove ( symbol );
	}

	const PushdownStoreSymbolType & getInitialSymbol ( ) const {
		return this->template accessElement < InitialSymbol > ( ).get ( );
	}

	bool setInitialSymbol ( PushdownStoreSymbolType symbol ) {
		return this->template accessElement < InitialSymbol > ( ).set ( std::move ( symbol ) );
	}

	const std::set < InputSymbolType > & getInputAlphabet ( ) const {
		return this->template accessComponent < InputAlphabet > ( ).get ( );
	}

	bool addInputSymbol ( InputSymbolType symbol ) {
		return this->template accessComponent < InputAlphabet > ( ).add ( std::move ( symbol ) );
	}

	void addInputSymbols ( std::set < InputSymbolType > symbols ) {
		this->template accessComponent < InputAlphabet > ( ).add ( std::move ( symbols ) );
	}

	void setInputAlphabet ( std::set < InputSymbolType > symbols ) {
		this->template accessComponent < InputAlphabet > ( ).set ( std::move ( symbols ) );
	}

	void removeInputSymbol ( const InputSymbolType & symbol ) {
		this->template accessComponent < InputAlphabet > ( ).remove ( symbol );
	}

	bool setPushdownStoreOperation ( InputSymbolType input, std::vector < PushdownStoreSymbolType > pop, std::vector < PushdownStoreSymbolType > push );

	void setPushdownStoreOperations ( std::map < InputSymbolType, std::pair < std::vector < PushdownStoreSymbolType >, std::vector < PushdownStoreSymbolType > > > operations );

	bool clearPushdownStoreOperation ( const InputSymbolType & input );

	const std::map < InputSymbolType, std::pair < std::vector < PushdownStoreSymbolType >, std::vector < PushdownStoreSymbolType > > > & getPushdownStoreOperations ( ) const;

	/**
	 * Adds transition defined by parameters to the automaton.
	 * @param current current state
	 * @param input input symbol
	 * @param next next state
	 * @throws AutomatonException when transition already exists or when transition contains state or symbol not present in the automaton
	 */
	bool addTransition ( StateType current, InputSymbolType input, StateType next );

	/**
	 * Removes transition from the automaton.
	 * @param transition transition to remove
	 * @throws AutomatonException when transition doesn't exists.
	 */
	bool removeTransition ( const StateType & current, const InputSymbolType & input, const StateType & next );

	/**
	 * @return automaton transitions
	 */
	const std::map < std::pair < StateType, InputSymbolType >, StateType > & getTransitions ( ) const;

	std::map < std::pair < StateType, InputSymbolType >, StateType > getTransitionsFromState ( const StateType & from ) const;

	std::map < std::pair < StateType, InputSymbolType >, StateType > getTransitionsToState ( const StateType & to ) const;

	/**
	 * Determines whether InputDrivenDPDA is deterministic.
	 * FA is deterministic if and only if:
	 * \li \c contains only 1 initial state.
	 * \li \c is epsilon free. Trivial for this class
	 * \li \c size of transition function \delta (from state, input symbol) \leq 1
	 * @return true when automaton is deterministic, false otherwise
	 */
	bool isDeterministic ( ) const;

	virtual int compare ( const ObjectBase & other ) const {
		if ( std::type_index ( typeid ( * this ) ) == std::type_index ( typeid ( other ) ) ) return this->compare ( ( decltype ( * this ) )other );

		return std::type_index ( typeid ( * this ) ) - std::type_index ( typeid ( other ) );
	}

	virtual int compare ( const InputDrivenDPDA & other ) const;

	virtual void operator >>( std::ostream & os ) const;

	virtual explicit operator std::string ( ) const;

	static const std::string & getXmlTagName() {
		static std::string xmlTagName = "InputDrivenDPDA";

		return xmlTagName;
	}

	static InputDrivenDPDA parse ( std::deque < sax::Token >::iterator & input );
	static void parseTransition ( std::deque < sax::Token >::iterator & input, InputDrivenDPDA & automaton );

	void compose ( std::deque < sax::Token > & out ) const;
	void composeTransitions ( std::deque < sax::Token > & out ) const;

	virtual alib::ObjectBase * inc ( ) &&;
};

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::InputDrivenDPDA ( std::set < StateType > states, std::set < InputSymbolType > inputAlphabet, std::set < PushdownStoreSymbolType > pushdownStoreAlphabet, StateType initialState, PushdownStoreSymbolType initialSymbol, std::set < StateType > finalStates ) : std::Components < InputDrivenDPDA, InputSymbolType, std::tuple < InputAlphabet >, std::tuple < >, PushdownStoreSymbolType, std::tuple < PushdownStoreAlphabet >, std::tuple < InitialSymbol >, StateType, std::tuple < States, FinalStates >, std::tuple < InitialState > > ( std::make_tuple ( std::move ( inputAlphabet ) ), std::tuple < > ( ), std::make_tuple ( std::move ( pushdownStoreAlphabet ) ), std::make_tuple ( std::move ( initialSymbol ) ), std::make_tuple ( std::move ( states ), std::move ( finalStates ) ), std::make_tuple ( std::move ( initialState ) ) ) {
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::InputDrivenDPDA ( StateType initialState, PushdownStoreSymbolType initialPushdownSymbol) : InputDrivenDPDA ( std::set < StateType > { initialState }, std::set < InputSymbolType > { }, std::set < PushdownStoreSymbolType > { initialPushdownSymbol }, initialState, initialPushdownSymbol, std::set < StateType > { }) {
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
AutomatonBase* InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::clone() const {
	return new InputDrivenDPDA(*this);
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
AutomatonBase* InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::plunder() && {
	return new InputDrivenDPDA(std::move(*this));
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::checkPushdownStoreOperation(const InputSymbolType& input, const std::vector<PushdownStoreSymbolType>& pop, const std::vector<PushdownStoreSymbolType>& push) {
	if (! getInputAlphabet().count(input)) {
		throw AutomatonException("Input symbol \"" + std::to_string ( input ) + "\" doesn't exist.");
	}

	for(const PushdownStoreSymbolType& popSymbol : pop) {
		if (! getPushdownStoreAlphabet().count(popSymbol)) {
			throw AutomatonException("Pushdown store symbol \"" + std::to_string ( popSymbol ) + "\" doesn't exist.");
		}
	}

	for(const PushdownStoreSymbolType& pushSymbol : push) {
		if (! getPushdownStoreAlphabet().count(pushSymbol)) {
			throw AutomatonException("Pushdown store symbol \"" + std::to_string ( pushSymbol ) + "\" doesn't exist.");
		}
	}
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
bool InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::setPushdownStoreOperation ( InputSymbolType input, std::vector<PushdownStoreSymbolType> pop, std::vector<PushdownStoreSymbolType> push) {
	checkPushdownStoreOperation(input, pop, push);
	return inputSymbolToPushdownStoreOperation.insert(std::make_pair(std::move(input), std::make_pair(std::move(pop), std::move(push)))).second;
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::setPushdownStoreOperations(std::map<InputSymbolType, std::pair<std::vector<PushdownStoreSymbolType>, std::vector<PushdownStoreSymbolType>>> operations) {
	std::set<InputSymbolType> removed;
	std::set_difference(getInputAlphabet().begin(), getInputAlphabet().end(), key_begin(operations), key_end(operations), std::inserter(removed, removed.end()));

	for(const InputSymbolType& removedSymbol : removed) {
		clearPushdownStoreOperation(removedSymbol);
	}

	for(const auto& added : operations) {
		checkPushdownStoreOperation(added.first, added.second.first, added.second.second);
	}

	inputSymbolToPushdownStoreOperation = std::move(operations);
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
bool InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::clearPushdownStoreOperation(const InputSymbolType& input) {
	for (const std::pair<const std::pair<StateType, InputSymbolType>, StateType>& transition : transitions) {
		if (transition.first.second == input)
			throw AutomatonException("Input symbol \"" + std::to_string ( input ) + "\" is used.");
	}

	return inputSymbolToPushdownStoreOperation.erase(input);
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
const std::map < InputSymbolType, std::pair<std::vector<PushdownStoreSymbolType>, std::vector<PushdownStoreSymbolType>>>& InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::getPushdownStoreOperations() const {
	return inputSymbolToPushdownStoreOperation;
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
bool InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::addTransition(StateType from, InputSymbolType input, StateType to) {
	if (!getStates().count(from))
		throw AutomatonException("State \"" + std::to_string ( from ) + "\" doesn't exist.");

	if (!getInputAlphabet().count(input))
		throw AutomatonException("Input symbol \"" + std::to_string ( input ) + "\" doesn't exist.");

	if (! getPushdownStoreOperations().count(input))
		throw AutomatonException("Input symbol \"" + std::to_string ( input ) + "\" doesn't exist.");

	if (! getStates().count(to))
		throw AutomatonException("State \"" + std::to_string ( to ) + "\" doesn't exist.");

	std::pair<StateType, InputSymbolType> key = std::make_pair(std::move(from), std::move(input));

	if (transitions.find(key) != transitions.end()) {
		if(transitions.find(key)->second == to)
			return false;
		else
			throw AutomatonException( "Transition from this state and symbol already exists (\"" + std::to_string ( key.first ) + "\", \"" + std::to_string ( key.second ) + "\") -> \"" + std::to_string ( to ) + "\"." );
	}

	transitions.insert(std::make_pair(std::move(key), std::move(to)));
	return true;
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
bool InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::removeTransition(const StateType& from, const InputSymbolType& input, const StateType& to) {
	std::pair<StateType, InputSymbolType> key = std::make_pair(from, input);

	if (transitions.find(key) == transitions.end())
		return false;

	if(transitions.find(key)->second != to)
		throw AutomatonException( "Transition (\"" + std::to_string ( from ) + "\", \"" + std::to_string ( input ) + "\") -> \"" + std::to_string ( to ) + "\" doesn't exist.");

	transitions.erase(key);
	return true;
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
const std::map<std::pair<StateType, InputSymbolType>, StateType>& InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::getTransitions() const {
	return transitions;
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
std::map<std::pair<StateType, InputSymbolType>, StateType > InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::getTransitionsFromState(const StateType& from) const {
	if( ! getStates().count(from))
		throw AutomatonException("State \"" + std::to_string ( from ) + "\" doesn't exist");

	std::map<std::pair<StateType, InputSymbolType>, StateType> transitionsFromState;
	for (const std::pair<const std::pair<StateType, InputSymbolType>, StateType>& transition : transitions) {
		if (transition.first.first == from) {
			transitionsFromState.insert(transition);
		}
	}

	return transitionsFromState;
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
std::map<std::pair<StateType, InputSymbolType>, StateType> InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::getTransitionsToState(const StateType& to) const {
	if( ! getStates().count(to))
		throw AutomatonException("State \"" + std::to_string ( to ) + "\" doesn't exist");

	std::map<std::pair<StateType, InputSymbolType>, StateType> transitionsToState;
	for (const std::pair<const std::pair<StateType, InputSymbolType>, StateType>& transition : transitions) {
		if (transition.second == to) {
			transitionsToState.insert(transition);
		}
	}

	return transitionsToState;
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
int InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::compare(const InputDrivenDPDA& other) const {
	auto first = std::tie(getStates(), getInputAlphabet(), getInitialState(), getFinalStates(), getPushdownStoreAlphabet(), getInitialSymbol(), getPushdownStoreOperations(), transitions);
	auto second = std::tie(other.getStates(), other.getInputAlphabet(), other.getInitialState(), other.getFinalStates(), other.getPushdownStoreAlphabet(), other.getInitialSymbol(), other.getPushdownStoreOperations(), other.transitions);

	static std::compare<decltype(first)> comp;
	return comp(first, second);
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::operator>>(std::ostream& out) const {
	out << "(InputDrivenDPDA "
		<< " states = " << getStates()
		<< " inputAlphabet = " << getInputAlphabet()
		<< " initialState = " << getInitialState()
		<< " finalStates = " << getFinalStates()
		<< " pushdownStoreAlphabet = " << getPushdownStoreAlphabet()
		<< " initialSymbol = " << getInitialSymbol()
		<< " transitions = " << transitions
		<< " inputSymbolToPushdownStoreOperation = " << getPushdownStoreOperations()
		<< ")";
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::operator std::string () const {
	std::stringstream ss;
	ss << *this;
	return ss.str();
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::parse(std::deque<sax::Token>::iterator& input) {
	sax::FromXMLParserHelper::popToken(input, sax::Token::TokenType::START_ELEMENT, InputDrivenDPDA::getXmlTagName());

	std::set<StateType> states = AutomatonFromXMLParser::parseStates<StateType>(input);
	std::set<InputSymbolType> inputSymbols = AutomatonFromXMLParser::parseInputAlphabet<InputSymbolType>(input);
	std::set<PushdownStoreSymbolType> pushdownStoreSymbols = AutomatonFromXMLParser::parsePushdownStoreAlphabet<PushdownStoreSymbolType>(input);
	StateType initialState = AutomatonFromXMLParser::parseInitialState<StateType>(input);
	PushdownStoreSymbolType initialPushdownStoreSymbol = AutomatonFromXMLParser::parseInitialPushdownStoreSymbol<PushdownStoreSymbolType>(input);
	std::set<StateType> finalStates = AutomatonFromXMLParser::parseFinalStates<StateType>(input);

	InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > automaton(std::move(initialState), std::move(initialPushdownStoreSymbol));
	automaton.setStates(std::move(states));
	automaton.setInputAlphabet(std::move(inputSymbols));
	automaton.setPushdownStoreAlphabet(std::move(pushdownStoreSymbols));
	automaton.setFinalStates(std::move(finalStates));

	automaton.setPushdownStoreOperations(AutomatonFromXMLParser::parseInputToPushdownStoreOperation<InputSymbolType, PushdownStoreSymbolType>(input));
	AutomatonFromXMLParser::parseTransitions<InputDrivenDPDA>(input, automaton);

	sax::FromXMLParserHelper::popToken(input, sax::Token::TokenType::END_ELEMENT, InputDrivenDPDA::getXmlTagName());
	return automaton;
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::parseTransition(std::deque<sax::Token>::iterator& input, InputDrivenDPDA& automaton) {
	sax::FromXMLParserHelper::popToken(input, sax::Token::TokenType::START_ELEMENT, "transition");
	StateType from = AutomatonFromXMLParser::parseTransitionFrom<StateType>(input);
	InputSymbolType inputSymbol = AutomatonFromXMLParser::parseTransitionInputSymbol<InputSymbolType>(input);
	StateType to = AutomatonFromXMLParser::parseTransitionTo<StateType>(input);
	sax::FromXMLParserHelper::popToken(input, sax::Token::TokenType::END_ELEMENT, "transition");

	automaton.addTransition(std::move(from), std::move(inputSymbol), std::move(to));
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::compose(std::deque<sax::Token>& out) const {
	out.emplace_back(InputDrivenDPDA::getXmlTagName(), sax::Token::TokenType::START_ELEMENT);

	AutomatonToXMLComposer::composeStates(out, this->getStates());
	AutomatonToXMLComposer::composeInputAlphabet(out, this->getInputAlphabet());
	AutomatonToXMLComposer::composePushdownStoreAlphabet(out, this->getPushdownStoreAlphabet());
	AutomatonToXMLComposer::composeInitialState(out, this->getInitialState());
	AutomatonToXMLComposer::composeInitialPushdownStoreSymbol(out, this->getInitialSymbol());
	AutomatonToXMLComposer::composeFinalStates(out, this->getFinalStates());
	AutomatonToXMLComposer::composeInputToPushdownStoreOperation(out, this->getPushdownStoreOperations());
	composeTransitions(out);

	out.emplace_back(InputDrivenDPDA::getXmlTagName(), sax::Token::TokenType::END_ELEMENT);
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
void InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::composeTransitions(std::deque<sax::Token>& out) const {
	out.emplace_back("transitions", sax::Token::TokenType::START_ELEMENT);
	for(const auto& transition : this->getTransitions()) {
		out.emplace_back("transition", sax::Token::TokenType::START_ELEMENT);

		AutomatonToXMLComposer::composeTransitionFrom(out, transition.first.first);
		AutomatonToXMLComposer::composeTransitionInputSymbol(out, transition.first.second);
		AutomatonToXMLComposer::composeTransitionTo(out, transition.second);

		out.emplace_back("transition", sax::Token::TokenType::END_ELEMENT);
	}

	out.emplace_back("transitions", sax::Token::TokenType::END_ELEMENT);
}

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
alib::ObjectBase* InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >::inc() && {
	return new alib::UniqueObject(alib::Object(std::move(*this)), primitive::Integer(0));
}

} /* namespace automaton */

namespace std {

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
class ComponentConstraint< automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >, InputSymbolType, automaton::InputAlphabet > {
public:
	static bool used ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & automaton, const InputSymbolType & symbol ) {
		for (const std::pair<const std::pair<StateType, InputSymbolType>, StateType>& transition : automaton.getTransitions())
			if (transition.first.second == symbol)
				return true;

		return false;
	}

	static bool available ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const InputSymbolType & ) {
		return true;
	}

	static void valid ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const InputSymbolType & ) {
	}
};

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
class ComponentConstraint< automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >, PushdownStoreSymbolType, automaton::PushdownStoreAlphabet > {
public:
	static bool used ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & automaton, const PushdownStoreSymbolType & symbol ) {
		for (const auto& pushdownStoreOperation : automaton.getPushdownStoreOperations()) {
			if (std::find(pushdownStoreOperation.second.first.begin(), pushdownStoreOperation.second.first.end(), symbol) != pushdownStoreOperation.second.first.end())
				return true;
			if (std::find(pushdownStoreOperation.second.second.begin(), pushdownStoreOperation.second.second.end(), symbol) != pushdownStoreOperation.second.second.end())
				return true;
		}

		if(automaton.getInitialSymbol() == symbol)
			return true;

		return false;
	}

	static bool available ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const PushdownStoreSymbolType & ) {
		return true;
	}

	static void valid ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const PushdownStoreSymbolType & ) {
	}
};

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
class ElementConstraint< automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >, PushdownStoreSymbolType, automaton::InitialSymbol > {
public:
	static bool available ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & automaton, const PushdownStoreSymbolType & symbol ) {
		return automaton.template accessComponent < automaton::PushdownStoreAlphabet > ( ).get ( ).count ( symbol );
	}

	static void valid ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const PushdownStoreSymbolType & ) {
	}
};

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
class ComponentConstraint< automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >, StateType, automaton::States > {
public:
	static bool used ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & automaton, const StateType & state ) {
		if ( automaton.getInitialState ( ) == state )
			return true;

		if ( automaton.getFinalStates ( ).count ( state ) )
			return true;

		for (const std::pair<const std::pair<StateType, InputSymbolType>, StateType>& t : automaton.getTransitions())
			if (t.first.first == state || t.second == state)
				return true;

		return false;
	}

	static bool available ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const StateType & ) {
		return true;
	}

	static void valid ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const StateType & ) {
	}
};

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
class ComponentConstraint< automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >, StateType, automaton::FinalStates > {
public:
	static bool used ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const StateType & ) {
		return false;
	}

	static bool available ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & automaton, const StateType & state ) {
		return automaton.template accessComponent < automaton::States > ( ).get ( ).count ( state );
	}

	static void valid ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const StateType & ) {
	}
};

template < class InputSymbolType, class PushdownStoreSymbolType, class StateType >
class ElementConstraint< automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType >, StateType, automaton::InitialState > {
public:
	static bool available ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > & automaton, const StateType & state ) {
		return automaton.template accessComponent < automaton::States > ( ).get ( ).count ( state );
	}

	static void valid ( const automaton::InputDrivenDPDA < InputSymbolType, PushdownStoreSymbolType, StateType > &, const StateType & ) {
	}
};

} /* namespace std */

#endif /* INPUT_DRIVEN_DPDA_H_ */