dbm::dbm_t

dbm::dbm_t Class Reference

#include <fed.h>

List of all members.

Public Types

enum { MAX_DIM_POWER = 15, MAX_DIM = ((1 << MAX_DIM_POWER) - 1) }

Public Member Functions

dbm_t (cindex_t dim=1)

Initialize a dbm_t to empty DBM of a given dimension.

dbm_t (const dbm_t &arg)

Standard copy constructor.

dbm_t (const raw_t *arg, cindex_t dim)

Copy constructor from a DBM matrix.

~dbm_t ()

cindex_t getDimension () const

std::string toString (const ClockAccessor &) const

void setDimension (cindex_t dim)

Change the dimension of this DBM.

bool isEmpty () const

void setEmpty ()

Empty this DBM.

void nil ()

Short for setDimension(1), has the effect of deallocating the DBM.

bool hasZero () const

uint32_t hash (uint32_t seed=0) const

bool sameAs (const dbm_t &arg) const

void intern ()

Try to share the DBM.

void copyFrom (const raw_t *src, cindex_t dim)

Copy from a DBM.

void copyTo (raw_t *dst, cindex_t dim) const

Copy to a DBM.

const raw_t * operator() () const

raw_t operator() (cindex_t i, cindex_t j) const

const raw_t * operator[] (cindex_t i) const

raw_t * getDBM ()

size_t analyzeForMinDBM (uint32_t *bitMatrix) const

Compute the minimal set of constraints to represent this DBM.

int32_t * writeToMinDBMWithOffset (bool minimizeGraph, bool tryConstraints16, allocator_t c_alloc, size_t offset) const

Compute & save the minimal set of constraints.

int32_t * writeAnalyzedDBM (uint32_t *bitMatrix, size_t nbConstraints, BOOL tryConstraints16, allocator_t c_alloc, size_t offset) const

Similar to writeToMinDBMWithOffset but works with a pre-analyzed DBM.

relation_t relation (mingraph_t ming, raw_t *unpackBuffer) const

Relation with a mingraph_t,.

dbm_t & operator= (const dbm_t &)

Overload of standard operators.

dbm_t & operator= (const raw_t *)

bool operator== (const dbm_t &) const

Comparisons have the semantics of set inclusion.

bool operator== (const fed_t &) const

bool operator== (const raw_t *) const

bool operator!= (const dbm_t &) const

bool operator!= (const fed_t &) const

bool operator!= (const raw_t *) const

bool operator< (const dbm_t &) const

bool operator< (const fed_t &) const

bool operator< (const raw_t *) const

bool operator> (const dbm_t &) const

bool operator> (const fed_t &) const

bool operator> (const raw_t *) const

bool operator<= (const dbm_t &) const

bool operator<= (const fed_t &) const

bool operator<= (const raw_t *) const

bool operator>= (const dbm_t &) const

bool operator>= (const fed_t &) const

bool operator>= (const raw_t *) const

relation_t relation (const dbm_t &arg) const

Relation (wrt inclusion, approximate only for fed_t).

relation_t relation (const fed_t &arg) const

relation_t relation (const raw_t *arg, cindex_t dim) const

bool lt (const fed_t &arg) const

Exact (expensive) relations (for fed_t only).

bool gt (const fed_t &arg) const

bool le (const fed_t &arg) const

bool ge (const fed_t &arg) const

bool eq (const fed_t &arg) const

relation_t exactRelation (const fed_t &arg) const

dbm_t & setZero ()

Set this zone to zero (origin).

dbm_t & setInit ()

(re-)initialize the DBM with no constraint.

bool isInit () const

bool isZero () const

int32_t getUpperMinimumCost (int32_t cost) const

Computes the biggest lower cost in the zone.

int32_t getInfimum () const

Only for compatibility with priced DBMs.

dbm_t & operator+= (const dbm_t &)

Convex union operator (+).

dbm_t & operator+= (const fed_t &)

dbm_t & operator+= (const raw_t *)

dbm_t & operator &= (const dbm_t &)

Intersection and constraint operator (&).

dbm_t & operator &= (const raw_t *)

dbm_t & operator &= (const constraint_t &)

dbm_t & operator &= (const base::pointer_t< constraint_t > &)

dbm_t & operator &= (const std::vector< constraint_t > &)

bool constrain (cindex_t i, int32_t value)

Methods for constraining: with one or more constraints.

bool constrain (cindex_t i, cindex_t j, raw_t c)

bool constrain (cindex_t i, cindex_t j, int32_t b, strictness_t s)

bool constrain (cindex_t i, cindex_t j, int32_t b, bool isStrict)

bool constrain (const constraint_t &c)

bool constrain (const constraint_t *c, size_t n)

bool constrain (const cindex_t *table, const constraint_t *c, size_t n)

bool constrain (const cindex_t *table, const base::pointer_t< constraint_t > &)

bool constrain (const cindex_t *table, const std::vector< constraint_t > &)

bool intersects (const dbm_t &) const

bool intersects (const fed_t &) const

bool intersects (const raw_t *, cindex_t dim) const

dbm_t & up ()

Delay (strongest post-condition).

dbm_t & down ()

Inverse delay (weakest pre-condition).

dbm_t & freeClock (cindex_t clock)

Free clock (unconstrain).

dbm_t & freeUp (cindex_t clock)

Free upper or lower bounds only for a particular clock or for all clocks.

dbm_t & freeDown (cindex_t clock)

dbm_t & freeAllUp ()

dbm_t & freeAllDown ()

void updateValue (cindex_t x, int32_t v)

Update methods where x & y are clocks, v an integer value.

void updateClock (cindex_t x, cindex_t y)

void updateIncrement (cindex_t x, int32_t v)

void update (cindex_t x, cindex_t y, int32_t v)

bool satisfies (cindex_t i, cindex_t j, raw_t c) const

Check if the DBM satisfies a constraint c_ij.

bool satisfies (const constraint_t &c) const

bool operator && (const constraint_t &c) const

bool isUnbounded () const

dbm_t & relaxUp ()

Make upper or lower finite bounds non strict.

dbm_t & relaxDown ()

