AutomataLeftQuotientCartesianProduct.h

Go to the documentation of this file.

 
/*
 * 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/>.
 */
 
#pragma once
 
#include <automaton/FSM/MultiInitialStateNFA.h>
#include <queue>
 
namespace automaton {
 
namespace transform {
 
class AutomataLeftQuotientCartesianProduct {
public:
    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.empty ( ) ) {
        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) {
                        if ( ! full || ! first.getFinalStates ( ).count ( tp.second ) )
                            delta [ ext::make_pair ( state, tp.first.second ) ].insert ( ext::make_pair ( tp.second, tq.second ) );
 
                        queue.push ( ext::make_pair ( tp.second, tq.second ) ); // 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 ) ) {
        for ( ext::pair < StateType1, StateType2 > to : ext::make_mover ( transitions.second ) )
            res.addTransition ( transitions.first.first, transitions.first.second, std::move ( to ) );
    }
 
    res.setInitialStates ( Q0 );
    res.setFinalStates ( F );
 
    return res;
}
 
} /* namespace transform */
 
} /* namespace automaton */