diff --git a/alib2algo/src/automaton/transform/AutomataLeftQuotientCartesianProduct.cpp b/alib2algo/src/automaton/transform/AutomataLeftQuotientCartesianProduct.cpp new file mode 100644 index 0000000000000000000000000000000000000000..dbaf8b60f7237ffabfaa86abbef29e8eef7a98ab --- /dev/null +++ b/alib2algo/src/automaton/transform/AutomataLeftQuotientCartesianProduct.cpp @@ -0,0 +1,20 @@ +/* + * AutomataLeftQuotientCartesianProduct.cpp + * + * Created on: 20. 11. 2014 + * Author: Tomas Pecka + */ + +#include "AutomataLeftQuotientCartesianProduct.h" +#include <registration/AlgoRegistration.hpp> + +namespace automaton { + +namespace transform { + +auto AutomataLeftQuotientCartesianProductNFA2 = registration::AbstractRegister < AutomataLeftQuotientCartesianProduct, automaton::MultiInitialStateNFA < DefaultSymbolType, ext::pair < DefaultStateType, DefaultStateType > >, const automaton::NFA < > &, const automaton::NFA < > &, bool > ( AutomataLeftQuotientCartesianProduct::quotient ); + + +} /* namespace transform */ + +} /* namespace automaton */ diff --git a/alib2algo/src/automaton/transform/AutomataLeftQuotientCartesianProduct.h b/alib2algo/src/automaton/transform/AutomataLeftQuotientCartesianProduct.h new file mode 100644 index 0000000000000000000000000000000000000000..1c448d82cbacbf8023573732e6c2d8814a1b302b --- /dev/null +++ b/alib2algo/src/automaton/transform/AutomataLeftQuotientCartesianProduct.h @@ -0,0 +1,112 @@ +/* + * AutomataLeftQuotientCartesianProduct.h + * + * This file is part of Algorithms library toolkit. + * Copyright (C) 2017 Jan Travnicek (jan.travnicek@fit.cvut.cz) + + * Algorithms library toolkit is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + + * Algorithms library toolkit is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + + * You should have received a copy of the GNU General Public License + * along with Algorithms library toolkit. If not, see <http://www.gnu.org/licenses/>. + * + * Created on: 20. 11. 2014 + * Author: Tomas Pecka + */ + +#ifndef AUTOMATA_LEFT_QUOTIENT_CARTESIAN_H_ +#define AUTOMATA_LEFT_QUOTIENT_CARTESIAN_H_ + +#include <automaton/FSM/MultiInitialStateNFA.h> +#include <queue> + +namespace automaton { + +namespace transform { + +/** + * Computation of the left quotient of languages represented by two finite automata. + * For finite automata A1, A2, we create a finite automaton A such that L(A) = \{ x : wx \in L(A2) and w \in L(A1) \}. + * Full quotient requires that w is maximal and x does not have prefix from L(A1). Non-full quotient does not require that to be true and only some prefix is removed from words in L(A2). + * This method utilizes cartesian product construction and it is described in paper "The Full Quotient and Its Closure Properties for Regular Languages". + */ +class AutomataLeftQuotientCartesianProduct { +public: + /** + * Divides (computes quotient of) two languages represented by two finite automata. + * @tparam SymbolType Type for input symbols. + * @tparam StateType1 Type for states in the first automaton. + * @tparam StateType2 Type for states in the second automaton. + * @param first First automaton (A1) representing language of the removed prefix + * @param second Second automaton (A2) representing language from which the prefix is removed + * @param full true if the resulting quotient should be full, false if not. + * @return nondeterministic FA with multiple initial states representing the division (computed quotient) of two languages + */ + template < class SymbolType, class StateType1, class StateType2 > + static automaton::MultiInitialStateNFA < SymbolType, ext::pair < StateType1, StateType2 > > quotient(const automaton::NFA < SymbolType, StateType1 > & first, const automaton::NFA < SymbolType, StateType2 > & second, bool full); +}; + +template < class SymbolType, class StateType1, class StateType2 > +automaton::MultiInitialStateNFA < SymbolType, ext::pair < StateType1, StateType2 > > AutomataLeftQuotientCartesianProduct::quotient(const automaton::NFA < SymbolType, StateType1 > & first, const automaton::NFA < SymbolType, StateType2 > & second, bool full) { + std::queue < ext::pair < StateType1, StateType2 > > queue; + queue.push ( ext::pair < StateType1, StateType2 > ( first.getInitialState ( ), second.getInitialState ( ) ) ); + + ext::set < ext::pair < StateType1, StateType2 > > Q; + ext::map < ext::pair < ext::pair < StateType1, StateType2 >, SymbolType >, ext::set < ext::pair < StateType1, StateType2 > > > delta; + ext::set < ext::pair < StateType1, StateType2 > > Q0; + ext::set < ext::pair < StateType1, StateType2 > > F; + + while ( queue.size ( ) ) { + ext::pair < StateType1, StateType2 > state = std::move ( queue.front ( ) ); + queue.pop ( ); + + if ( ! Q.count ( state ) ) { + Q.insert ( state ); + + if ( first.getFinalStates ( ).count ( state.first ) ) + Q0.insert ( state ); + if ( second.getFinalStates ( ).count ( state.second ) ) + F.insert ( state ); + + for(const auto & tp : first.getTransitionsFromState ( state.first ) ) + for(const auto & tq : second.getTransitionsFromState ( state.second ) ) + if(tp.first.second == tq.first.second) + for(const auto & p : tp.second) + for(const auto & q : tq.second) { + if ( ! full || ! first.getFinalStates ( ).count ( p ) ) + delta [ ext::make_pair ( state, tp.first.second ) ].insert ( ext::make_pair ( p, q ) ); + + queue.push ( ext::make_pair ( p, q ) ); // Note: the original paper kept this queue push statement included in body of the above condition. That is not correct. + } + } + } + + automaton::MultiInitialStateNFA < SymbolType, ext::pair < StateType1, StateType2 > > res; + + res.addInputSymbols(first.getInputAlphabet()); + res.addInputSymbols(second.getInputAlphabet()); + + res.setStates ( Q ); + + for ( std::pair < ext::pair < ext::pair < StateType1, StateType2 >, SymbolType >, ext::set < ext::pair < StateType1, StateType2 > > > transitions : ext::make_mover ( delta ) ) { + res.addTransitions ( transitions.first.first, transitions.first.second, transitions.second ); + } + + res.setInitialStates ( Q0 ); + res.setFinalStates ( F ); + + return res; +} + +} /* namespace transform */ + +} /* namespace automaton */ + +#endif /* AUTOMATA_LEFT_QUOTIENT_CARTESIAN_H_ */