dbm_t & relaxUpClock (cindex_t clock)

Similar for all bounds of a particular clock.

dbm_t & relaxDownClock (cindex_t clock)

dbm_t & relaxAll ()

Make all constraints (except infinity) non strict.

bool contains (const IntValuation &point) const

Test point inclusion.

bool contains (const int32_t *point, cindex_t dim) const

bool contains (const DoubleValuation &point) const

bool contains (const double *point, cindex_t dim) const

bool delay (const DoubleValuation &point, double *t) const

Compute the 'almost min' necessary delay from a point to enter this federation.

bool delay (const double *point, cindex_t dim, double *t) const

void extrapolateMaxBounds (const int32_t *max)

Extrapolations:.

void diagonalExtrapolateMaxBounds (const int32_t *max)

void extrapolateLUBounds (const int32_t *lower, const int32_t *upper)

void diagonalExtrapolateLUBounds (const int32_t *lower, const int32_t *upper)

void resize (const uint32_t *bitSrc, const uint32_t *bitDst, size_t bitSize, cindex_t *table)

Resize this DBM: bitSrc marks the subset of clocks (out from a larger total set) that are in this DBM and bitDst marks the subset of clocks we want to change to.

void changeClocks (const cindex_t *target, cindex_t newDim)

Resize and change clocks of this DBM.

void swapClocks (cindex_t x, cindex_t y)

Swap clocks x and y.

DoubleValuation & getValuation (DoubleValuation &cval, bool *freeC=NULL) const throw (std::out_of_range)

Get a clock valuation and change only the clocks that are marked free.

dbm_t (const ClockOperation< dbm_t > &op)

Special constructor to copy the result of a pending operation.

ClockOperation< dbm_t > operator() (cindex_t clk)

bool isSubtractionEmpty (const raw_t *arg, cindex_t dim) const

bool isSubtractionEmpty (const fed_t &arg) const

bool isSubtractionEmpty (const dbm_t &arg) const

void newCopy (const raw_t *arg, cindex_t dim)

Simplified copy with.

void newCopy (const dbm_t &arg)

Simplified copy with.

void updateCopy (const raw_t *arg, cindex_t dim)

Simplified copy with.

void updateCopy (const dbm_t &arg)

Simplified copy with.

const idbm_t * const_idbmt () const

Const access to its idbm_t,.

idbm_t * idbmt ()

const raw_t * const_dbm () const

Explicit const access to the DBM matrix.

raw_t * dbm ()

Mutable access to the DBM matrix.

cindex_t edim () const

cindex_t pdim () const

bool isMutable () const

raw_t * getNew ()

Set and return a new writable DBM,.

raw_t * getCopy ()

Set and return a writable copy of this DBM,.

Static Public Member Functions

static size_t getSizeOfMinDBM (cindex_t dim, mingraph_t)

Wrapper for dbm_getSizeOfMinDBM.

static dbm_t readFromMinDBM (cindex_t dim, mingraph_t)

Construct a dbm_t from a mingraph_t.

Private Member Functions

uintptr_t uval () const

void incRef () const

Wrapper for idbmPtr.

void decRef () const

Wrapper for idbmPtr.

void empty (cindex_t dim)

Specialized versions to remove idbmPtr and setEmpty(dim),.

void emptyImmutable (cindex_t dim)

void emptyMutable (cindex_t dim)

void setEmpty (cindex_t dim)

Set idbmPtr to empty with dimension dim.

void setPtr (idbm_t *ptr)

Set a pointer for idbmPtr.

bool tryMutable ()

Check and try to make idbmPtr mutable cheaply (eg if reference counter is equal to 1 and the DBM is in the hash, then it is cheap).

raw_t * setNew (cindex_t dim)

Set idbmPtr to a newly allocated DBM with explicit dimension.

raw_t * inew (cindex_t dim)

Allocate new DBM and return the matrix.

raw_t * icopy (cindex_t dim)

Copy its DBM and return the matrix.

void ptr_intern ()

Implementations of previous methods with.

dbm_t & ptr_convexUnion (const raw_t *arg, cindex_t dim)

bool ptr_intersectionIsArg (const raw_t *arg, cindex_t dim)

bool ptr_constrain (cindex_t i, cindex_t j, raw_t c)

bool ptr_constrain (cindex_t k, int32_t value)

bool ptr_constrain (const constraint_t *cnstr, size_t n)

bool ptr_constrain (const cindex_t *table, const constraint_t *cnstr, size_t n)

void ptr_up ()

void ptr_down ()

void ptr_freeClock (cindex_t k)

void ptr_updateValue (cindex_t i, int32_t v)

void ptr_updateClock (cindex_t i, cindex_t j)

void ptr_update (cindex_t i, cindex_t j, int32_t v)

void ptr_freeUp (cindex_t k)

void ptr_freeDown (cindex_t k)

void ptr_freeAllUp ()

void ptr_freeAllDown ()

void ptr_relaxDownClock (cindex_t k)

void ptr_relaxUpClock (cindex_t k)

void ptr_relaxAll ()

bool ptr_getValuation (DoubleValuation &cval, bool *freeC) const

void ptr_swapClocks (cindex_t x, cindex_t y)

Private Attributes

idbm_t * idbmPtr

Internal pointer or special coding for empty.

Friends

class fed_t

class dbmlist_t

Member Enumeration Documentation

anonymous enum

Enumeration values:

MAX_DIM_POWER

MAX_DIM

Constructor & Destructor Documentation

dbm::dbm_t::dbm_t ( cindex_t dim = 1 ) [inline, explicit]

Initialize a dbm_t to empty DBM of a given dimension.

Parameters:

dim,: dimension of the DBM.

Postcondition:
isEmpty()

dbm::dbm_t::dbm_t ( const dbm_t & arg ) [inline]

Standard copy constructor.

dbm::dbm_t::dbm_t ( const raw_t * arg,

cindex_t dim

) [inline]

Copy constructor from a DBM matrix.

Postcondition:
isEmpty() iff dim == 0

dbm::dbm_t::~dbm_t ( ) [inline]

