BddStateMachine.hh

Go to the documentation of this file.

/* 
 * @file   BddStateMachine.hh
 * @author Yannick Pencole, ypencole@laas.fr, LAAS-CNRS, Univ. Toulouse, FRANCE
 *
 * @date 3 November 2017, 12:44
 */

#ifndef __DIADES__SDMDL_EXPERIMENTAL__BDDSTATEMACHINE__HH__
#define __DIADES__SDMDL_EXPERIMENTAL__BDDSTATEMACHINE__HH__

#include <vector>
#include <unordered_map>
#include<diades/utils/Exceptions.hh>

#include<diades/sdmdl/Formula.hh>

namespace Diades
{
    namespace Sdmdl
    {
        namespace Experimental
        {

            class BddStateMachine
            {
            public:

                static string typeName()
                {
                    return "Diades::Sdmdl::Experimental::BddStateMachine";
                }

                using Exception = Diades::Utils::Exception<BddStateMachine>;

                using VariableVector = Variable::VariableVector;

                using FormulaVector = Formula::FormulaVector;

                using SlStates = Formula;

                using SlTransitions = Formula;

                using SlEvents = Formula;

                using Event = size_t;
            private:

                FormulaVector _behaviour;
                FormulaVector _initialState;

                mutable FormulaVector _noTransitions;


                std::unordered_map<std::string, FormulaVector> _eventOfValue;

                std::unordered_map<Event, FormulaVector> _formulaOfEvent;


                FormulaVector _events;
                FormulaVector _setOfEvents;
                VariableVector _stateVariable;
                VariableVector _nextStateVariable;
                VariableVector _eventVariable;
                FormulaFactory _internalFactory;

                mutable std::vector< std::reference_wrapper<FormulaFactory> > _factory;

            public:

                BddStateMachine() :
                _behaviour(),
                _initialState(),
                _noTransitions(),
                _eventOfValue(),
                _formulaOfEvent(),
                _events(),
                _setOfEvents(),
                _stateVariable(),
                _nextStateVariable(),
                _eventVariable(),
                _internalFactory(),
                                _factory()
                {
                    _factory.push_back(_internalFactory);
                    setInitialStates(_internalFactory.isFalse());
                    _behaviour.push_back(_internalFactory.isFalse());
                    _events.push_back(_internalFactory.isFalse());
                    _setOfEvents.push_back(_internalFactory.isFalse());
                };

                FormulaFactory & setFormulaFactory(FormulaFactory & factory)
                {
                    _factory.clear();
                    _factory.push_back(factory);
                    return _factory[0].get();
                }

                FormulaFactory & resetInternalFormulaFactory()
                {
                   // std::cout << "HELOLLLLjajoue" << std::endl;
                    _factory.clear();
                    
                    _factory.push_back(_internalFactory);
                    VariableVector varSet;
                    if (!_eventVariable.empty())
                    {
                        varSet.push_back(eventVariable());
                    }
                 //   std::cout << "_stateVar" << _stateVariable.size() << std::endl;
                    if (!_stateVariable.empty())
                    {
                        varSet.push_back(stateVariable());
                    }

                    if (!_nextStateVariable.empty())
                    {
                        varSet.push_back(nextStateVariable());
                    }
                    _internalFactory.reset(varSet);
                    setInitialStates(_internalFactory.isFalse());
                    _behaviour.clear();
                    _behaviour.push_back(_internalFactory.isFalse());
                    _events.clear();
                    _events.push_back(_internalFactory.isFalse());
                    _setOfEvents.clear();
                    _setOfEvents.push_back(_internalFactory.isFalse());
                    return _factory[0].get();
                }

                const Variable & eventVariable() const
                {
                    return _eventVariable[0].get();
                }

                Variable & eventVariable()
                {
                    return _eventVariable[0].get();
                }

                Variable & setEventVariable(Variable & event)
                {
                    _eventVariable.clear();
                    _eventVariable.push_back(event);
                    return _eventVariable[0].get();
                }

                Variable & stateVariable()
                {
                    return _stateVariable[0].get();
                }

                const Variable & stateVariable() const
                {
                    return _stateVariable[0].get();
                }

                Variable & setStateVariable(Variable & stateVar)
                {
                    _stateVariable.clear();
                    _stateVariable.push_back(stateVar);
                    return _stateVariable[0].get();
                }

                Variable & nextStateVariable()
                {
                    return _nextStateVariable[0].get();
                }

                const Variable & nextStateVariable() const
                {
                    return _nextStateVariable[0].get();
                }

                Variable & setNextStateVariable(Variable & nextStateVar)
                {
                    _nextStateVariable.clear();
                    _nextStateVariable.push_back(nextStateVar);
                    return _nextStateVariable[0].get();
                }

                ~BddStateMachine()
                {
                    _factory.clear();
                    _internalFactory.destroy();
                };

