EncodedInstance.hh

Go to the documentation of this file.

#ifndef __DIADES__ALTARICA_ENCODEDINSTANCE__HH
#define __DIADES__ALTARICA_ENCODEDINSTANCE__HH

#include<diades/graph/Graph.hh>
#include<diades/graph/NodeMap.hh>
#include<diades/graph/EdgeMap.hh>
#include<diades/altarica/Node.hh>

namespace Diades
{
  namespace Altarica
  {

        class EncodedInstanceData
        {
        public:
          typedef Diades::Graph::Graph Fsm;   
          typedef Diades::Graph::Node  State; 
          typedef Diades::Graph::Edge  Trans; 
          typedef Diades::Graph::NodeMap<Formula> StateFormulaMap; 
          typedef Diades::Graph::EdgeMap<Event> TransEventMap; 
          typedef list<Formula>::const_iterator AssertionIterator; 
        
        private:
          Node  _node;
          list<Formula> _invariant;
          bool _invariantComputed;
          Formula _initialisation;
          bool _initialisationComputed;
          list<EncodedTransition *> _transitions;
          bool _transitionsComputed;
          Fsm _fsm;
          State _initial;
          StateFormulaMap _configurationFormula;
          StateFormulaMap _stateFormula;
          TransEventMap  _tranEvents;
          string _logs;
          State _hole;
        
        public:
          EncodedInstanceData(Node instance):_node(instance),
                                                                                                 _invariant(),
                                                                                                 _invariantComputed(false),
                                                                                                 _initialisation(),
                                                                                                 _initialisationComputed(false),
                                                                                                 _transitions(),
                                                                                                 _transitionsComputed(false),
                                                                                                 _fsm(),
                                                                                                 _initial(),
                                                                                                 _configurationFormula(),
                                                                                                 _stateFormula(),
                                                                                                 _tranEvents(),
                                                                                                 _logs(),
                                                                                                 _hole()
          {
                _fsm.init();
                _configurationFormula.init(_fsm);
                _stateFormula.init(_fsm);
                _tranEvents.init(_fsm);
          }

          ~EncodedInstanceData()
          {
                _fsm.destroy();
          }
          
          const string & logs() const
          {
                return _logs;
          }
        
          Node nodeInstance() const { return _node; }

          State initialState();

          Formula getStateFormula(State state) const
          {
                if(!state.valid() || !(state.owner()==_fsm))
                  {
                        return Formula();
                  }
                return _stateFormula[state];
          }
        
          Formula getConfigurationFormula(State state) const
          {
                if(!state.valid() || !(state.owner()==_fsm))
                  {
                        return Formula();
                  }
                return _configurationFormula[state];
          }


          Formula getFormula(State state) const
          {
                if(!state.valid() || !(state.owner()==_fsm))
                  {
                        return Formula();
                  }
                return getStateFormula(state) && getConfigurationFormula(state);
          }     

        


          State getState(Formula formula) const;

          typedef Diades::Graph::NodeIterator StateIterator; 
          typedef Diades::Graph::EdgeIterator TransIterator; 

          StateIterator stateBegin() const
          {
                return _fsm.nodeBegin();
          }
        
          StateIterator stateEnd() const
          {
                return _fsm.nodeEnd();
          }


          TransIterator transBegin() const
          {
                return _fsm.edgeBegin();
          }
        
          TransIterator transEnd() const
          {
                return _fsm.edgeEnd();
          }
        
        
          void getNextStates(State state,const Event & event, set<State> & successors);

          AssertionIterator assertionBegin() const
          {
                return _invariant.begin();
          }
          AssertionIterator assertionEnd() const
          {
                return _invariant.end();
          }
          const Event & getEvent(Trans t) const
          {
                return _tranEvents[t];
          }
        };

  
        class EncodedInstance
        {
        public:
          typedef Diades::Graph::Graph Fsm;   
          typedef Diades::Graph::Node  State; 
          typedef Diades::Graph::Edge  Trans; 
          typedef Diades::Graph::NodeMap<Formula> StateFormulaMap; 
          typedef Diades::Graph::NodeIterator StateIterator; 
          typedef Diades::Graph::EdgeIterator TransIterator; 
          typedef EncodedInstanceData::AssertionIterator AssertionIterator; 
        
        private:
          EncodedInstanceData * _data; 
        public:

          EncodedInstance():_data(0){}
          EncodedInstance(EncodedInstanceData * data):_data(data){}
          EncodedInstance(const EncodedInstance & instance):_data(instance._data){}

          EncodedInstance & operator=(const EncodedInstance & instance)
          {
                if(this != &instance)
                  {
                        _data = instance._data;
                  }
                return *this;
          }
        
          Formula getFormula(State state) const
          {
                if(!valid())
                  {
                        return Formula();
                  }
                return _data->getFormula(state);
          }
          Formula getStateFormula(State state) const
          {
                if(!valid())
                  {
                        return Formula();
                  }
                return _data->getStateFormula(state);
          }




          Formula getConfigurationFormula(State state) const
          {
                if(!valid())
                  {
                        return Formula();
                  }
                return _data->getConfigurationFormula(state);
          }



        
          Node nodeInstance() const {
                if(!valid())
                  {
                        return Node();
                  }
                return _data->nodeInstance();
          }

          bool valid() const
          {
                return _data!=0;
          }

          bool operator==(const EncodedInstance & instance)
          {
                return _data==instance._data;
          }


          bool operator!=(const EncodedInstance & instance)
          {
                return !((*this)==instance);
          }

          bool operator<(const EncodedInstance & instance)
          {
                return _data<instance._data;
          }

          State initialState()
          {
                if(!valid())
                  {
                        return State();
                  }
                return _data->initialState();
          }


          const string & logs() const
          {
                return _data->logs();
          }


          State getState(Formula formula) const
          {
                if(!valid())
                  {
                        return State();
                  }
                return _data->getState(formula);
          }




          StateIterator stateBegin() const
          {
                return _data->stateBegin();
          }
        
          StateIterator stateEnd() const
          {
                return _data->stateEnd();
          }
        
          TransIterator transBegin() const
          {
                return _data->transBegin();
          }
        
          TransIterator transEnd() const
          {
                return _data->transEnd();
          }
        
          void getNextStates(State state,const Event &  event, set<State> & successors)
          {
                _data->getNextStates(state,event,successors);
          }


          const Event & getEvent(Trans t) const
          {
                return _data->getEvent(t);
          }


          AssertionIterator assertionBegin() const
          {
                return _data->assertionBegin();
          }
          AssertionIterator assertionEnd() const
          {
                return _data->assertionEnd();
          }

        
        };

  


        EncodedInstance createEncodedNode(Node instance);
        void unfold(EncodedInstance instance);
        void export2dot(EncodedInstance instance, const string & fileName);
  };
};
#endif