dbm::dbm_t::dbm_t ( const ClockOperation< dbm_t > & op ) [inline]

Special constructor to copy the result of a pending operation.

Parameters:

op,: clock operation.

Member Function Documentation

size_t dbm::dbm_t::analyzeForMinDBM ( uint32_t * bitMatrix ) const [inline]

Compute the minimal set of constraints to represent this DBM.

See also:
dbm_analyzeForMinDBM.

Returns:
the number of constraints of the set.

Precondition:
bitMatrix is a uint32_t[bits2intsize(dim*dim)] and !isEmpty()

void dbm::dbm_t::changeClocks ( const cindex_t * target,

cindex_t newDim

)

Resize and change clocks of this DBM.
The updated DBM will have its clocks i coming from target[i] in the original DBM.
Parameters:

target is the table that says where to put the current clocks in the target DBM. If target[i] = ~0 then a new free clock is inserted.

Precondition:
newDim > 0, target is a cindex_t[newDim], and for all i < newDim, target[i] < getDimension().

const raw_t * dbm::dbm_t::const_dbm ( ) const [inline]

Explicit const access to the DBM matrix.
Note: const_dbm() and dbm() have different assertions.
Precondition:
!isEmpty()

const idbm_t * dbm::dbm_t::const_idbmt ( ) const [inline]

Const access to its idbm_t,.

Precondition:
!isEmpty()

bool dbm::dbm_t::constrain ( const cindex_t * table,

const std::vector< constraint_t > &

) [inline]

bool dbm::dbm_t::constrain ( const cindex_t * table,

const base::pointer_t< constraint_t > &

) [inline]

bool dbm::dbm_t::constrain ( const cindex_t * table,

const constraint_t * c,

size_t n

) [inline]

bool dbm::dbm_t::constrain ( const constraint_t * c,

size_t n

) [inline]

bool dbm::dbm_t::constrain ( const constraint_t & c ) [inline]

bool dbm::dbm_t::constrain ( cindex_t i,

cindex_t j,

int32_t b,

bool isStrict

) [inline]

bool dbm::dbm_t::constrain ( cindex_t i,

cindex_t j,

int32_t b,

strictness_t s

) [inline]

bool dbm::dbm_t::constrain ( cindex_t i,

cindex_t j,

raw_t c

) [inline]

bool dbm::dbm_t::constrain ( cindex_t i,

int32_t value

) [inline]

Methods for constraining: with one or more constraints.
Variants with
Parameters:

table,: indirection table for the indices.

clock xi == value
clocks xi-xj < cij or <= cij (constraint = c)
clocks xi-xj < or <= b depending on strictness (strictness_t or bool).
or several constraints at once.

Precondition:
compatible indices, i != j for the constraints, and table is an cindex_t[getDimension()]

Returns:
!isEmpty()

bool dbm::dbm_t::contains ( const double * point,

cindex_t dim

) const

bool dbm::dbm_t::contains ( const DoubleValuation & point ) const

bool dbm::dbm_t::contains ( const int32_t * point,

cindex_t dim

) const

bool dbm::dbm_t::contains ( const IntValuation & point ) const

Test point inclusion.

Precondition:
same dimension.

void dbm::dbm_t::copyFrom ( const raw_t * src,

cindex_t dim

)

Copy from a DBM.

void dbm::dbm_t::copyTo ( raw_t * dst,

cindex_t dim

) const

Copy to a DBM.

Precondition:
dbm_isValid(dst, dim) and dim == getDimension()

raw_t * dbm::dbm_t::dbm ( ) [inline]

Mutable access to the DBM matrix.

Precondition:
isMutable()

void dbm::dbm_t::decRef ( ) const [inline, private]

Wrapper for idbmPtr.

bool dbm::dbm_t::delay ( const double * point,

cindex_t dim,

double * t

) const

bool dbm::dbm_t::delay ( const DoubleValuation & point,

double * t

) const [inline]

Compute the 'almost min' necessary delay from a point to enter this federation.
If this point is already contained in this federation, 0.0 is returned. The result is 'almost min' since we want a discrete value, which is not possible in case of strict constraints.
Precondition:
dim == getDimension() and point[0] == 0.0 otherwise the computation will not work.

Returns:
true if it is possible to reach this DBM by delaying, or false if this DBM is empty or it is not possible to reach it by delaying. The delay is written in t.

void dbm::dbm_t::diagonalExtrapolateLUBounds ( const int32_t * lower,

const int32_t * upper

) [inline]

void dbm::dbm_t::diagonalExtrapolateMaxBounds ( const int32_t * max ) [inline]

dbm_t & dbm::dbm_t::down ( ) [inline]

Inverse delay (weakest pre-condition).
Remove lower bounds.
Returns:
this

cindex_t dbm::dbm_t::edim ( ) const [inline]

Returns:
dimension with

Precondition:
isEmpty()

void dbm::dbm_t::empty ( cindex_t dim ) [inline, private]

Specialized versions to remove idbmPtr and setEmpty(dim),.

Precondition:
!isEmpty()

void dbm::dbm_t::emptyImmutable ( cindex_t dim ) [inline, private]

void dbm::dbm_t::emptyMutable ( cindex_t dim ) [inline, private]

bool dbm::dbm_t::eq ( const fed_t & arg ) const [inline]

relation_t dbm::dbm_t::exactRelation ( const fed_t & arg ) const [inline]

void dbm::dbm_t::extrapolateLUBounds ( const int32_t * lower,

const int32_t * upper

) [inline]

void dbm::dbm_t::extrapolateMaxBounds ( const int32_t * max ) [inline]

Extrapolations:.

See also:
dbm_##method functions in dbm.h.

Precondition:
max, lower, and upper are int32_t[getDimension()]

dbm_t & dbm::dbm_t::freeAllDown ( ) [inline]

dbm_t & dbm::dbm_t::freeAllUp ( ) [inline]

dbm_t & dbm::dbm_t::freeClock ( cindex_t clock ) [inline]

Free clock (unconstrain).
Remove constraints on a particular clock, both upper and lower bounds.
Returns:
this.

Postcondition:
freeClock(c) == freeUp(c).freeDown(c)

