Vdd.hh

Go to the documentation of this file.

/*
 * Vdd.hh
 *
 *  Created on: 28 août 2008
 *      Author: ypencole
 */

#ifndef __DIADES__PETRI__VDD__HH__
#define __DIADES__PETRI__VDD__HH__

#include <vector>
#include <diades/utils/Assertion.hh>
#include <diades/petri/Net.hh>


namespace Diades
{
  namespace Petri
  {
        class VddInvalid : public runtime_error, public domain_error {
        public:
          VddInvalid(const string& whatArg) : runtime_error(whatArg),  domain_error(whatArg){
                cerr << "EXCEPTION Vdd -> " << whatArg << endl;
          }
        };

        class VddFactory;


        class Vdd
        {
        private:

          Place _place;
          int _tokens;
          const Vdd * _eq;
          const Vdd * _sup;
          unsigned _id;
          VddFactory * _factory;


        public:
          Vdd():_place(),_tokens(0),_eq(0),_sup(0),_id(0),_factory(0){}

          Vdd(VddFactory * factory):_place(),_tokens(0),_eq(0),_sup(0),_id(0),_factory(factory){}

        private:
          Vdd(Place p, int tokens, const Vdd * eq, const Vdd * sup, unsigned id, VddFactory * factory):
                _place(p), _tokens(tokens), _eq(eq), _sup(sup),  _id(id), _factory(factory){
                require(VddInvalid,p.valid(),"Vdd: invalid place");
                require(VddInvalid,id > 0, "Vdd: null id");
                require(VddInvalid,tokens >= 0, "Vdd: negative number of tokens");
          }

        public:

          virtual ~Vdd(){}

          unsigned id() const { return _id; }

          int tokens() const { return _tokens; }

          Place place() const { return _place; }

          const Vdd * eq() const { return _eq; }



          const Vdd * sup() const { return _sup; }

          int getCardinality() const;

          bool isEmpty() const;

          bool holds(Place p, int tokens) const;


          bool isNull() const;



          bool valid() const
          {
                return (tokens() >= 0) && (id() > 0) && (place().valid()) && ( (eq()->isEmpty()) ||  (eq()->isNull()) || ( eq()->valid()  && (eq()->place() > place()) ))
                  && ( (sup()->isEmpty()) ||  (sup()->isNull()) || ( sup()->valid()  && (sup()->place() == place()) && (sup()->tokens() > tokens()) ));
          }

          friend class VddFactory;

        };

        class VddFactory
        {

        private:
          const Net * _net;
          vector<  vector<  unordered_map<unsigned, unordered_map <unsigned, Vdd *> > > > _vdd;
          vector<Vdd *> _table;
          vector<int> _card;
          Vdd * _empty;
          Vdd * _null;

        public:
          VddFactory(const Net & net):
                _net(&net),
                _vdd(net.numberOfPlaces()+1),
                _table(2),_card(2),
                _empty(0),_null(0){
                _table[0] = new Vdd(this);
                _table[1] = new Vdd(this);
                _empty = _table[1];
                _null = _table[0];
                _empty->_id = 1;
                _null->_id = 0;
                _card[0] = 1; // null vector represents the marking  0 0 0 0
                _card[1] = 0; // empty vector represents "empty set"
          }

          virtual ~VddFactory();

          const Vdd * getVdd(Place place, int tokens, const Vdd * eq, const Vdd * sup);


          int getCardinality(const Vdd * vdd);


          bool holds(const Vdd * vdd, Place p, int tokens) const;


          const Vdd * getVdd(const Vdd * vdd, const Zsl * zsl);




          const Vdd * getVdd(const set<Place> & marking);

          bool isEmpty(const Vdd * vdd) const { return vdd == _empty; }


          bool isNull(const Vdd * vdd) const { return vdd == _null; }


          const Vdd * getVdd(unsigned id) { if(id >= _table.size()) { return 0; } return _table[id]; }

          const Vdd * addZslToVdd(const Vdd * vdd, const Zsl * zsl);

          const Vdd * getFirable(const Vdd * vdd, const Zsl * zsl);


          const Vdd * getUnion(const Vdd * vdd1,  const Vdd * vdd2);

          const Vdd * getIntersection(const Vdd * vdd1,  const Vdd * vdd2);

          const Net * owner() const { return _net; }


          void printDot(const string & fileName) const;

          void printDot(const Vdd * vdd, const string & fileName) const;


          const Vdd * empty() const { return _empty; }

          const Vdd * null() const { return _null; }
        };
  };
};

#endif /* VDD_HH_ */