DeterminizeIDPDAPart.cxx

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

#include <core/multipleDispatch.hpp>

#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
	automaton::State initialState ( createDFAState ( { nfa.getInitialState ( ) } ) );
	automaton::InputDrivenDPDA res ( initialState, nfa.getInitialSymbol ( ) );

	res.setInputAlphabet ( nfa.getInputAlphabet ( ) );
	res.setStackAlphabet ( nfa.getStackAlphabet ( ) );
	res.setPushdownStoreOperations ( nfa.getPushdownStoreOperations ( ) );

	 // 2
	std::deque < automaton::State > todo;
	todo.push_back ( std::move ( initialState ) );

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

		 // 3b
		for ( const alphabet::Symbol & input : nfa.getInputAlphabet ( ) ) {
			std::set < automaton::State > targetIDPDAStates;

			for ( automaton::State nfaState : make_dsubset_iterator ( state ) ) {
				auto iter = nfa.getTransitions ( ).find ( std::make_pair ( std::move ( nfaState ), input ) );

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

			automaton::State dfaState = createDFAState ( std::move ( targetIDPDAStates ) );

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

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

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

	 // 5
	const std::set<automaton::State>& finalLabels = nfa.getFinalStates();
	for ( const automaton::State & dfaState : res.getStates ( ) ) {
		auto nfaStates = make_dsubset_iterator ( dfaState );

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

	return res;
}

auto DeterminizeInputDrivenNPDA = Determinize::RegistratorWrapper < automaton::InputDrivenDPDA, automaton::InputDrivenNPDA > ( Determinize::determinize );

} /* namespace determinize */

} /* namespace automaton */