dbm_t & dbm::dbm_t::freeDown ( cindex_t clock ) [inline]

dbm_t & dbm::dbm_t::freeUp ( cindex_t clock ) [inline]

Free upper or lower bounds only for a particular clock or for all clocks.

Precondition:
0 < clock < getDimension()

Returns:
this.

See also:
dbm.h

bool dbm::dbm_t::ge ( const fed_t & arg ) const [inline]

raw_t * dbm::dbm_t::getCopy ( ) [inline]

Set and return a writable copy of this DBM,.

Precondition:
!isEmpty()

raw_t * dbm::dbm_t::getDBM ( ) [inline]

Returns:
a read-write access pointer to the internal DBM.

Postcondition:
return non null pointer iff getDimension() > 0

cindex_t dbm::dbm_t::getDimension ( ) const [inline]

Returns:
the dimension of this DBM.

int32_t dbm::dbm_t::getInfimum ( ) const [inline]

Only for compatibility with priced DBMs.

raw_t * dbm::dbm_t::getNew ( ) [inline]

Set and return a new writable DBM,.

Precondition:
!isEmpty()

size_t dbm::dbm_t::getSizeOfMinDBM ( cindex_t dim,

mingraph_t

) [inline, static]

Wrapper for dbm_getSizeOfMinDBM.
Here for other compatibility reasons.
Precondition:
dimension == getDimension()

int32_t dbm::dbm_t::getUpperMinimumCost ( int32_t cost ) const

Computes the biggest lower cost in the zone.
This corresponds to the value $\sup\{ c \mid \exists v \in Z : c = \inf \{ c' \mid v[cost\mapsto c'] \in Z \} \}$

DoubleValuation & dbm::dbm_t::getValuation ( DoubleValuation & cval,

bool * freeC = NULL

) const throw (std::out_of_range)

Get a clock valuation and change only the clocks that are marked free.

Parameters:

cval,: clock valuation to write.

freeC,: free clocks to write. If freeC = NULL then all clocks are considered free.

Returns:
cval

Exceptions:

std::out_of_range if the generation fails if isEmpty() or cval too constrained.

Postcondition:
if freeC != NULL, forall i < dim: freeC[i] = false

bool dbm::dbm_t::gt ( const fed_t & arg ) const [inline]

uint32_t dbm::dbm_t::hash ( uint32_t seed = 0 ) const [inline]

Returns:
a hash value.

bool dbm::dbm_t::hasZero ( ) const

Returns:
true if this DBM contains the zero point.

raw_t * dbm::dbm_t::icopy ( cindex_t dim ) [inline, private]

Copy its DBM and return the matrix.

Precondition:
!isEmpty() && !tryMutable()

idbm_t * dbm::dbm_t::idbmt ( ) [inline]

Returns:
idbmPtr as a pointer

Precondition:
!isEmpty()

void dbm::dbm_t::incRef ( ) const [inline, private]

Wrapper for idbmPtr.

raw_t * dbm::dbm_t::inew ( cindex_t dim ) [inline, private]

Allocate new DBM and return the matrix.

Precondition:
!isEmpty() && !tryMutable()

void dbm::dbm_t::intern ( ) [inline]

Try to share the DBM.

bool dbm::dbm_t::intersects ( const raw_t * ,

cindex_t dim

) const

bool dbm::dbm_t::intersects ( const fed_t & ) const

bool dbm::dbm_t::intersects ( const dbm_t & ) const

Returns:
false if there is no intersection with the argument or true if there *may* be an intersection.

Precondition:
same dimension.

bool dbm::dbm_t::isEmpty ( ) const [inline]

Returns:
true if it is empty.

bool dbm::dbm_t::isInit ( ) const [inline]

Returns:
dbm_isEqualToInit(DBM),

See also:
dbm.h

bool dbm::dbm_t::isMutable ( ) const [inline]

Returns:
true if this fed_t can be modified,

Precondition:
isPointer()

bool dbm::dbm_t::isSubtractionEmpty ( const dbm_t & arg ) const [inline]

bool dbm::dbm_t::isSubtractionEmpty ( const fed_t & arg ) const

bool dbm::dbm_t::isSubtractionEmpty ( const raw_t * arg,

cindex_t dim

) const [inline]

Returns:
(this-arg).isEmpty() but it is able to stop the subtraction early if it is not empty and it does not modify itself.

Precondition:
same dimension.

bool dbm::dbm_t::isUnbounded ( ) const [inline]

Returns:
true if this DBM contains points that can delay arbitrarily.

bool dbm::dbm_t::isZero ( ) const [inline]

Returns:
dbm_isEqualToZero(DBM),

See also:
dbm.h

bool dbm::dbm_t::le ( const fed_t & arg ) const [inline]

bool dbm::dbm_t::lt ( const fed_t & arg ) const [inline]

Exact (expensive) relations (for fed_t only).

void dbm::dbm_t::newCopy ( const dbm_t & arg ) [inline]

Simplified copy with.

Precondition:
isEmpty() && !arg.isEmpty()

void dbm::dbm_t::newCopy ( const raw_t * arg,

cindex_t dim

) [inline]

Simplified copy with.

Precondition:
isEmpty()

void dbm::dbm_t::nil ( ) [inline]

Short for setDimension(1), has the effect of deallocating the DBM.

bool dbm::dbm_t::operator && ( const constraint_t & c ) const [inline]

dbm_t & dbm::dbm_t::operator &= ( const std::vector< constraint_t > & ) [inline]

dbm_t & dbm::dbm_t::operator &= ( const base::pointer_t< constraint_t > & ) [inline]

dbm_t & dbm::dbm_t::operator &= ( const constraint_t & ) [inline]

dbm_t & dbm::dbm_t::operator &= ( const raw_t * )

dbm_t & dbm::dbm_t::operator &= ( const dbm_t & )

Intersection and constraint operator (&).

Precondition:
same dimension, compatible indices, and i != j for the constraints.

bool dbm::dbm_t::operator!= ( const raw_t * ) const [inline]

bool dbm::dbm_t::operator!= ( const fed_t & ) const [inline]

