Trace.hh

Go to the documentation of this file.

#ifndef __DIADES__AUTOMATA__TRACE_HH
#define __DIADES__AUTOMATA__TRACE_HH

#include<diades/utils/Exceptions.hh>
#include<diades/graph/GraphInt.hh>
#include<diades/automata/Component.hh>
#include<diades/automata/ObservableComponent.hh>

namespace Diades {

    namespace Automata {

        class Trace : public Component {
        private:
            unordered_set<State> _acceptors; 
            Diades::Graph::NodeMap<int> _status; 

        public:

            static string typeName() {
                return "Automata::Trace";
            }
            typedef Diades::Utils::Exception<Trace> Exception;



            /*************** CONSTRUCTORS **********************************/

            Trace();

            /************** TRACE OPERATORS *******************************/

        private:
            
            void pruneSpuriousStates();

            void extractUnobservableBehaviours(const Component & comp, 
                    const ObservableMask & mask,
                    const unordered_map<State, State> & sources,
                    unordered_map<State, State> & targets,
                    unsigned level);

            bool extractBehaviours(const Component & comp,
                    const ObservableMask & mask,
                    const unordered_map<State, State> & sources,
                    const Event & obs,
                    unordered_map<State, State> & targets,
                    unsigned level);

        public:

            bool extract(const Component & comp, const ObservableMask & mask,
                    const vector<Event> & observations);




            void extract(const Component & comp, Event event, bool presence);

            void extract(const Trace & trace, const Trace & projection, const set<Event> & projectedEvents);



            void extractObservableTrace(const ObservableComponent & comp, Event event, bool presence);


            void extractAllObservableTraces(const ObservableComponent & comp);








            bool project(const Trace & trace,
                    const set<Event> & projectedEvents);



            bool intersection(const Trace & trace1, const Trace & trace2);


            bool substract(const Trace & trace1, const Trace & trace2);

            bool complement(const Trace & trace, const set<Event> & events);


            bool compose(const Trace & trace1, const Trace & trace2, const set<Event> & events);


            State makeComplete();


        private:

            void computeTrace(const Component & comp, Event event, bool presence);


        public:

            /*************** MISC *******************************************/

            bool isFinite(list< set<Event> > & combinations) const;




            bool isContinuationFinite() const;

            State initialState() const {
                try {
                    return *initialStateBegin();
                } catch (exception & e) {
                    throw Exception("initialState(): unable to get access to the initial state", e);
                }
                return State();
            }


            /**************** ACCEPTORS MANAGEMENT **************************/

            bool isAcceptor(State state) const {
                try {
                    require(Exception, state.valid(), "isAcceptor(), invalid state");
                    require(Exception, &state.owner() == &behaviour(), "isAcceptor(), the state does not belong to this trace");
                    return (state.valid()
                            && (&state.owner() == &behaviour())
                            && (_status[state] == 1));
                } catch (exception & e) {
                    throw Exception("isAcceptor(): unable to get the accepting status of the state", e);
                }
            }

            void setAcceptor(State state) {
                try {
                    require(Exception, state.valid(), "setAcceptor(), invalid state");
                    require(Exception, &state.owner() == &behaviour(), "setAcceptor(), the state does not belong to this trace");
                    if (state.valid() && (&state.owner() == &behaviour())) {
                        if (_status[state] == 0) {
                            _status[state] = 1;
                            _acceptors.insert(state);
                        }
                    }
                } catch (exception & e) {
                    throw Exception("setAcceptor(): unable to get the accepting status of the state", e);
                }
            }

            void setNonAcceptor(State state) {
                try {
                    require(Exception, state.valid(), "setNonAcceptor(), invalid state");
                    require(Exception, &state.owner() == &behaviour(), "setNonAcceptor(), the state does not belong to this trace");
                    if (state.valid() && (&state.owner() == &behaviour())) {
                        if (_status[state] == 1) {
                            _status[state] = 0;
                            _acceptors.erase(state);
                        }
                    }
                } catch (exception & e) {
                    throw Exception("setNonAcceptor(): unable to get the accepting status of the state", e);
                }
            }

            unordered_set<State>::const_iterator beginOfAcceptorStates() const {
                try {
                    return _acceptors.begin();
                } catch (exception & e) {
                    throw Exception("beginOfAcceptorStates(): unable to get the iterator", e);
                }
                return _acceptors.begin();
            }

            unordered_set<State>::const_iterator endOfAcceptorStates() const {
                try {
                    return _acceptors.end();
                } catch (exception & e) {
                    throw Exception("endOfAcceptorStates(): unable to get the iterator", e);
                }
                return _acceptors.end();
            }

            void makeAllAcceptors() {
                try {
                    for (StateIterator stateIt = stateBegin();
                            stateIt != stateEnd();
                            ++stateIt) {
                        setAcceptor(*stateIt);
                    }
                } catch (exception & e) {
                    throw Exception("makeAllAcceptors(): unable to set the states as acceptor states", e);
                }
            }

            void makeAllNonAcceptors() {
                try {
                    for (StateIterator stateIt = stateBegin();
                            stateIt != stateEnd();
                            ++stateIt) {
                        setNonAcceptor(*stateIt);
                    }
                } catch (exception & e) {
                    throw Exception("makeAllNonAcceptors(): unable to set the states as non-acceptor states", e);
                }
            }

            const unordered_set<State> & acceptors() const {
                return _acceptors;
            }

            virtual void mergeInfoStates(const vector<const Component *> & components, const vector<State> & states, State currentState);

            /**************************** GENERAL METHODS ******************/

            void clear() {
                Component::clear();
                _acceptors.clear();
                _status.init(behaviour());
            }

        public:
            void trace2dot(const string & filename) const;



        };






    };

};

#endif