BddModel.hh

Go to the documentation of this file.

#ifndef __DIADES__SDMDL__BDDMODEL__HH
#define __DIADES__SDMDL__BDDMODEL__HH

#include <diades/automata/SynchronisationRules.hh>
#include <diades/automata/Event.hh>
#include <diades/sdmdl/Formula.hh>
#include <diades/sdmdl/BddComponent.hh>



namespace Diades
{
  namespace Sdmdl
  {

    using Diades::Automata::SynchronisationRules;
    using Diades::Automata::Event;
    
    class BddModel
    {

            
    public:
      static string typeName() { return "Diades::Sdmdl::BddModel"; }
      typedef Diades::Utils::Exception<BddModel> Exception;
      typedef Diades::Automata::SynchronisationRules::ComponentVector ComponentVector;
      typedef vector<BddComponent> BddComponentVector;
      typedef Variable::VariableVector VariableVector;
      typedef Formula::FormulaVector FormulaVector;
    private:
      const SynchronisationRules & _model;
      BddComponentVector _bddComponents;
      VariableFactory * _varFactory;
      FormulaFactory  * _formulas;
      VariableVector  _stateVariables;
      VariableVector  _nextStateVariables;
      Variable & _event;
      VariableVector _varSet;
      FormulaVector _observables;
      FormulaVector _isObs;
      FormulaVector _faults;
      FormulaVector _isFault;
      FormulaVector _setOfEvents;
      FormulaVector _events;
      vector< vector<size_t> > _supports;
      vector< vector<bool> > _booleanSupports;
      mutable FormulaVector _transitions;
      typedef BddComponent::SlStates SlStates;
      typedef BddComponent::SlTransitions SlTransitions;
      typedef BddComponent::SlEvents SlEvents;
    public:

      BddModel(const SynchronisationRules &  model,
               const set<Event> & observable,
               const set<Event> & faults);


      ~BddModel();


      FormulaFactory & formulaFactory()
      {
        return *_formulas;
      }
      
      const BddComponent & getComponent(BddComponentVector::size_type index) const
      {
        require(Exception,index < _bddComponents.size(),
                Diades::Utils::Msg("BddComponent::getComponent, out-of-range index '%1% >= %2%'") % index % _bddComponents.size());
        return _bddComponents[index];
      }
      

      BddComponent & getComponent(BddComponentVector::size_type index)
      {
        require(Exception,index < _bddComponents.size(),
                Diades::Utils::Msg("BddComponent::getComponent, out-of-range index '%1% >= %2%'") % index % _bddComponents.size());
        return _bddComponents[index];
      }




      const SlStates & initialStates() const;



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


      const SlTransitions & transitions() const;
      

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

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



      const VariableVector  & stateVariables() const
      {
        return _stateVariables;
      }

      const VariableVector  & nextStateVariables() const
      {
        return _nextStateVariables;
      }



      
    private:
      void encodeStateVariables();

      void encodeEvents();

      
      void setFaults(const set<Event> & faults);



      void setObservables(const set<Event> & observable);


      
      const SlStates & trigger(const SlStates & sources,
                               size_t eventIndex) const;


    };

  };
};

#endif