bool dbm::dbm_t::operator!= ( const dbm_t & ) const [inline]

ClockOperation< dbm_t > dbm::dbm_t::operator() ( cindex_t clk ) [inline]

See also:
ClockOperation for more details.

Precondition:
clk > 0 except for clock constraint tests and clk < getDimension()

raw_t dbm::dbm_t::operator() ( cindex_t i,

cindex_t j

) const [inline]

Returns:
DBM[i,j]

Precondition:
!isEmpty() && i < getDimension() && j < getDimension() otherwise segfault.

const raw_t * dbm::dbm_t::operator() ( ) const [inline]

Returns:
read-only pointer to the internal DBM matrix.

Postcondition:
non null pointer iff !isEmpty()

dbm_t & dbm::dbm_t::operator+= ( const raw_t * )

dbm_t & dbm::dbm_t::operator+= ( const fed_t & )

dbm_t & dbm::dbm_t::operator+= ( const dbm_t & )

Convex union operator (+).

Precondition:
same dimension.

bool dbm::dbm_t::operator< ( const raw_t * ) const

bool dbm::dbm_t::operator< ( const fed_t & ) const [inline]

bool dbm::dbm_t::operator< ( const dbm_t & ) const [inline]

bool dbm::dbm_t::operator<= ( const raw_t * ) const [inline]

bool dbm::dbm_t::operator<= ( const fed_t & ) const [inline]

bool dbm::dbm_t::operator<= ( const dbm_t & ) const

dbm_t & dbm::dbm_t::operator= ( const raw_t * ) [inline]

dbm_t & dbm::dbm_t::operator= ( const dbm_t & ) [inline]

Overload of standard operators.
The raw_t* arguments are assumed to be matrices of the same dimension of this dbm_t (and dbm_isValid also holds).

bool dbm::dbm_t::operator== ( const raw_t * ) const

bool dbm::dbm_t::operator== ( const fed_t & ) const [inline]

bool dbm::dbm_t::operator== ( const dbm_t & ) const

Comparisons have the semantics of set inclusion.
Equality of dimensions is checked. Comparisons agains fed_t are approximate and cheap since done between DBMs pair-wise. See the header.

bool dbm::dbm_t::operator> ( const raw_t * ) const

bool dbm::dbm_t::operator> ( const fed_t & ) const [inline]

bool dbm::dbm_t::operator> ( const dbm_t & ) const [inline]

bool dbm::dbm_t::operator>= ( const raw_t * ) const [inline]

bool dbm::dbm_t::operator>= ( const fed_t & ) const [inline]

bool dbm::dbm_t::operator>= ( const dbm_t & ) const [inline]

const raw_t * dbm::dbm_t::operator[] ( cindex_t i ) const [inline]

Returns:
row DBM[i]

Precondition:
!isEmpty() && i < getDimension()

cindex_t dbm::dbm_t::pdim ( ) const [inline]

Returns:
dimension with

Precondition:
!isEmpty()

bool dbm::dbm_t::ptr_constrain ( const cindex_t * table,

const constraint_t * cnstr,

size_t n

) [private]

bool dbm::dbm_t::ptr_constrain ( const constraint_t * cnstr,

size_t n

) [private]

bool dbm::dbm_t::ptr_constrain ( cindex_t k,

int32_t value

) [private]

bool dbm::dbm_t::ptr_constrain ( cindex_t i,

cindex_t j,

raw_t c

) [private]

dbm_t & dbm::dbm_t::ptr_convexUnion ( const raw_t * arg,

cindex_t dim

) [private]

void dbm::dbm_t::ptr_down ( ) [private]

void dbm::dbm_t::ptr_freeAllDown ( ) [private]

void dbm::dbm_t::ptr_freeAllUp ( ) [private]

void dbm::dbm_t::ptr_freeClock ( cindex_t k ) [private]

void dbm::dbm_t::ptr_freeDown ( cindex_t k ) [private]

void dbm::dbm_t::ptr_freeUp ( cindex_t k ) [private]

bool dbm::dbm_t::ptr_getValuation ( DoubleValuation & cval,

bool * freeC

) const [private]

void dbm::dbm_t::ptr_intern ( ) [private]

Implementations of previous methods with.

Precondition:
isPointer() useful for fed_t since the invariant states that there is no empty dbm_t in fed_t.

bool dbm::dbm_t::ptr_intersectionIsArg ( const raw_t * arg,

cindex_t dim

) [private]

void dbm::dbm_t::ptr_relaxAll ( ) [private]

void dbm::dbm_t::ptr_relaxDownClock ( cindex_t k ) [private]

void dbm::dbm_t::ptr_relaxUpClock ( cindex_t k ) [private]

void dbm::dbm_t::ptr_swapClocks ( cindex_t x,

cindex_t y

) [private]

void dbm::dbm_t::ptr_up ( ) [private]

void dbm::dbm_t::ptr_update ( cindex_t i,

cindex_t j,

int32_t v

) [private]

void dbm::dbm_t::ptr_updateClock ( cindex_t i,

cindex_t j

) [private]

void dbm::dbm_t::ptr_updateValue ( cindex_t i,

int32_t v

) [private]

dbm_t dbm::dbm_t::readFromMinDBM ( cindex_t dim,

mingraph_t

) [inline, static]

Construct a dbm_t from a mingraph_t.
Not as a constructor for other compatibility reasons.
Precondition:
dimension == getDimension()

relation_t dbm::dbm_t::relation ( const raw_t * arg,

cindex_t dim

) const

relation_t dbm::dbm_t::relation ( const fed_t & arg ) const [inline]

relation_t dbm::dbm_t::relation ( const dbm_t & arg ) const

Relation (wrt inclusion, approximate only for fed_t).

Returns:
this (relation) arg.

relation_t dbm::dbm_t::relation ( mingraph_t ming,

raw_t * unpackBuffer

) const [inline]

Relation with a mingraph_t,.

See also:
dbm_relationWithMinDBM.

Precondition:
unpackBuffer is a raw_t[dim*dim].

dbm_t & dbm::dbm_t::relaxAll ( ) [inline]

