/*
 * 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>

#include <set>
#include <map>
#include <queue>

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 );
}

std::set<automaton::State> AutomatonPropertiesFSM::epsilonClosure( automaton::EpsilonNFA const& fsm, automaton::State const& q ) {
	std::set<automaton::State> closure;
	std::queue<automaton::State> queue;
	std::map<automaton::State, bool> visited;

	for( const auto & p : fsm.getStates( ) )
		visited[ p ] = false;

	queue.push( q );
	while( ! queue.empty( ) )
	{
		const automaton::State & p = queue.front( );
		queue.pop( );
		visited[ p ] = true;
		closure.insert( p );

		for( const auto & transition : fsm.getEpsilonTransitionsFromState( p ) )
			for (const auto & to : transition.second )
				if( visited [ to ] == false )
					queue.push( to );
	}

	return closure;
}

}