pfed.h

Go to the documentation of this file.

// -*- Mode: C++; c-file-style: "stroustrup"; c-basic-offset: 4; -*-
///////////////////////////////////////////////////////////////////////////////
//
// This file is a part of the UPPAAL toolkit.
// Copyright (c) 2006, Uppsala University and Aalborg University.
// All right reserved.
//
///////////////////////////////////////////////////////////////////////////////

#ifndef DBM_PFED_H
#define DBM_PFED_H

#include <stdexcept>
#include "dbm/Valuation.h"
#include "dbm/priced.h"
#include "base/slist.h"

namespace dbm
{
    class pdbm_t;

    /**
     * A priced federation is a list of priced DBMs.
     * 
     * Priced federations implement copy on write using reference
     * counting.
     */
    class pfed_t
    {
    public:
        typedef std::slist<PDBM>::const_iterator const_iterator;

    protected:
        typedef std::slist<PDBM>::iterator iterator;

        struct pfed_s
        {
            std::slist<PDBM> zones;
            uint32_t count;
            cindex_t dim;
        };

        static std::allocator<pfed_s> alloc;

        /** Pointer to record holding the federation. */
        struct pfed_s *ptr;

        /** Increment reference count. */
        void incRef();

        /** Decrement reference count. */
        void decRef();

        /** Prepare federation for modification. */
        void prepare();

        /** Returns a mutable iterator to the beginning of the federation. */
        iterator beginMutable();

        /** Returns a mutable iterator to the end of the federation. */
        iterator endMutable();

        /**
         * Erases a DBM from the federation and returns an itertor to the
         * successor element.
         */
        iterator erase(iterator);

        /**
         * Adds \a pdbm to the federation. The reference count on pdbm
         * is incremented by one.
         */
        void add(const PDBM pdbm, size_t dim);    
    public:

        /** Allocate empty priced federation of dimension 0. */
        pfed_t();

        /** Allocate empty priced federation of dimension \a dim. */
        explicit pfed_t(cindex_t dim);

        /**
         * Allocate a priced federation of dimension \a dim initialised to
         * \a pdbm.
         */
        pfed_t(const PDBM pdbm, cindex_t dim);

        /** The copy constructor implements copy on write. */
        pfed_t(const pfed_t &);

        /**
         * The destructor decrements the reference count and deallocates
         * the priced DBM when the count reaches zero.
         */
        ~pfed_t();

        /**
         * Constrain x(i) to value. 
         *
         * @return Returns true if non-empty after operation.
         */
        bool constrain(cindex_t i, uint32_t value);

        /**
         * Constrain federation to valuations satisfying x(i) - x(j) ~
         * constraint.
         *
         * @return Returns true if non-empty after operation.
         */
        bool constrain(cindex_t i, cindex_t j, raw_t constraint);

        /**
         * Constrain federation to valuations satisfying x(i) - x(j) ~
         * (b, isStrict).
         *
         * @return Returns true if non-empty after operation.
         */
        bool constrain(cindex_t i, cindex_t j, int32_t b, bool isStrict);

        /**
         * Constrain federation to valuations satisfying the
         * constraints.
         *
         * @param constraints Array of length \a n of constraints.
         * @param n           length of \a constraints.
         * @pre               n > 0
         * @return Returns true if non-empty after operation.
         */
        bool constrain(const constraint_t *constraints, size_t n);

        /**
         * Constrain federation to valuations satisfying \a c.
         *
         * @return Returns true if non-empty after operation.
         */
        bool constrain(const constraint_t& c);

        /** Returns the infimum of the federation. */
        int32_t getInfimum() const;

        /**
         * Check if the federation satisfies a given constraint.        
         *
         * @return Returns true if the federation satisfies \a c.
         */
        bool satisfies(const constraint_t& c) const;

        /**
         * Check if the federation satisfies a given constraint.        
         *
         * @return Returns true if the federation satisfies x(i) -
         * x(j) ~ constraint.
         */
        bool satisfies(cindex_t i, cindex_t j, raw_t constraint) const;

        /** Returns true iff the federation is empty. */
        bool isEmpty() const;

        
        bool isUnbounded() const;