Make all constraints (except infinity) non strict.

dbm_t & dbm::dbm_t::relaxDown ( ) [inline]

dbm_t & dbm::dbm_t::relaxDownClock ( cindex_t clock ) [inline]

dbm_t & dbm::dbm_t::relaxUp ( ) [inline]

Make upper or lower finite bounds non strict.

See also:
dbm.h.

Returns:
this.

dbm_t & dbm::dbm_t::relaxUpClock ( cindex_t clock ) [inline]

Similar for all bounds of a particular clock.

See also:
dbm.h. Special for clock == 0: relaxUp(0) = relaxDown() and relaxDown(0) = relaxUp().

void dbm::dbm_t::resize ( const uint32_t * bitSrc,

const uint32_t * bitDst,

size_t bitSize,

cindex_t * table

)

Resize this DBM: bitSrc marks the subset of clocks (out from a larger total set) that are in this DBM and bitDst marks the subset of clocks we want to change to.
Resizing means keep the constraints of the clocks that are kept, remove the constraints of the clocks that are removed, and add free constraints (infinity) for the new clocks.
See also:
dbm_shrinkExpand in dbm.h.

Parameters:

bitSrc,bitDst,bitSize,: bit strings of (int) size bitSize that mark the source and destination active clocks.

table,: redirection table to write.

Precondition:
bitSrc & bitDst are uint32_t[bitSize] and table is a uint32_t[32*bitSize]

Postcondition:
the indirection table is written.

bool dbm::dbm_t::sameAs ( const dbm_t & arg ) const [inline]

Returns:
true if arg has the same internal idbmPtr.

bool dbm::dbm_t::satisfies ( const constraint_t & c ) const [inline]

bool dbm::dbm_t::satisfies ( cindex_t i,

cindex_t j,

raw_t c

) const [inline]

Check if the DBM satisfies a constraint c_ij.

Precondition:
i != j, i and j < getDimension()

void dbm::dbm_t::setDimension ( cindex_t dim ) [inline]

Change the dimension of this DBM.
The resulting DBM is empty.
Postcondition:
isEmpty()

void dbm::dbm_t::setEmpty ( cindex_t dim ) [inline, private]

Set idbmPtr to empty with dimension dim.

void dbm::dbm_t::setEmpty ( ) [inline]

Empty this DBM.

dbm_t & dbm::dbm_t::setInit ( )

(re-)initialize the DBM with no constraint.

Postcondition:
!isEmpty() iff dim > 0.

raw_t * dbm::dbm_t::setNew ( cindex_t dim ) [inline, private]

Set idbmPtr to a newly allocated DBM with explicit dimension.

Precondition:
getDimension() > 0

void dbm::dbm_t::setPtr ( idbm_t * ptr ) [inline, private]

Set a pointer for idbmPtr.

dbm_t & dbm::dbm_t::setZero ( )

Set this zone to zero (origin).

Parameters:

tau,: tau clock,

See also:
dbm.h

Postcondition:
!isEmpty() iff dim > 0.

void dbm::dbm_t::swapClocks ( cindex_t x,

cindex_t y

) [inline]

Swap clocks x and y.

std::string dbm::dbm_t::toString ( const ClockAccessor & ) const

Returns:
string representation of the constraints of this DBM. A clock is always positive, so "true" simply means all clocks positive.

bool dbm::dbm_t::tryMutable ( ) [inline, private]

Check and try to make idbmPtr mutable cheaply (eg if reference counter is equal to 1 and the DBM is in the hash, then it is cheap).

Precondition:
!isEmpty()

dbm_t & dbm::dbm_t::up ( ) [inline]

Delay (strongest post-condition).
Remove upper bounds.
Returns:
this

void dbm::dbm_t::update ( cindex_t x,

cindex_t y,

int32_t v

)

void dbm::dbm_t::updateClock ( cindex_t x,

cindex_t y

) [inline]

void dbm::dbm_t::updateCopy ( const dbm_t & arg ) [inline]

Simplified copy with.

Precondition:
!isEmpty() && !arg.isEmpty()

void dbm::dbm_t::updateCopy ( const raw_t * arg,

cindex_t dim

) [inline]

Simplified copy with.

Precondition:
!isEmpty()

void dbm::dbm_t::updateIncrement ( cindex_t x,

int32_t v

) [inline]

void dbm::dbm_t::updateValue ( cindex_t x,

int32_t v

) [inline]

Update methods where x & y are clocks, v an integer value.
x := v -> updateValue x := y -> updateClock x := x + v -> updateIncrement x := y + v -> update
Precondition:
0 < x and y < getDimension(), v < infinity, and v is s.t. the clocks stay positive.

uintptr_t dbm::dbm_t::uval ( ) const [inline, private]

Returns:
idbmPtr as an int.

int32_t * dbm::dbm_t::writeAnalyzedDBM ( uint32_t * bitMatrix,

size_t nbConstraints,

BOOL tryConstraints16,

allocator_t c_alloc,

size_t offset

) const [inline]

Similar to writeToMinDBMWithOffset but works with a pre-analyzed DBM.

Precondition:
!isEmpty() and bitMatrix corresponds to its analysis (otherwise nonsense will be written).

See also:
dbm_writeAnalyzedDBM.

Postcondition:
bitMatrix is cleaned from the constraints xi>=0.

int32_t * dbm::dbm_t::writeToMinDBMWithOffset ( bool minimizeGraph,

bool tryConstraints16,

allocator_t c_alloc,

size_t offset

) const [inline]

Compute & save the minimal set of constraints.

Parameters:

tryConstraints16,: flag to try to save constraints on 16 bits, will cost dim*dim time.

c_alloc,: C allocator wrapper

offset,: offset for allocation.

Returns:
allocated memory.

Precondition:
!isEmpty().

Friends And Related Function Documentation

friend class dbmlist_t [friend]

friend class fed_t [friend]

Member Data Documentation

idbm_t* dbm::dbm_t::idbmPtr [private]

Internal pointer or special coding for empty.

The documentation for this class was generated from the following files:

