Abstract.hh

Go to the documentation of this file.

#ifndef __DIADES__AUTOMATA__EXPERIMENTAL__ABSTRACT__HH
#define __DIADES__AUTOMATA__EXPERIMENTAL__ABSTRACT__HH

#include<unordered_map>
#include<unordered_set>
#include<diades/automata/experimental/StateMachine.hh>
#include<diades/automata/experimental/BeliefState.hh>
#include<diades/automata/experimental/StatePropertyManager.hh>

namespace Diades {
    namespace Automata {
        namespace Experimental {

            template<typename Fsm, typename BeliefStateIterator, typename StateCreation>
            bool
            abstract(const Fsm & machine,
                     Fsm & abstractedMachine,
                     BeliefStateIterator bfBegin, BeliefStateIterator bfEnd,
                     std::vector<typename Fsm::State> & abstractedStates,
                     StateCreation & creator) {
                using State = typename Fsm::State;
                using Transition = typename Fsm::Transition;
                if (machine == abstractedMachine) {
                    return false;
                }
                std::unordered_map<State, std::unordered_set < size_t>> bsOfState;
                std::vector<BeliefStateIterator> iterators;

                for (auto it = bfBegin; it != bfEnd; ++it) {
                    bool result;
                    typename Fsm::State newState;
                    std::tie(newState,result) = creator.newState(*it);
                    iterators.push_back(it);
                    abstractedStates.push_back(newState);
                    std::for_each(it->begin(), it->end(), [&](State s) {
                        bsOfState[s].insert(iterators.size() - 1);
                        if (machine.isInitial(s)) {
                            abstractedMachine.setInitial(abstractedStates.back());
                        }
                    });
                }
                abstractedMachine.copyEventPropertyIds(machine);
                std::for_each(bsOfState.begin(), bsOfState.end(),
                        [&](const std::pair<State, std::unordered_set < size_t> > & bsState) {
                            std::for_each(machine.outputTransitionBegin(bsState.first),
                                    machine.outputTransitionEnd(bsState.first),
                                    [&](Transition t) {
                                        auto itTarget = bsOfState.find(t.target());
                                        if (itTarget != bsOfState.end()) {
                                            std::for_each(bsState.second.begin(),
                                                    bsState.second.end(),
                                                    [&](size_t sourceId) {
                                                        std::for_each(itTarget->second.begin(),
                                                                itTarget->second.end(),
                                                                [&](size_t targetId) {
                                                                    abstractedMachine.newTransition(abstractedStates[sourceId],
                                                                            abstractedStates[targetId],
                                                                            machine.getEvent(t));
                                                                });
                                                    });
                                        }
                                    });
                        });
                return true;
            }

            
//            /**
//             * 
//             * @param machine a StateMachine
//             * @param abstractMachine the resulting abstracted StateMachine
//             * @param bfBegin the start iterator of a BeliefState<Property,EventInfo> range
//             * @param bfEnd the end iterator of a BeliefState<Property,EventInfo> range
//             * @param abstractedStates the created states of abstractMachine in the order of the BeliefState range.
//             * @return true if the abstraction is a success. If not the state of the abstractedMachine
//             * is undetermined.
//             * 
//             * @pre machine should not be abstractedMachine
//             * @p [bfBegin,bfEnd) represents a set of belief states bs1, bs2, ... bsn.
//             * Each bsi is a set of State from the initial StateMachine 'machine'.
//             * The abstracted machine will contain n states. State si will represent 
//             * the states of bsi. A transition t of event e between state si and sj exists  
//             * in the abstracted machine iff there exists a transition t of event e
//             * between a state from bsi and a state from bsj in the original machine.
//             * The state si of the abtracted machine is initial as soon as one of
//             * the state of bsi is initial.  
//             * 
//             */
//            template<typename Property, typename EventInfo, typename BeliefStateIterator>
//            bool
//            abstract(const StateMachine<Property, EventInfo> & machine,
//                    StateMachine<Property, EventInfo> & abstractedMachine,
//                    BeliefStateIterator bfBegin, BeliefStateIterator bfEnd,
//                    std::vector<typename StateMachine<Property, EventInfo>::State> & abstractedStates) {
//                using Fsm = StateMachine<Property, EventInfo>;
//                using State = typename Fsm::State;
//                using Transition = typename Fsm::Transition;
//                if (machine == abstractedMachine) {
//                    return false;
//                }
//                std::unordered_map<State, std::unordered_set < size_t>> bsOfState;
//                std::vector<BeliefStateIterator> iterators;
//
//                for (auto it = bfBegin; it != bfEnd; ++it) {
//                    iterators.push_back(it);
//                    abstractedStates.push_back(abstractedMachine.newState());
//                    std::for_each(it->begin(), it->end(), [&](State s) {
//                        bsOfState[s].insert(iterators.size() - 1);
//                        if (machine.isInitial(s)) {
//                            abstractedMachine.setInitial(abstractedStates.back());
//                        }
//                    });
//                }
//                abstractedMachine.copyEventPropertyIds(machine);
//                std::for_each(bsOfState.begin(), bsOfState.end(),
//                        [&](const std::pair<State, std::unordered_set < size_t> > & bsState) {
//                            std::for_each(machine.outputTransitionBegin(bsState.first),
//                                    machine.outputTransitionEnd(bsState.first),
//                                    [&](Transition t) {
//                                        auto itTarget = bsOfState.find(t.target());
//                                        if (itTarget != bsOfState.end()) {
//                                            std::for_each(bsState.second.begin(),
//                                                    bsState.second.end(),
//                                                    [&](size_t sourceId) {
//                                                        std::for_each(itTarget->second.begin(),
//                                                                itTarget->second.end(),
//                                                                [&](size_t targetId) {
//                                                                    abstractedMachine.newTransition(abstractedStates[sourceId],
//                                                                            abstractedStates[targetId],
//                                                                            machine.getEvent(t));
//                                                                });
//                                                    });
//                                        }
//                                    });
//                        });
//                return true;
//            }

