diff --git a/alib2algo/src/automaton/simplify/Normalize.cpp b/alib2algo/src/automaton/simplify/Normalize.cpp index 30d0ba345f10ec1ea7232aca534dcf39a02a428d..a0e22e9a1d6355c80c98fc98feb5ea1bbe95af48 100644 --- a/alib2algo/src/automaton/simplify/Normalize.cpp +++ b/alib2algo/src/automaton/simplify/Normalize.cpp @@ -40,6 +40,15 @@ We normalize also the pushdown store symbols.\n\ \n\ @throws exception::CommonException if the passed dpda was not deterministic connected pda" ); +auto NormalizeDFTA = registration::AbstractRegister < Normalize, automaton::DFTA < DefaultSymbolType, DefaultRankType, unsigned >, const automaton::DFTA < > & > ( Normalize::normalize, "automaton" ).setDocumentation ( +"Normalization of deterministic finite tree automata.\n\ +The process of normalization is a BFS traversal through the graph representing the automaton. The states are named by integers in the visited order.\n\ +\n\ +@param dfa determinsitic finite tree automaton to normalize\n\ +@return @p dfta with state labels normalized\n\ +\n\ +@throws exception::CommonException if the passed dfta was not minimal connected dfta" ); + } /* namespace simplify */ } /* namespace automaton */ diff --git a/alib2algo/src/automaton/simplify/Normalize.h b/alib2algo/src/automaton/simplify/Normalize.h index 2ecf1131fba9180da93984d45ef05fbfa6f76088..5d4fd9df8385d540a960a62166b83c248b4f4380 100644 --- a/alib2algo/src/automaton/simplify/Normalize.h +++ b/alib2algo/src/automaton/simplify/Normalize.h @@ -26,6 +26,7 @@ #include <automaton/FSM/DFA.h> #include <automaton/FSM/CompactDFA.h> +#include <automaton/TA/DFTA.h> #include <automaton/PDA/DPDA.h> namespace automaton { @@ -86,6 +87,21 @@ public: */ template < class InputSymbolType, class EpsilonType, class PushdownStoreSymbolType, class StateType > static automaton::DPDA < InputSymbolType, EpsilonType, unsigned, unsigned > normalize(const automaton::DPDA < InputSymbolType, EpsilonType, PushdownStoreSymbolType, StateType > & dpda); + + /** + * Normalization of deterministic finite tree automata. + * The process of normalization is a BFS traversal through the graph representing the automaton. The states are named by integers in the visited order. + * + * @tparam SymbolType Type for input symbols. + * @tparam RankType Type for input symbols rank. + * @tparam StateType Type for states. + * @param dfa determinsitic finite tree automaton to normalize + * @return @p fta with state labels normalized + * + * @throws exception::CommonException if the passed dfa was not minimal dfta + */ + template < class SymbolType, class RankType, class StateType > + static automaton::DFTA < SymbolType, RankType, unsigned > normalize ( const automaton::DFTA < SymbolType, RankType, StateType > & fta ); }; template < class SymbolType, class StateType > @@ -266,6 +282,62 @@ automaton::DPDA < InputSymbolType, EpsilonType, unsigned, unsigned > Normalize:: return result; } +template < class SymbolType, class RankType, class StateType > +automaton::DFTA < SymbolType, RankType, unsigned > Normalize::normalize ( const automaton::DFTA < SymbolType, RankType, StateType > & fta ) { + unsigned counter = 0; + ext::map < StateType, unsigned > normalizationData; + + auto isNormalized = [ & normalizationData ] ( const StateType & origName ) { + return normalizationData.count ( origName ) > 0; + }; + + ext::map < ext::pair < common::ranked_symbol < SymbolType, RankType >, ext::vector < unsigned > >, StateType > processing; + do { + processing.clear ( ); + + // accumulate all transitions from normalized states to not yet normalized state + for ( const auto & transition : fta.getTransitions ( ) ) + if ( std::all_of ( transition.first.second.begin ( ), transition.first.second.end ( ), isNormalized ) && ! isNormalized ( transition.second ) ) { + ext::vector < unsigned > from; + for ( const StateType & state : transition.first.second ) + from.push_back ( normalizationData.at ( state ) ); + + processing.insert ( ext::make_pair ( transition.first.first, from ), transition.second ); + } + + for ( const std::pair < const ext::pair < common::ranked_symbol < SymbolType, RankType >, ext::vector < unsigned > >, StateType > & transition : processing ) + // accumuated transition inducing normalization might have contained two or more transitions to the same state, but we want to normalize only once + if ( ! isNormalized ( transition.second ) ) + normalizationData [ transition.second ] = counter ++; + + } while ( processing.size ( ) > 0 ); + + if ( normalizationData.size ( ) != fta.getStates ( ).size ( ) ) { + throw exception::CommonException ( "Automaton normalize require minimal deterministic finite tree automaton" ); + } + + automaton::DFTA < SymbolType, RankType, unsigned > result; + result.setInputAlphabet ( fta.getInputAlphabet ( ) ); + + for ( const StateType & state : fta.getStates ( ) ) { + result.addState ( normalizationData.at ( state ) ); + } + + for ( const StateType & finalState : fta.getFinalStates ( ) ) { + result.addFinalState ( normalizationData.at ( finalState ) ); + } + + for ( const auto & transition : fta.getTransitions ( ) ) { + ext::vector < unsigned > prevStates; + for ( const StateType & prev : transition.first.second ) + prevStates.push_back ( normalizationData.at ( prev ) ); + + result.addTransition ( transition.first.first, prevStates, normalizationData.at ( transition.second ) ); + } + + return result; +} + } /* namespace simplify */ } /* namespace automaton */