/home/adavid/UPPAAL/trunk/server/modules/include/dbm/fed.h
/home/adavid/UPPAAL/trunk/server/modules/include/dbm/inline_fed.h
/home/adavid/UPPAAL/trunk/server/modules/dbm/fed_dbm.cpp

Generated on Fri Jun 30 00:02:47 2006 for Module dbm by

1.4.2


Public Types
enum	{ MAX_DIM_POWER = 15, MAX_DIM = ((1 << MAX_DIM_POWER) - 1) }
Public Member Functions
	dbm_t (cindex_t dim=1)
	Initialize a dbm_t to empty DBM of a given dimension.
	dbm_t (const dbm_t &arg)
	Standard copy constructor.
	dbm_t (const raw_t *arg, cindex_t dim)
	Copy constructor from a DBM matrix.
	~dbm_t ()
cindex_t	getDimension () const
std::string	toString (const ClockAccessor &) const
void	setDimension (cindex_t dim)
	Change the dimension of this DBM.
bool	isEmpty () const
void	setEmpty ()
	Empty this DBM.
void	nil ()
	Short for setDimension(1), has the effect of deallocating the DBM.
bool	hasZero () const
uint32_t	hash (uint32_t seed=0) const
bool	sameAs (const dbm_t &arg) const
void	intern ()
	Try to share the DBM.
void	copyFrom (const raw_t *src, cindex_t dim)
	Copy from a DBM.
void	copyTo (raw_t *dst, cindex_t dim) const
	Copy to a DBM.
const raw_t *	operator() () const
raw_t	operator() (cindex_t i, cindex_t j) const
const raw_t *	operator[] (cindex_t i) const
raw_t *	getDBM ()
size_t	analyzeForMinDBM (uint32_t *bitMatrix) const
	Compute the minimal set of constraints to represent this DBM.
int32_t *	writeToMinDBMWithOffset (bool minimizeGraph, bool tryConstraints16, allocator_t c_alloc, size_t offset) const
	Compute & save the minimal set of constraints.
int32_t *	writeAnalyzedDBM (uint32_t *bitMatrix, size_t nbConstraints, BOOL tryConstraints16, allocator_t c_alloc, size_t offset) const
	Similar to writeToMinDBMWithOffset but works with a pre-analyzed DBM.
relation_t	relation (mingraph_t ming, raw_t *unpackBuffer) const
	Relation with a mingraph_t,.
dbm_t &	operator= (const dbm_t &)
	Overload of standard operators.
dbm_t &	operator= (const raw_t *)
bool	operator== (const dbm_t &) const
	Comparisons have the semantics of set inclusion.
bool	operator== (const fed_t &) const
bool	operator== (const raw_t *) const
bool	operator!= (const dbm_t &) const
bool	operator!= (const fed_t &) const
bool	operator!= (const raw_t *) const
bool	operator< (const dbm_t &) const
bool	operator< (const fed_t &) const
bool	operator< (const raw_t *) const
bool	operator> (const dbm_t &) const
bool	operator> (const fed_t &) const
bool	operator> (const raw_t *) const
bool	operator<= (const dbm_t &) const
bool	operator<= (const fed_t &) const
bool	operator<= (const raw_t *) const
bool	operator>= (const dbm_t &) const
bool	operator>= (const fed_t &) const
bool	operator>= (const raw_t *) const
relation_t	relation (const dbm_t &arg) const
	Relation (wrt inclusion, approximate only for fed_t).
relation_t	relation (const fed_t &arg) const
relation_t	relation (const raw_t *arg, cindex_t dim) const
bool	lt (const fed_t &arg) const
	Exact (expensive) relations (for fed_t only).
bool	gt (const fed_t &arg) const
bool	le (const fed_t &arg) const
bool	ge (const fed_t &arg) const
bool	eq (const fed_t &arg) const
relation_t	exactRelation (const fed_t &arg) const
dbm_t &	setZero ()
	Set this zone to zero (origin).
dbm_t &	setInit ()
	(re-)initialize the DBM with no constraint.
bool	isInit () const
bool	isZero () const
int32_t	getUpperMinimumCost (int32_t cost) const
	Computes the biggest lower cost in the zone.
int32_t	getInfimum () const
	Only for compatibility with priced DBMs.
dbm_t &	operator+= (const dbm_t &)
	Convex union operator (+).
dbm_t &	operator+= (const fed_t &)
dbm_t &	operator+= (const raw_t *)
dbm_t &	operator &= (const dbm_t &)
	Intersection and constraint operator (&).
dbm_t &	operator &= (const raw_t *)
dbm_t &	operator &= (const constraint_t &)
dbm_t &	operator &= (const base::pointer_t< constraint_t > &)
dbm_t &	operator &= (const std::vector< constraint_t > &)
bool	constrain (cindex_t i, int32_t value)
	Methods for constraining: with one or more constraints.
bool	constrain (cindex_t i, cindex_t j, raw_t c)
bool	constrain (cindex_t i, cindex_t j, int32_t b, strictness_t s)
bool	constrain (cindex_t i, cindex_t j, int32_t b, bool isStrict)
bool	constrain (const constraint_t &c)
bool	constrain (const constraint_t *c, size_t n)
bool	constrain (const cindex_t table, const constraint_t c, size_t n)
bool	constrain (const cindex_t *table, const base::pointer_t< constraint_t > &)
bool	constrain (const cindex_t *table, const std::vector< constraint_t > &)
bool	intersects (const dbm_t &) const
bool	intersects (const fed_t &) const
bool	intersects (const raw_t *, cindex_t dim) const
dbm_t &	up ()
	Delay (strongest post-condition).
dbm_t &	down ()
	Inverse delay (weakest pre-condition).
dbm_t &	freeClock (cindex_t clock)
	Free clock (unconstrain).
dbm_t &	freeUp (cindex_t clock)
	Free upper or lower bounds only for a particular clock or for all clocks.
dbm_t &	freeDown (cindex_t clock)
dbm_t &	freeAllUp ()
dbm_t &	freeAllDown ()
void	updateValue (cindex_t x, int32_t v)
	Update methods where x & y are clocks, v an integer value.