        /** Contains a hash of the federation. */
        uint32_t hash(uint32_t seed) const;

        /** Returns true iff the federation contains \v. */
        bool contains(const DoubleValuation &v) const;

        /** Returns true iff the federation contains \v. */
        bool contains(const IntValuation &v) const;

        /** Delay with the current delay rate. */
        void up();

        /** Delay with rate \a rate. */
        void up(int32_t rate);

        /** Set x(clock) to \a value. */
        void updateValue(cindex_t clock, uint32_t value);

        /** 
         * Set x(clock) to \a value. x(zero) must be on a zero-cycle with
         * x(clock).
         */
        void updateValueZero(cindex_t clock, int32_t value, cindex_t zero);

        void extrapolateMaxBounds(int32_t *max);
        void diagonalExtrapolateMaxBounds(int32_t *max);
        void diagonalExtrapolateLUBounds(int32_t *lower, int32_t *upper);

        void incrementCost(int32_t value);
    
        int32_t getCostOfValuation(const IntValuation &valuation) const;
        void relax();

        void freeClock(cindex_t clock);

        /**
         * Resets the federation to the federation containing only the
         * origin, with a cost of 0.
         */
        void setZero();

        /**
         * Resets the federation to the federation containing all
         * valuations, with a cost of 0.
         */
        void setInit();

        /**
         * Resets the federation to the empty federation.
         */
        void setEmpty();

        /**
         * Returns an iterator to the first zone of the federation.
         */
        const_iterator begin() const;

        /**
         * Returns an iterator to the position after the last zone of
         * the federation.
         */
        const_iterator end() const;

        bool operator == (const pfed_t &) const;

        /** Assignment operator. */
        pfed_t &operator = (const pfed_t &);

        /** Assignment operator. */
        pfed_t& operator = (const PDBM);

        /** Union operator. */
        pfed_t &operator |= (const pfed_t &);

        /** Union operator. */
        pfed_t &operator |= (const PDBM);

        /** Not implemented. */
        pfed_t &operator -= (const pfed_t &);

        /** Not implemented. */
        pfed_t &operator += (const pfed_t &);

        /** Not implemented. */
        pfed_t &operator &= (const pfed_t &);

        /** Not implemented. */
        bool intersects(const pfed_t &) const;

        /** Not implemented. */
        pfed_t operator & (const pfed_t& b) const;

        /** Not implemented. */
        pfed_t operator - (const pfed_t& b) const;

        /** Not implemented. */
        void down();

        /** Not implemented. */
        int32_t getUpperMinimumCost(cindex_t) const;

        /** Not implemented. */
        void relaxUp();

        /** Not implemented. */
        void getValuation(DoubleValuation& cval, bool *freeC = NULL) const;

        /** Not implemented. */
        void swapClocks(cindex_t, cindex_t);

        /** Not implemented. */        
        void splitExtrapolate(const constraint_t *, const constraint_t *,
                              const int32_t *);

        /**
         * Relation between two priced federations: SUBSET is returned
         * if all zones of this federation are contained in some zone
         * of fed. SUPERSET is returned if all zones of \a fed are
         * contained in some zone of this federation. EQUAL is
         * returned if both conditions are true. DIFFERENT is returned
         * if none of them are true.
         *
         * Notice that this implementation of set inclusion is not
         * complete in the sense that DIFFERENT could be returned even
         * though the two federations are comparable.
         */
        relation_t relation(const pfed_t &fed) const;

        /**
         * Returns the infimum of the federation given a partial
         * valuation.
         */
        int32_t getInfimumValuation(IntValuation &valuation, const bool *free = NULL) const;

        /** Returns the number of zones in the federation. */
        size_t size() const;

        /** Returns the dimension of the federation. */
        size_t getDimension() const;

        /**
         * Implementation of the free up operation for priced
         * federations.
         *
         * @see pdbm_freeUp
         */
        void freeUp(cindex_t);

        /**
         * Implementation of the free down operation for priced
         * federations.
         *
         * @see pdbm_freeDown
         */
        void freeDown(cindex_t);

