/*
 * AutomatonPropertiesFSM.cpp
 *
 *  Created on: 23. 3. 2014
 *	  Author: Tomas Pecka
 */

#include "AutomatonPropertiesFSM.h"

#include <exception/AlibException.h>
#include <automaton/FSM/ExtendedNFA.h>
#include <automaton/FSM/CompactNFA.h>
#include <automaton/FSM/EpsilonNFA.h>
#include <automaton/FSM/NFA.h>
#include <automaton/FSM/DFA.h>

namespace automaton {

template<class T>
std::set<automaton::State> AutomatonPropertiesFSM::getUsefullStates( const T & fsm ) {
	// 1a
	std::deque<std::set<automaton::State>> Qi;
	Qi.push_back( std::set<automaton::State>( ) );
	Qi.at( 0 ) = fsm.getFinalStates( );

	int i = 1;

	// 1bc
	while( true ) {
		Qi.push_back( Qi.at( i - 1 ) ); // copy Qi-1 into Qi
		for( const auto & p : Qi.at( i - 1 ) )
			for( const auto & t : fsm.getTransitionsToState( p ) )
				Qi.at( i ).insert( t.first.first );

		if( Qi.at( i ) == Qi.at( i - 1 ) )
			break;

		i = i + 1;
	}
	return Qi.at( i );
}

template std::set<automaton::State> AutomatonPropertiesFSM::getUsefullStates( const automaton::EpsilonNFA & fsm );
template std::set<automaton::State> AutomatonPropertiesFSM::getUsefullStates( const automaton::NFA & fsm );
template std::set<automaton::State> AutomatonPropertiesFSM::getUsefullStates( const automaton::CompactNFA & fsm );
template std::set<automaton::State> AutomatonPropertiesFSM::getUsefullStates( const automaton::ExtendedNFA & fsm );

template<>
std::set<automaton::State> AutomatonPropertiesFSM::getUsefullStates( const automaton::DFA & fsm ) {
	// 1a
	std::deque<std::set<automaton::State>> Qi;
	Qi.push_back( std::set<automaton::State>( ) );
	Qi.at( 0 ) = fsm.getFinalStates( );

	int i = 1;

	// 1bc
	while( true ) {
		Qi.push_back( Qi.at( i - 1 ) ); // copy Qi-1 into Qi
		for( const auto & p : Qi.at( i - 1 ) )
			for( const auto & t : fsm.getTransitionsToState( p ) )
				Qi.at( i ).insert( t.first.first );

		if( Qi.at( i ) == Qi.at( i - 1 ) )
			break;

		i = i + 1;
	}
	return Qi.at( i );
}

template<class T>
std::set<automaton::State> AutomatonPropertiesFSM::getUnreachableStates( const T & fsm ) {
	// 1a
	std::deque<std::set<automaton::State>> Qi;
	Qi.push_back( std::set<automaton::State>( ) );
	Qi.at( 0 ) = fsm.getInitialStates( );

	int i = 1;

	// 1bc
	while( true ) {
		Qi.push_back( Qi.at( i - 1 ) );

		for( const auto & p : Qi.at( i - 1 ) )
			for( const auto & transition : fsm.getTransitionsFromState( p ) )
				Qi.at( i ).insert( transition.second.begin(), transition.second.end() );

		if( Qi.at( i ) == Qi.at( i - 1 ) )
			break;

		i = i + 1;
	}

	return Qi.at( i );
}

template std::set<automaton::State> AutomatonPropertiesFSM::getUnreachableStates( const automaton::EpsilonNFA & fsm );
template std::set<automaton::State> AutomatonPropertiesFSM::getUnreachableStates( const automaton::NFA & fsm );
template std::set<automaton::State> AutomatonPropertiesFSM::getUnreachableStates( const automaton::CompactNFA & fsm );
template std::set<automaton::State> AutomatonPropertiesFSM::getUnreachableStates( const automaton::ExtendedNFA & fsm );

template<>
std::set<automaton::State> AutomatonPropertiesFSM::getUnreachableStates( const automaton::DFA & fsm ) {
	// 1a
	std::deque<std::set<automaton::State>> Qi;
	Qi.push_back( std::set<automaton::State>( ) );
	Qi.at( 0 ). insert( fsm.getInitialState( ) );

	int i = 1;

	// 1bc
	while( true ) {
		Qi.push_back( Qi.at( i - 1 ) );

		for( const auto & p : Qi.at( i - 1 ) )
			for( const auto & transition : fsm.getTransitionsFromState( p ) )
				Qi.at( i ).insert( transition.second );

		if( Qi.at( i ) == Qi.at( i - 1 ) )
			break;

		i = i + 1;
	}

	return Qi.at( i );
}

}