                const SlStates & initialStates() const
                {
                    require(Exception, _initialState.size() == 1,
                            "initialStates: not initialised");
                    return _initialState[0].get();
                }

                const SlStates & addInitialStates(const SlStates & newInitialStates);

                const SlStates & setInitialStates(const SlStates & newInitialStates)
                {
                    _initialState.clear();
                    _initialState.push_back(newInitialStates);
                    return _initialState.back();
                }

                const SlEvents & addEvent(Event evt)
                {
                    stringstream stream;
                    stream << evt;
                    auto & value = eventVariable().getValue(stream.str());
                    
                    _events.push_back(factory().newFormula(eventVariable(), value));
                    _eventOfValue[value.label()].push_back(_events.back());
                    _formulaOfEvent[evt].push_back(_events.back());
                    const SlEvents & currentSetOfEvent = _setOfEvents[0].get();
                    _setOfEvents.clear();
                    _setOfEvents.push_back(currentSetOfEvent || _events.back());
                    return _events.back();
                }

                const SlEvents & event(const Value & eventValue) const
                {
                    auto it = _eventOfValue.find(eventValue.label());
                    return (it->second)[0].get();
                }

                const SlEvents & event(Event evt) const
                {
                    auto it = _formulaOfEvent.find(evt);
                    return (it->second)[0].get();
                }

                const SlEvents & sources(const Value & sourceStateValue) const
                {
                    return _factory[0].get().newFormula(stateVariable(),sourceStateValue);
                }
                
                template<typename ValueIterator>
                const SlEvents & sources(ValueIterator first, ValueIterator last) const
                {
                    FormulaVector tmp;
                    if(first!=last)
                    {
                        tmp.push_back(_factory[0].get().isTrue());
                    }
                    else
                    {
                        tmp.push_back(_factory[0].get().isFalse());
                    }
                    while(first != last)
                    {
                        Formula & current = tmp[0].get();
                        tmp.clear();
                        tmp.push_back(current && sources(*first));
                        ++first;
                    }
                    return tmp[0].get();
                }
                
                
                const SlEvents & targets(const Value & targetStateValue) const
                {
                    return _factory[0].get().newFormula(nextStateVariable(),targetStateValue);
                }
                

                template<typename ValueIterator>
                const SlEvents & targets(ValueIterator first, ValueIterator last) const
                {
                    FormulaVector tmp;
                    if(first!=last)
                    {
                        tmp.push_back(_factory[0].get().isTrue());
                    }
                    else
                    {
                        tmp.push_back(_factory[0].get().isFalse());
                    }
                    while(first != last)
                    {
                        Formula & current = tmp[0].get();
                        tmp.clear();
                        tmp.push_back(current && targets(*first));
                        ++first;
                    }
                    return tmp[0].get();
                }
                
                const SlTransitions & addTransitions(const SlTransitions & transition)
                {
                    const SlTransitions & currentTransitions = _behaviour[0].get();
                    _behaviour.clear();
                    _behaviour.push_back(currentTransitions
                                         ||
                                         transition);
                    return transition;
                }

                const SlTransitions & transitions() const
                {
                    require(Exception, _behaviour.size() == 1,
                            "transitions: not initialised");
                    return _behaviour[0].get();
                }

                const SlTransitions & transitions(const SlEvents & event) const
                {
                    require(Exception, _behaviour.size() == 1,
                            "transitions: not initialised");
                    return _behaviour[0].get() && event;
                }


                const SlTransitions & noTransitions() const;

                const SlTransitions & transitions(const SlStates & sources, const SlEvents & events) const
                {
                    require(Exception, _behaviour.size() == 1,
                            "transitions: not initialised");
                    return (_behaviour[0].get() && sources && events);
                }

                const SlEvents & events() const
                {
                    return _setOfEvents[0].get();
                }

                template<typename EventIterator>
                const SlEvents & events(EventIterator first, EventIterator last)
                {
                    FormulaVector tmp;
                    tmp.push_back(factory().isFalse());
                    while(first != last)
                    {
                        const SlEvents & current = tmp[0].get();
                        tmp.clear();
                        tmp.push_back(current || event(*first));
                        ++first;
                    }
                    const SlEvents & result = tmp[0].get();
                    tmp.clear();
                    return result;
                }
                const SlStates & trigger(const SlStates & sources, const SlEvents & events) const;


                const SlStates & synchronousTrigger(const SlStates & sources,
                                                    const SlEvents & events) const;

                const SlStates & reach(const SlStates & sources, const SlEvents & nonObservables,
                                       const SlEvents & observations);

                FormulaFactory & factory()
                {
                    require(Exception, _factory.size() == 1,
                            "BddComponent::factory: not initialised");
                    return _factory[0].get();
                }



                void clear();

            };


        }
    }
}


#endif