MinimizeByPartitioning.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 <alib/set>
#include <alib/map>
 
#include <automaton/FSM/DFA.h>
#include <automaton/FSM/NFA.h>
#include <automaton/TA/DFTA.h>
#include <automaton/TA/NFTA.h>
#include <automaton/TA/UnorderedDFTA.h>
#include <automaton/TA/UnorderedNFTA.h>
 
namespace automaton {
 
namespace simplify {
 
class MinimizeByPartitioning {
    template < class T >
    using FA = typename std::conditional < isDFA < T >, automaton::DFA < typename T::SymbolType, ext::set < typename T::StateType > >, automaton::NFA < typename T::SymbolType, ext::set < typename T::StateType > > >::type;
 
    template < class T >
    using FTA = typename std::conditional < isDFTA < T >, automaton::DFTA < typename T::SymbolType, ext::set < typename T::StateType > >, automaton::NFTA < typename T::SymbolType, ext::set < typename T::StateType > > >::type;
 
    template < class T >
    using UnorderedFTA = typename std::conditional < isUnorderedDFTA < T >, automaton::UnorderedDFTA < typename T::SymbolType, ext::set < typename T::StateType > >, automaton::UnorderedNFTA < typename T::SymbolType, ext::set < typename T::StateType > > >::type;
 
public:
    template < class T >
    requires isDFA < T > || isNFA < T >
    static FA < T > minimize ( const T & nfa, const ext::set < ext::set < typename T::StateType > > & partitions );
 
    template < class T >
    requires isDFTA < T > || isNFTA < T >
    static FTA < T > minimize ( const T & dfta, const ext::set < ext::set < typename T::StateType > > & partitions );
 
    template < class T >
    requires isUnorderedDFTA < T > || isUnorderedNFTA < T >
    static UnorderedFTA < T > minimize ( const T & dfta, const ext::set < ext::set < typename T::StateType > > & partitions );
 
private:
    template < class StateType >
    static ext::map < StateType, ext::set < StateType > > partitionMap ( const ext::set < ext::set < StateType > > & partitions );
};
 
template < class StateType >
ext::map < StateType, ext::set < StateType > > MinimizeByPartitioning::partitionMap ( const ext::set < ext::set < StateType > > & partitions ) {
    ext::map < StateType, ext::set < StateType > > res;
 
    for ( const auto & partition : partitions )
        for ( const StateType & state : partition )
            res [ state ] = partition;
 
    return res;
}
 
template < class T >
requires isDFA < T > || isNFA < T >
MinimizeByPartitioning::FA < T > MinimizeByPartitioning::minimize ( const T & nfa, const ext::set < ext::set < typename T::StateType > > & partitions ) {
    using StateType = typename T::StateType;
 
    const ext::map < StateType, ext::set < StateType > > statePartitionMap = partitionMap ( partitions );
 
    MinimizeByPartitioning::FA < T > res ( statePartitionMap.at ( nfa.getInitialState ( ) ) );
    res.setStates ( partitions );
    res.addInputSymbols ( nfa.getInputAlphabet ( ) );
    for ( const StateType & state : nfa.getFinalStates ( ) )
        res.addFinalState ( statePartitionMap.at ( state ) );
 
    for ( const auto & transition : nfa.getTransitions ( ) )
        res.addTransition ( statePartitionMap.at ( transition.first.first ), transition.first.second, statePartitionMap.at ( transition.second ) );
 
    return res;
}
 
template < class T >
requires isDFTA < T > || isNFTA < T >
MinimizeByPartitioning::FTA < T > MinimizeByPartitioning::minimize ( const T & dfta, const ext::set < ext::set < typename T::StateType > > & partitions ) {
    using StateType = typename T::StateType;
 
    const ext::map < StateType, ext::set < StateType > > statePartitionMap = partitionMap ( partitions );
 
    MinimizeByPartitioning::FTA < T > res;
    res.setStates ( partitions );
    res.addInputSymbols ( dfta.getInputAlphabet ( ) );
    for ( const StateType & state : dfta.getFinalStates ( ) )
        res.addFinalState ( statePartitionMap.at ( state ) );
 
    for ( const auto & transition : dfta.getTransitions ( ) ) {
        ext::vector < ext::set < StateType > > minimalFrom;
        for ( const StateType & from : transition.first.second )
            minimalFrom.push_back ( statePartitionMap.at ( from ) );
        res.addTransition ( transition.first.first, minimalFrom, statePartitionMap.at ( transition.second ) );
    }
 
    return res;
}
 
template < class T >
requires isUnorderedDFTA < T > || isUnorderedNFTA < T >
MinimizeByPartitioning::UnorderedFTA < T > MinimizeByPartitioning::minimize ( const T & dfta, const ext::set < ext::set < typename T::StateType > > & partitions ) {
    using StateType = typename T::StateType;
 
    const ext::map < StateType, ext::set < StateType > > statePartitionMap = partitionMap ( partitions );
 
    MinimizeByPartitioning::UnorderedFTA < T > res;
    res.setStates ( partitions );
    res.addInputSymbols ( dfta.getInputAlphabet ( ) );
    for ( const StateType & state : dfta.getFinalStates ( ) )
        res.addFinalState ( statePartitionMap.at ( state ) );
 
    for ( const auto & transition : dfta.getTransitions ( ) ) {
        ext::multiset < ext::set < StateType > > minimalFrom;
        for ( const StateType & from : transition.first.second )
            minimalFrom.insert ( statePartitionMap.at ( from ) );
        res.addTransition ( transition.first.first, minimalFrom, statePartitionMap.at ( transition.second ) );
    }
 
    return res;
}
 
} /* namespace simplify */
 
} /* namespace automaton */