        template <typename Predicate>
        void erase_if(Predicate p);

        template <typename Predicate>
        void erase_if_not(Predicate p);
        
        // The following operate on the first zone only.

        /**
         * Returns the bound on x(i) - x(j) of the first zone of the
         * federation.
         *
         * @pre size() == 1
         */
        raw_t operator () (cindex_t i, cindex_t j) const;

        /**
         *
         * @pre size() == 1
         */
        int32_t getRate(cindex_t) const;

        /**
         *
         * @pre size() == 1
         */
        size_t analyzeForMinDBM(uint32_t *bitMatrix) const;

        /**
         *
         * @pre size() == 1
         */
        int32_t getOffsetCost() const;

        /**
         *
         * @pre size() == 1
         */
        int32_t getSlopeOfDelayTrajectory() const;

        void setOffsetCost(int32_t);
        void setRate(cindex_t, int32_t);

        /** @see dbm_writeToMinDBMWithOffset() */
        int32_t *writeToMinDBMWithOffset(bool minimizeGraph,
                                         bool tryConstraints16,
                                         allocator_t c_alloc,
                                         uint32_t offset) const;


        static size_t getSizeOfMinDBM(size_t dimension, const int32_t *);

        static pfed_t readFromMinDBM(size_t dimension, const int32_t *);

        /** @see pdbm_relationWithMinDBM() */
        relation_t relation(const int32_t *, raw_t *) const;
        
        /**
         * Returns true and a clock in \a result that is on a zero
         * cycle with \a clock or false if no such clock exists.
         */
        bool isOnZeroCycle(cindex_t clock, cindex_t &result) const;

        const pfed_t &const_dbmt() const;
    };

    template <typename Predicate>
    inline void pfed_t::erase_if(Predicate p)
    {
        iterator first = beginMutable();
        iterator last = endMutable();
        while (first != last)
        {
            if (p(*first))
            {
                first = erase(first);
            }
            else
            {
                ++first;
            }
        }
    }

    template <typename Predicate>
    void pfed_t::erase_if_not(Predicate p) 
    {
        iterator first = beginMutable();
        iterator last = endMutable();
        while (first != last)
        {
            if (p(*first))
            {
                ++first;
            }
            else
            {
                first = erase(first);
            }
        }
    }


    inline pfed_t::pfed_t(const pfed_t &pfed) : ptr(pfed.ptr)
    {
        incRef();
    }

    inline pfed_t::~pfed_t()
    {
        assert(ptr->count > 0);
        decRef();
    }

    inline pfed_t::iterator pfed_t::beginMutable()
    {
        assert(ptr->count <= 1);
        return ptr->zones.begin();
    }

    inline pfed_t::iterator pfed_t::endMutable()
    {
        assert(ptr->count <= 1);
        return ptr->zones.end();
    }

    inline pfed_t::const_iterator pfed_t::begin() const
    {
        return ptr->zones.begin();
    }
 
    inline pfed_t::const_iterator pfed_t::end() const
    {
        return ptr->zones.end();
    }

    inline size_t pfed_t::getDimension() const
    {
        return ptr->dim;
    }

    inline size_t pfed_t::size() const
    {
        return ptr->zones.size();
    }

    inline void pfed_t::incRef()
    {
        ptr->count++;
    }


    inline bool pfed_t::isEmpty() const
    {
        return ptr->zones.empty();
    }

    inline const pfed_t &pfed_t::const_dbmt() const 
    {
        assert(size() == 1);
        return *this;
    }

    inline pfed_t& pfed_t::operator = (const PDBM pdbm)
    {
        *this = pfed_t(pdbm, ptr->dim);
        return *this;
    }

    inline bool pfed_t::constrain(cindex_t i, cindex_t j, int32_t b, bool isStrict)
    {
        return constrain(i, j, dbm_boundbool2raw(b, isStrict));
    }

    inline bool pfed_t::constrain(const constraint_t& c)
    {
        return constrain(c.i, c.j, c.value);
    }

    inline bool pfed_t::satisfies(const constraint_t& c) const 
    {
        return satisfies(c.i, c.j, c.value);
    }
}

#endif

---