            template<typename Fsm, typename BeliefStateIterator, typename StateCreation>
            bool
            abstract(const Fsm & machine,
                    Fsm & abstractedMachine,
                    BeliefStateIterator bfBegin, BeliefStateIterator bfEnd,
                    StateCreation & creator) {
                std::vector<typename Fsm::State> abstractedStates;
                return abstract(machine, abstractedMachine, bfBegin, bfEnd, abstractedStates,creator);
            }

//            /**
//             * 
//             * @param machine a StateMachine
//             * @param abstractMachine the resulting abstracted StateMachine
//             * @param bfBegin the start iterator of a BeliefState<Property,EventInfo> range
//             * @param bfEnd the end iterator of a BeliefState<Property,EventInfo> range 
//             * @param stateManager StateInfoManger of the original machine
//             * @param abstractedStateManager StateInfoManger of the abstracted machine
//             * @param disjunction Definition of the way the minimal machine will hold the disjunction states from the 
//             * original machine.
//             * @return true if the abstraction is a success. If not the state of the abstractedMachine
//             * is undetermined.
//             * 
//             * @pre machine should not be abstractedMachine
//             * @p [bfBegin,bfEnd) represents a set of belief states bs1, bs2, ... bsn.
//             * Each bsi is a set of State from the initial StateMachine 'machine'.
//             * The abstracted machine will contain n states. State si will represent 
//             * the states of bsi. A transition t of event e between state si and sj exists  
//             * in the abstracted machine iff there exists a transition t of event e
//             * between a state from bsi and a state from bsj in the original machine.
//             * The state si of the abtracted machine is initial as soon as one of
//             * the state of bsi is initial.  
//             * 
//             */
//            template<typename Fsm,typename BeliefStateIterator>
//            bool
//            abstract(const StateMachine<StateProperty, EventId> & machine,
//                    StateMachine<StateProperty, EventId> & abstractedMachine,
//                    BeliefStateIterator bfBegin, BeliefStateIterator bfEnd,
//                    const StatePropertyManager<StateInfo, StateProperty> & stateManager,
//                    StatePropertyManager<StateInfo, StateProperty> & abstractedStateManager,
//                    const Disjunction & disjunction) {
//                using Fsm = StateMachine<StateProperty, EventId>;
//                std::vector<typename Fsm::State> abstractedStates;
//                bool result = abstract(machine, abstractedMachine, bfBegin, bfEnd, abstractedStates);
//
//                if (result) {
//                    size_t counter = 0;
//                    for (auto it = bfBegin; it != bfEnd; ++it) {
//                        auto begin = stateManager.statePropertyIdRangeStatePropertyIterator(machine.statePropertyIdRangeIterator(it->begin()));
//                        auto end = stateManager.statePropertyIdRangeStatePropertyIterator(machine.statePropertyIdRangeIterator(it->end()));
//                        abstractedMachine.setStatePropertyId(abstractedStates[counter],
//                                abstractedStateManager.statePropertyId(disjunction.operator()(begin, end)));
//                        ++counter;
//                    }
//                }
//                return result;
//            }

        }
    }
}



#endif /* __DIADES__AUTOMATA__EXPERIMENTAL__ABSTRACT__HH */