DeterminizeIDPDAPart.cxx

/*
 * IDPDADeterminizer.cpp
 *
 *  Created on: 16. 1. 2014
 *	  Author: Jan Vesely
 */

#include "common/NFACommon.h"

#include <automaton/PDA/InputDrivenNPDA.h>
#include <deque>
#include <algorithm>

namespace automaton {

namespace determinize {

automaton::InputDrivenDPDA < > Determinize::determinize ( const automaton::InputDrivenNPDA < > & nfa ) {
	 // 1, 4
	DefaultStateType initialState ( createDFAState ( { nfa.getInitialState ( ) } ) );
	automaton::InputDrivenDPDA < > res ( initialState, nfa.getInitialSymbol ( ) );

	res.setInputAlphabet ( nfa.getInputAlphabet ( ) );
	res.setPushdownStoreAlphabet ( nfa.getPushdownStoreAlphabet ( ) );
	res.setPushdownStoreOperations ( nfa.getPushdownStoreOperations ( ) );

	 // 2
	ext::deque < DefaultStateType > todo;
	todo.push_back ( std::move ( initialState ) );

	do {
		 // 3a, c
		DefaultStateType state = std::move ( todo.front ( ) );
		todo.pop_front ( );

		 // 3b
		for ( const DefaultSymbolType & input : nfa.getInputAlphabet ( ) ) {
			ext::set < DefaultStateType > targetIDPDAStates;

			for ( DefaultStateType nfaState : recreateNFAStates ( state ) ) {
				auto iter = nfa.getTransitions ( ).find ( ext::make_pair ( std::move ( nfaState ), input ) );

				if ( iter != nfa.getTransitions ( ).end ( ) )
					targetIDPDAStates.insert ( iter->second.begin ( ), iter->second.end ( ) );
			}

			DefaultStateType dfaState = createDFAState ( std::move ( targetIDPDAStates ) );

			 // 4
			bool existed = !res.addState ( dfaState );

			if ( !existed ) todo.push_back ( dfaState );

			 // 3b
			res.addTransition ( state, input, std::move ( dfaState ) );
		}
	} while ( !todo.empty ( ) );

	 // 5
	const ext::set<DefaultStateType>& finalLabels = nfa.getFinalStates();
	for ( const DefaultStateType & dfaState : res.getStates ( ) ) {
		const ext::set < DefaultStateType > & nfaStates = recreateNFAStates ( dfaState );

		if(!ext::excludes(finalLabels.begin(), finalLabels.end(), nfaStates.begin(), nfaStates.end()))
			res.addFinalState ( dfaState );
	}

	return res;
}

auto DeterminizeInputDrivenNPDA = registration::AbstractRegister < Determinize, automaton::InputDrivenDPDA < >, const automaton::InputDrivenNPDA < > & > ( Determinize::determinize );

} /* namespace determinize */

} /* namespace automaton */