ToRTEStateElimination.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 <algorithm>
#include <numeric>
 
#include <rte/formal/FormalRTE.h>
 
#include <automaton/Automaton.h>
#include <automaton/TA/DFTA.h>
#include <automaton/TA/ExtendedNFTA.h>
#include <automaton/TA/NFTA.h>
 
#include <rte/formal/FormalRTEElements.h>
 
#include <common/createUnique.hpp>
 
#include <label/FinalStateLabel.h>
 
#include <rte/simplify/RTEOptimize.h>
 
namespace automaton {
 
namespace convert {
 
class ToRTEStateElimination {
public:
    template < class T, class SymbolType = DefaultSymbolType, class StateType = DefaultStateType >
    static rte::FormalRTE< ext::variant< SymbolType, StateType > > convert ( const T& automaton );
 
private:
    template < class SymbolType, class StateType >
    static void extendExtendedNFTA ( automaton::ExtendedNFTA< SymbolType, StateType >& automaton );
 
    template < class SymbolType, class StateType >
    static automaton::ExtendedNFTA< SymbolType, StateType > eliminateState ( const automaton::ExtendedNFTA< SymbolType, StateType >& automaton, const StateType& state );
 
    template < class SymbolType, class StateType >
    static rte::FormalRTEStructure< ext::variant< SymbolType, StateType > > createAlternation ( const ext::vector< ext::pair< ext::pair< rte::FormalRTEStructure< ext::variant< SymbolType, StateType > >, ext::vector< StateType > >, StateType > >& transitions );
};
 
template < class T, class SymbolType, class StateType >
rte::FormalRTE< ext::variant< SymbolType, StateType > > ToRTEStateElimination::convert ( const T& automaton ) {
    if ( automaton.getFinalStates ( ).empty ( ) )
        return rte::FormalRTE< ext::variant< SymbolType, StateType > > ( );
 
    // create an automaton, extend it with a new final state
    automaton::ExtendedNFTA< SymbolType, StateType > extendedAutomaton ( automaton );
    extendExtendedNFTA ( extendedAutomaton );
 
    // eliminate all non-final states
    ext::set< StateType > statesToEliminate;
    std::set_difference ( extendedAutomaton.getStates ( ).begin ( ), extendedAutomaton.getStates ( ).end ( ),
                          extendedAutomaton.getFinalStates ( ).begin ( ), extendedAutomaton.getFinalStates ( ).end ( ),
                          std::inserter ( statesToEliminate, statesToEliminate.begin ( ) ) );
 
    for ( const StateType& state : statesToEliminate ) {
        extendedAutomaton = eliminateState ( extendedAutomaton, state );
    }
 
    // step 4
    ext::vector< ext::pair< ext::pair< rte::FormalRTEStructure< ext::variant< SymbolType, StateType > >, ext::vector< StateType > >, StateType > > alt;
    for ( const auto& tr : extendedAutomaton.getTransitions ( ) )
        for ( const StateType& targetState : tr.second )
            alt.push_back ( ext::make_pair ( tr.first, targetState ) );
 
    return rte::FormalRTE< ext::variant< SymbolType, StateType > > ( rte::simplify::RTEOptimize::optimize ( createAlternation ( alt ) ) );
}
 
template < class SymbolType, class StateType >
rte::FormalRTEStructure< ext::variant< SymbolType, StateType > > ToRTEStateElimination::createAlternation ( const ext::vector< ext::pair< ext::pair< rte::FormalRTEStructure< ext::variant< SymbolType, StateType > >, ext::vector< StateType > >, StateType > >& transitions ) {
    if ( transitions.empty ( ) )
        return rte::FormalRTEStructure< ext::variant< SymbolType, StateType > > ( rte::FormalRTEEmpty< ext::variant< SymbolType, StateType > > ( ) );
    if ( transitions.size ( ) == 1 )
        return transitions.at ( 0 ).first.first;
 
    static auto alt = [] ( const rte::FormalRTEStructure< ext::variant< SymbolType, StateType > >& sum, const ext::pair< ext::pair< rte::FormalRTEStructure< ext::variant< SymbolType, StateType > >, ext::vector< StateType > >, StateType >& transition ) {
        return rte::FormalRTEStructure< ext::variant< SymbolType, StateType > > ( rte::FormalRTEAlternation< ext::variant< SymbolType, StateType > > ( sum.getStructure ( ), transition.first.first.getStructure ( ) ) );
    };
 
    return std::accumulate ( transitions.begin ( ), transitions.end ( ), rte::FormalRTEStructure< ext::variant< SymbolType, StateType > > ( ), alt );
}
 
template < class SymbolType, class StateType >
automaton::ExtendedNFTA< SymbolType, StateType > ToRTEStateElimination::eliminateState ( const automaton::ExtendedNFTA< SymbolType, StateType >& automaton, const StateType & state ) {
    // create state symbol in RTE's K alphabet
    const rte::FormalRTESymbolSubst< ext::variant< SymbolType, StateType > > stateSymbol ( common::ranked_symbol< ext::variant< SymbolType, StateType > > ( state, 0 ) );
 
    // create new automaton, without state Q
    automaton::ExtendedNFTA< SymbolType, StateType > newAutomaton ( automaton.getStates ( ), automaton.getInputAlphabet ( ), automaton.getFinalStates ( ) );
    newAutomaton.removeState ( state ); // preserve all states but state (the one to eliminate)
 
    // divide transitions into the following groups:
    // - loop(Q)          - Q is     in sources AND Q is     a target
    // - incoming(Q)      - Q is NOT in sources AND Q is     a target
    // - outgoing(Q)      - Q is     in sources AND Q is NOT a target
    // - not_take_part(Q) - Q is NOT in sources AND Q is NOT a target
    //
    // also identify prev(incoming(Q)), loop(incoming(Q))
    using transitionType = ext::vector< ext::pair< ext::pair< rte::FormalRTEStructure< ext::variant< SymbolType, StateType > >, ext::vector< StateType > >, StateType > >;
    transitionType loop;
    transitionType incoming;
    transitionType outgoing;
 
    ext::set < StateType > prev_loop;
    ext::set < StateType > prev_incoming;
 
    for ( const auto& transition : automaton.getTransitions ( ) ) {
        for ( const StateType& target : transition.second ) {
            const ext::vector< StateType >& src_states = transition.first.second;
 
            const bool is_source = std::find ( src_states.begin ( ), src_states.end ( ), state ) != src_states.end ( );
            const bool is_target = target == state;
 
            if ( is_source && is_target ) { // loop
                loop.push_back ( ext::make_pair ( transition.first, target ) );
                prev_loop.insert ( transition.first.second.begin ( ), transition.first.second.end ( ) );
            } else if ( ! is_source && is_target ) { // incoming
                incoming.push_back ( ext::make_pair ( transition.first, target ) );
                prev_incoming.insert ( transition.first.second.begin ( ), transition.first.second.end ( ) );
            } else if ( is_source && ! is_target ) { //outgoing
                outgoing.push_back ( ext::make_pair ( transition.first, target ) );
            } else /* ( ! is_source && ! is_target ) */ { // not_take_part
                newAutomaton.addTransition ( transition.first.first, transition.first.second, target );
            }
        }
    }
 
    using edgeLabelType = rte::FormalRTEStructure< ext::variant< SymbolType, StateType > >;
    const edgeLabelType rte_loop = createAlternation ( loop );
    const edgeLabelType rte_incoming = createAlternation ( incoming );
 
    // eliminate all incoming and outgoing transitions as follows:
    // for every outgoing transition:
    //  - do the SUBST(outgoing, SUBST(iter(loops), incoming)) operation
    for ( const auto& transition : outgoing ) {
        const rte::FormalRTEStructure< ext::variant< SymbolType, StateType > >& tr_rte = transition.first.first;
        const ext::vector< StateType >& tr_src_states = transition.first.second;
        const StateType& tr_target = transition.second;
 
        // by eliminating Q, the new transition T will be in the from ( merge(prev_loop, prev_incoming, prev_outgoing) ) -> outgoing.target
        // The order of prev_states is not important as the order is present in the RTE structure since the first conversion to ExtendedNFTA
        ext::set< StateType > prevStates;
        prevStates.insert ( prev_loop.begin ( ), prev_loop.end ( ) );
        prevStates.insert ( prev_incoming.begin ( ), prev_incoming.end ( ) );
        prevStates.insert ( tr_src_states.begin ( ), tr_src_states.end ( ) );
        prevStates.erase ( state );
 
        rte::FormalRTEStructure< ext::variant< SymbolType, StateType > > rte (
            rte::FormalRTESubstitution< ext::variant< SymbolType, StateType > > (
                tr_rte.getStructure ( ), // outgoing rte
                rte::FormalRTESubstitution< ext::variant< SymbolType, StateType > > (
                    rte::FormalRTEIteration< ext::variant< SymbolType, StateType > > ( rte_loop.getStructure ( ), stateSymbol ),
                    rte_incoming.getStructure ( ), stateSymbol ),
                stateSymbol ) );
 
        // TATA pattern
        /*
        rte::FormalRTEStructure < ext::variant < SymbolType, StateType > > rte (
                rte::FormalRTESubstitution < ext::variant < SymbolType, StateType > > (
                    rte::FormalRTESubstitution < ext::variant < SymbolType, StateType > > (
                        tr_rte.getStructure ( ), // outgoing rte
                        rte::FormalRTEIteration < ext::variant < SymbolType, StateType > > ( rte_loop.getStructure ( ), stateSymbol ),
                        stateSymbol ),
                    rte_incoming.getStructure ( ),
                    stateSymbol ) );
        */
 
        newAutomaton.addTransition ( rte::simplify::RTEOptimize::optimize ( rte ), ext::vector< StateType > ( prevStates.begin ( ), prevStates.end ( ) ), tr_target );
    }
 
    return newAutomaton;
}
 
template < class SymbolType, class StateType >
void ToRTEStateElimination::extendExtendedNFTA ( automaton::ExtendedNFTA< SymbolType, StateType >& automaton ) {
    // create new state with final label
    const StateType f = common::createUnique ( label::FinalStateLabel::instance< StateType > ( ), automaton.getStates ( ) );
    automaton.addState ( f );
 
    // create transitions from all final states to the new state, the transition contains only reference (RTE's K symbol) to the previous final state
    for ( const StateType& state : automaton.getFinalStates ( ) ) {
        const rte::FormalRTEStructure< ext::variant< SymbolType, StateType > > expr ( rte::FormalRTESymbolSubst< ext::variant< SymbolType, StateType > > ( common::ranked_symbol< ext::variant< SymbolType, StateType > > ( state, 0 ) ) );
        automaton.addTransition ( expr, { state }, f );
    }
 
    // new state is the only final
    automaton.setFinalStates ( { f } );
}
 
} /* namespace convert */
 
} /* namespace automaton */