BddComponent.hh

Go to the documentation of this file.

#ifndef __DIADES__SDMDL__BDDCOMPONENT__HH
#define __DIADES__SDMDL__BDDCOMPONENT__HH

#include <vector>
#include <unordered_map>
#include <diades/automata/Component.hh>
#include <diades/automata/SynchronisationRules.hh>
#include <diades/sdmdl/Formula.hh>

namespace Diades
{
  namespace Sdmdl
  {
    using std::unordered_map;
    using std::vector;
    using Diades::Automata::Event;
    using Diades::Automata::Transition;
    using Diades::Automata::Component;
    using Diades::Automata::SynchronisationRules;

    class BddComponent
    {
    public:
      static string typeName() { return "Diades::Sdmdl::BddComponent"; }
      typedef Diades::Utils::Exception<BddComponent> Exception;
      typedef Variable::VariableVector VariableVector;
      typedef Formula::FormulaVector FormulaVector;
      typedef Formula SlStates;
      typedef Formula SlTransitions;
      typedef Formula SlEvents;
      
    private:

      FormulaVector    _behaviour;
      FormulaVector    _initialState;
      mutable FormulaVector    _noTransitions;
      unordered_map<string,size_t> _eventLabels;
      FormulaVector    _events;
      FormulaVector    _setOfEvents;
      VariableVector   _stateVariable;
      VariableVector   _nextStateVariable;
      VariableVector   _eventVariable;
      
      mutable vector< reference_wrapper<FormulaFactory> >  _factory;
      
    public:
      
      BddComponent():_behaviour(),_initialState(),_eventLabels(),
                     _events(),_setOfEvents(),_stateVariable(),_nextStateVariable(),
                     _eventVariable(),_factory(){};



      ~BddComponent(){};



      void encodeComponent(FormulaFactory & factory,
                           const SynchronisationRules & model,
                           const Component & component,
                           Variable & stateVar,
                           Variable & nextStateVar,
                           Variable & event);



      void encodeComponent(FormulaFactory & factory,
                           const Component & component,
                           Variable & stateVar,
                           Variable & nextStateVar,
                           Variable & event);


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


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

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

      
      const SlTransitions & noTransitions() const;



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

      
      const SlEvents & events(std::set<Event> & events);


      const SlEvents & event(const Event & event);

      
      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);

      
    private:

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

      
      void clear();




      void encodeEventLabels(const SynchronisationRules & model,
                             const Component & component);

      void encodeEventLabels(const Component & component);

      
      void encodeInitialStates(const Component & component);


      void encodeTransitions(const Component & component);

      const Formula &  encodeTransition(const Component & component,
                                        const Transition & transition);

    };
  };
};

#endif