UnfoldingState.hh

Go to the documentation of this file.

#ifndef UNFOLDINGSTATE_H_
#define UNFOLDINGSTATE_H_

#include<list>
#include<vector>
#include"Variable.hh"
#include"Formula.hh"
#include"ComponentType.hh"

using namespace std;


namespace Diades
{
  namespace Sdmdl
  {

        class UnfoldingState
        {
        private:
          vector<Formula::ConstReference> _assignment;
          ComponentType *  _comp; 
          int * _cube;
          int _size;
        
        
        
        public:
          UnfoldingState():_comp(0),_cube(0),_size(0) {}
          bool valid() const { return (_comp != 0 && !_assignment.empty() && !_assignment[0].get().isNull()); }
          UnfoldingState(ComponentType & component);
          UnfoldingState(ComponentType & component, const Formula & f);
          UnfoldingState(const UnfoldingState & state);
          void trigger(Rule & rule, set<UnfoldingState> & targets);
          virtual ~UnfoldingState();
          UnfoldingState & operator=(const UnfoldingState & state);
          bool operator == (const UnfoldingState & state) const;
          string label() const;
          const Formula & formula() const { return _assignment[0]; }
          string observableLabel() const;
          bool satisfy(const Rule & rule);
          bool operator<(const UnfoldingState & state) const;
          friend ostream & operator << (ostream & os, const UnfoldingState & state);
        
          int * cube() const { return _cube; }
          int cubeSize() const { return _size; }
        };




        
  };
};

#endif /*UNFOLDINGSTATE_H_*/