void	updateClock (cindex_t x, cindex_t y)
void	updateIncrement (cindex_t x, int32_t v)
void	update (cindex_t x, cindex_t y, int32_t v)
bool	satisfies (cindex_t i, cindex_t j, raw_t c) const
	Check if the DBM satisfies a constraint c_ij.
bool	satisfies (const constraint_t &c) const
bool	operator && (const constraint_t &c) const
bool	isUnbounded () const
dbm_t &	relaxUp ()
	Make upper or lower finite bounds non strict.
dbm_t &	relaxDown ()
dbm_t &	relaxUpClock (cindex_t clock)
	Similar for all bounds of a particular clock.
dbm_t &	relaxDownClock (cindex_t clock)
dbm_t &	relaxAll ()
	Make all constraints (except infinity) non strict.
bool	contains (const IntValuation &point) const
	Test point inclusion.
bool	contains (const int32_t *point, cindex_t dim) const
bool	contains (const DoubleValuation &point) const
bool	contains (const double *point, cindex_t dim) const
bool	delay (const DoubleValuation &point, double *t) const
	Compute the 'almost min' necessary delay from a point to enter this federation.
bool	delay (const double point, cindex_t dim, double t) const
void	extrapolateMaxBounds (const int32_t *max)
	Extrapolations:.
void	diagonalExtrapolateMaxBounds (const int32_t *max)
void	extrapolateLUBounds (const int32_t lower, const int32_t upper)
void	diagonalExtrapolateLUBounds (const int32_t lower, const int32_t upper)
void	resize (const uint32_t bitSrc, const uint32_t bitDst, size_t bitSize, cindex_t *table)
	Resize this DBM: bitSrc marks the subset of clocks (out from a larger total set) that are in this DBM and bitDst marks the subset of clocks we want to change to.
void	changeClocks (const cindex_t *target, cindex_t newDim)
	Resize and change clocks of this DBM.
void	swapClocks (cindex_t x, cindex_t y)
	Swap clocks x and y.
DoubleValuation &	getValuation (DoubleValuation &cval, bool *freeC=NULL) const throw (std::out_of_range)
	Get a clock valuation and change only the clocks that are marked free.
	dbm_t (const ClockOperation< dbm_t > &op)
	Special constructor to copy the result of a pending operation.
ClockOperation< dbm_t >	operator() (cindex_t clk)
bool	isSubtractionEmpty (const raw_t *arg, cindex_t dim) const
bool	isSubtractionEmpty (const fed_t &arg) const
bool	isSubtractionEmpty (const dbm_t &arg) const
void	newCopy (const raw_t *arg, cindex_t dim)
	Simplified copy with.
void	newCopy (const dbm_t &arg)
	Simplified copy with.
void	updateCopy (const raw_t *arg, cindex_t dim)
	Simplified copy with.
void	updateCopy (const dbm_t &arg)
	Simplified copy with.
const idbm_t *	const_idbmt () const
	Const access to its idbm_t,.
idbm_t *	idbmt ()
const raw_t *	const_dbm () const
	Explicit const access to the DBM matrix.
raw_t *	dbm ()
	Mutable access to the DBM matrix.
cindex_t	edim () const
cindex_t	pdim () const
bool	isMutable () const
raw_t *	getNew ()
	Set and return a new writable DBM,.
raw_t *	getCopy ()
	Set and return a writable copy of this DBM,.
Static Public Member Functions
static size_t	getSizeOfMinDBM (cindex_t dim, mingraph_t)
	Wrapper for dbm_getSizeOfMinDBM.
static dbm_t	readFromMinDBM (cindex_t dim, mingraph_t)
	Construct a dbm_t from a mingraph_t.
Private Member Functions
uintptr_t	uval () const
void	incRef () const
	Wrapper for idbmPtr.
void	decRef () const
	Wrapper for idbmPtr.
void	empty (cindex_t dim)
	Specialized versions to remove idbmPtr and setEmpty(dim),.
void	emptyImmutable (cindex_t dim)
void	emptyMutable (cindex_t dim)
void	setEmpty (cindex_t dim)
	Set idbmPtr to empty with dimension dim.
void	setPtr (idbm_t *ptr)
	Set a pointer for idbmPtr.
bool	tryMutable ()
	Check and try to make idbmPtr mutable cheaply (eg if reference counter is equal to 1 and the DBM is in the hash, then it is cheap).
raw_t *	setNew (cindex_t dim)
	Set idbmPtr to a newly allocated DBM with explicit dimension.
raw_t *	inew (cindex_t dim)
	Allocate new DBM and return the matrix.
raw_t *	icopy (cindex_t dim)
	Copy its DBM and return the matrix.
void	ptr_intern ()
	Implementations of previous methods with.
dbm_t &	ptr_convexUnion (const raw_t *arg, cindex_t dim)
bool	ptr_intersectionIsArg (const raw_t *arg, cindex_t dim)
bool	ptr_constrain (cindex_t i, cindex_t j, raw_t c)
bool	ptr_constrain (cindex_t k, int32_t value)
bool	ptr_constrain (const constraint_t *cnstr, size_t n)
bool	ptr_constrain (const cindex_t table, const constraint_t cnstr, size_t n)
void	ptr_up ()
void	ptr_down ()
void	ptr_freeClock (cindex_t k)
void	ptr_updateValue (cindex_t i, int32_t v)
void	ptr_updateClock (cindex_t i, cindex_t j)
void	ptr_update (cindex_t i, cindex_t j, int32_t v)
void	ptr_freeUp (cindex_t k)
void	ptr_freeDown (cindex_t k)
void	ptr_freeAllUp ()
void	ptr_freeAllDown ()
void	ptr_relaxDownClock (cindex_t k)
void	ptr_relaxUpClock (cindex_t k)
void	ptr_relaxAll ()
bool	ptr_getValuation (DoubleValuation &cval, bool *freeC) const
void	ptr_swapClocks (cindex_t x, cindex_t y)
Private Attributes
idbm_t *	idbmPtr
	Internal pointer or special coding for empty.
Friends
class	fed_t
class	dbmlist_t