ReachableStates.h

Go to the documentation of this file.

 
#pragma once
 
#include <algorithm>
#include <deque>
#include <set>
#include <map>
 
#include <automaton/FSM/ExtendedNFA.h>
#include <automaton/FSM/CompactNFA.h>
#include <automaton/FSM/EpsilonNFA.h>
#include <automaton/FSM/NFA.h>
#include <automaton/FSM/DFA.h>
 
namespace automaton {
 
namespace properties {
 
namespace efficient {
 
class ReachableStates {
public:
    template < class T >
    static ext::set < typename T::StateType > reachableStates( const T & fsm );
    template < class SymbolType, class StateType >
    static ext::set<StateType> reachableStates( const automaton::MultiInitialStateNFA < SymbolType, StateType > & fsm );
};
 
template < class T >
ext::set < typename T::StateType > ReachableStates::reachableStates( const T & fsm ) {
    using StateType = typename T::StateType;
 
    ext::map<StateType, ext::set<StateType>> transitions;
    for(const auto& transition : fsm.getTransitions())
        transitions[transition.first.first].insert(transition.second);
 
    ext::deque<StateType> queue { fsm.getInitialState( ) };
    ext::set<StateType> visited { fsm.getInitialState( ) };
 
    while( !queue.empty() ) {
        const ext::set<StateType>& to = transitions[queue.front()];
        queue.pop_front();
 
        for(const StateType& process : to)
            if(visited.insert(process).second) {
                queue.push_back(std::move(const_cast<StateType&>(process)));
            }
    }
 
    return visited;
}
 
template < class SymbolType, class StateType >
ext::set<StateType> ReachableStates::reachableStates( const automaton::MultiInitialStateNFA < SymbolType, StateType > & fsm ) {
    ext::map<StateType, ext::set<StateType>> transitions;
    for(const auto& transition : fsm.getTransitions())
        transitions[transition.first.first].insert(transition.second);
 
    ext::deque<StateType> queue ( fsm.getInitialStates( ).begin(), fsm.getInitialStates().end() );
    ext::set<StateType> visited = fsm.getInitialStates( );
 
    while( !queue.empty() ) {
        const ext::set<StateType>& to = transitions[queue.front()];
        queue.pop_front();
 
        for(const StateType& process : to)
            if(visited.insert(process).second) {
                queue.push_back(std::move(const_cast<StateType&>(process)));
            }
    }
 
    return visited;
}
 
} /* namespace efficient */
 
} /* namespace properties */
 
} /* namespace automaton */