dbm::fed_t

dbm::fed_t Class Reference

#include <fed.h>

List of all members.

Public Member Functions

fed_t (cindex_t dim=1)

Initialize a fed_t to empty federation of a given dimension.

fed_t (const fed_t &arg)

Standard copy constructor.

fed_t (const dbm_t &arg)

Wrap a DBM in a federation.

fed_t (const raw_t *arg, cindex_t dim)

Copy a DBM matrix in a federation.

~fed_t ()

size_t size () const

cindex_t getDimension () const

void setDimension (cindex_t dim)

Change the dimension of this federation.

bool isEmpty () const

void setEmpty ()

Empty this federation.

void nil ()

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

bool hasZero () const

std::string toString (const ClockAccessor &) const

int32_t getUpperMinimumCost (int cost) const

Computes the biggest lower cost in the zone.

int32_t getInfimum () const

Only for compatibility with priced federations.

uint32_t hash (uint32_t seed=0) const

bool sameAs (const fed_t &arg) const

void intern ()

Try to share the DBMs. Side-effect: affects all copies of this fed_t.

fed_t & operator= (const fed_t &)

Overload of standard operators.

fed_t & operator= (const dbm_t &)

fed_t & operator= (const raw_t *)

bool operator== (const fed_t &) const

Comparisons have the semantics of set inclusion.

bool operator== (const dbm_t &) const

bool operator== (const raw_t *) const

bool operator!= (const fed_t &) const

bool operator!= (const dbm_t &) const

bool operator!= (const raw_t *) const

bool operator< (const fed_t &) const

bool operator< (const dbm_t &) const

bool operator< (const raw_t *) const

bool operator> (const fed_t &) const

bool operator> (const dbm_t &) const

bool operator> (const raw_t *) const

bool operator<= (const fed_t &) const

bool operator<= (const dbm_t &) const

bool operator<= (const raw_t *) const

bool operator>= (const fed_t &) const

bool operator>= (const dbm_t &) const

bool operator>= (const raw_t *) const

relation_t relation (const fed_t &arg) const

Relation (wrt inclusion, approximate).

relation_t relation (const dbm_t &arg) const

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

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

Specialized relation test: >= arg (approximate).

bool eq (const fed_t &arg) const

Exact (expensive) relations.

bool eq (const dbm_t &arg) const

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

bool lt (const fed_t &arg) const

bool lt (const dbm_t &arg) const

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

bool gt (const fed_t &arg) const

bool gt (const dbm_t &arg) const

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

bool le (const fed_t &arg) const

bool le (const dbm_t &arg) const

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

bool ge (const fed_t &arg) const

bool ge (const dbm_t &arg) const

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

relation_t exactRelation (const fed_t &arg) const

relation_t exactRelation (const dbm_t &arg) const

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

fed_t & setZero ()

Set this federation to zero (origin).

fed_t & setInit ()

(re-)initialize the federation with no constraint.

fed_t & convexHull ()

Convex union of its DBMs.

fed_t & operator|= (const fed_t &)

(Set) union operator (|).

fed_t & operator|= (const dbm_t &)

fed_t & operator|= (const raw_t *)

fed_t & unionWith (fed_t &arg)

Union of 2 fed_t.

fed_t & unionWithC (fed_t arg)

fed_t & add (const fed_t &arg)

Simply add (list concatenation) DBMs to this federation.

fed_t & add (const dbm_t &arg)

fed_t & add (const raw_t *arg, cindex_t dim)

fed_t & append (fed_t &arg)

Append arg to 'this',.

fed_t & appendC (fed_t arg)

void append (fdbm_t *arg)

fed_t & operator+= (const fed_t &)

Convex union operator (+).

fed_t & operator+= (const dbm_t &)

fed_t & operator+= (const raw_t *)

fed_t & operator &= (const fed_t &)

Intersection and constraint operator (&).

fed_t & operator &= (const dbm_t &)

fed_t & operator &= (const raw_t *)

fed_t & operator &= (const constraint_t &)

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

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

fed_t & operator-= (const fed_t &)

(Set) subtraction operator (-).

fed_t & operator-= (const dbm_t &)

fed_t & operator-= (const raw_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 fed_t &) const

bool intersects (const dbm_t &) const

bool intersects (const raw_t *, cindex_t dim) const

fed_t & up ()

Delay (strongest post-condition) for all the DBMs.

fed_t & down ()

Inverse delay (weakest pre-condition) for all the DBMs.

fed_t & freeClock (cindex_t clock)

Free clock (unconstraint) for all the DBMs.

fed_t & freeUp (cindex_t clock)

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

fed_t & freeDown (cindex_t clock)

fed_t & freeAllUp ()

fed_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

bool satisfies (const constraint_t &c) const

bool operator && (const constraint_t &c) const

bool isUnbounded () const

fed_t & relaxUp ()

Make upper or lower finite bounds non strict for all the DBMs.

fed_t & relaxDown ()

fed_t & relaxUpClock (cindex_t clock)

Similar for all bounds of a particular clock for all the DBMs.

fed_t & relaxDownClock (cindex_t clock)

fed_t & relaxAll ()

Make all constraints (except infinity) non strict for all the DBMs.

fed_t & reduce ()

Remove redundant DBMs (if included in ONE other DBM).

fed_t & noReduce ()

This method is useful only for experiments.

fed_t & expensiveReduce ()

Remove redundant DBMs (if included in the UNION of the other DBMs).

fed_t & mergeReduce ()

Try to merge DBMs by pairs.

fed_t & convexReduce ()

Use a heuristic to recompute parts of the federation as part=convexHull(part)-(convexHull(part)-part).

fed_t & expensiveConvexReduce ()

Try to replace this by convexHull(this)-(convexHull(this)-this).

fed_t & partitionReduce ()

Find partitions in the federation and reduce them separately.

bool contains (const IntValuation &point) const

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

double possibleBackDelay (const DoubleValuation &point) const

double possibleBackDelay (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 splitExtrapolate (const constraint_t *begin, const constraint_t *end, const int32_t *max)

"Split-extrapolation".

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

Resize all the DBMs of this federation,.

void changeClocks (const cindex_t *target, cindex_t newDim)

Resize and change clocks of all the DBMs of this federation.

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.

fed_t & predt (const fed_t &bad)

predt operation: temporal predecessor of this federation avoiding 'bad'.

fed_t & predt (const dbm_t &bad)

fed_t & predt (const raw_t *bad, cindex_t dim)

bool isIncludedInPredt (const fed_t &good, const fed_t &bad) const

bool has (const dbm_t &arg) const

Identify test to know if this federation has a specific DBM.

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

bool hasSame (const dbm_t &arg) const

Similar but test with exact same dbm_t.

void removeIncludedIn (const fed_t &arg)

Remove the DBMs that are included in DBMs of arg (pair-wise inclusion checking).

bool removeIncludedIn (const dbm_t &arg)

bool removeIncludedIn (const raw_t *arg, cindex_t dim)

fed_t (const ClockOperation< fed_t > &op)

Special constructor to copy the result of a pending operation.

ClockOperation< fed_t > operator() (cindex_t clk)

Overload of operator (): () or (i,j) make no sense here.

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

bool isSubtractionEmpty (const dbm_t &arg) const

bool isSubtractionEmpty (const fed_t &arg) const

void removeEmpty ()

Clean-up the federation of its empty dbm_t.

bool hasEmpty () const

const_iterator begin () const

Access to iterators.

const const_iterator end () const

iterator beginMutable ()

const iterator endMutable () const

iterator erase (iterator &iter)

size_t write (fdbm_t **mem)

Dump its list of ifed_t and reload them.

void read (fdbm_t **fed, size_t size)

Symmetric: read.

const dbm_t & const_dbmt () const

bool removeThisDBM (const dbm_t &dbm)

Remove a dbm_t from this fed_t.

void setMutable ()

Ensure this ifed_t is mutable.

Static Public Member Functions

static bool isSubtractionEmpty (const raw_t *dbm, cindex_t dim, const fed_t &fed)

static fed_t subtract (const raw_t *arg1, const raw_t *arg2, cindex_t dim)

Subtract DBM arg1 - DBM arg2 wrapper function.

static fed_t subtract (const dbm_t &arg1, const raw_t *arg2, cindex_t dim)

Private Member Functions

fed_t (ifed_t *ifed)

ifed_t * ifed ()

const ifed_t * ifed () const

bool isMutable () const

Call-backs to ifed_t.

bool isOK () const

void incRef () const

void decRef () const

void decRefImmutable () const

dbm_t & dbmt ()

void toArray (const raw_t **ar) const

Convert its linked list to an array.

void ptr_subtract (const raw_t *arg, cindex_t dim)

Internal subtraction implemention (*this - arg).

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

Similarly with a DBM.

Private Attributes

ifed_t * ifedPtr

Classes

class const_iterator

Const iterator -> iterate though dbm_t. More...

class iterator

Mutable iterator -> iterate though dbm_t. More...

Constructor & Destructor Documentation

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

Initialize a fed_t to empty federation of a given dimension.

Parameters:

dim,: dimension of the federation.

Postcondition:
isEmpty()

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

Standard copy constructor.

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

Wrap a DBM in a federation.

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

cindex_t dim

) [inline]

Copy a DBM matrix in a federation.

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

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

Special constructor to copy the result of a pending operation.

Parameters:

op,: clock operation.

dbm::fed_t::fed_t ( ifed_t * ifed ) [inline, private]

Member Function Documentation

fed_t & dbm::fed_t::add ( const raw_t * arg,

cindex_t dim

) [inline]

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

fed_t & dbm::fed_t::add ( const fed_t & arg ) [inline]

Simply add (list concatenation) DBMs to this federation.

Precondition:
same dimension.

void dbm::fed_t::append ( fdbm_t * arg )

fed_t & dbm::fed_t::append ( fed_t & arg )

Append arg to 'this',.

Postcondition:
arg.isEmpty()

fed_t & dbm::fed_t::appendC ( fed_t arg ) [inline]

fed_t::const_iterator dbm::fed_t::begin ( ) const [inline]

Access to iterators.
Limitation: you cannot modify the original fed_t object otherwise the iterator will be invalidated. In addition, you cannot copy the original either if the non const iterator is used.

fed_t::iterator dbm::fed_t::beginMutable ( ) [inline]

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

cindex_t newDim

)

Resize and change clocks of all the DBMs of this federation.
The updated DBMs 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 DBMs. 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 dbm_t & dbm::fed_t::const_dbmt ( ) const [inline]

Returns:
its first dbm_t,

Precondition:
size() > 0

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

const std::vector< constraint_t > &

)

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

const base::pointer_t< constraint_t > &

)

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

const constraint_t * c,

size_t n

)

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

size_t n

)

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

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

cindex_t j,

int32_t b,

bool isStrict

) [inline]

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

cindex_t j,

int32_t b,

strictness_t s

) [inline]

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

cindex_t j,

raw_t c

)

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

int32_t value

)

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

table,: indirection table for the indices.

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

See also:
dbm_t.

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

cindex_t dim

) const

bool dbm::fed_t::contains ( const DoubleValuation & point ) const [inline]

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

cindex_t dim

) const

bool dbm::fed_t::contains ( const IntValuation & point ) const [inline]

Returns:
true if a point (discrete or "real") is included in this federation (ie in one of its DBMs).

Precondition:
same dimension.

fed_t & dbm::fed_t::convexHull ( )

Convex union of its DBMs.

fed_t & dbm::fed_t::convexReduce ( )

Use a heuristic to recompute parts of the federation as part=convexHull(part)-(convexHull(part)-part).

Returns:
this.

dbm_t & dbm::fed_t::dbmt ( ) [inline, private]

Returns:
its dbm_t,

Precondition:
size() >= 1

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

void dbm::fed_t::decRefImmutable ( ) const [inline, private]

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

cindex_t dim,

double * t

) const

bool dbm::fed_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::fed_t::diagonalExtrapolateLUBounds ( const int32_t * lower,

const int32_t * upper

)

void dbm::fed_t::diagonalExtrapolateMaxBounds ( const int32_t * max )

fed_t & dbm::fed_t::down ( )

Inverse delay (weakest pre-condition) for all the DBMs.

const fed_t::const_iterator dbm::fed_t::end ( ) const [inline]

const fed_t::iterator dbm::fed_t::endMutable ( ) const [inline]

bool dbm::fed_t::eq ( const raw_t * arg,

cindex_t dim

) const [inline]

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

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

Exact (expensive) relations.
See comments on dbm_t. eq: equal, lt: less than, gt: greater than, le: less or equal, ge: greater or equal.
Precondition:
same dimension for eq,lt,le,gt,ge

fed_t::iterator dbm::fed_t::erase ( iterator & iter ) [inline]

relation_t dbm::fed_t::exactRelation ( const raw_t * arg,

cindex_t dim

) const

relation_t dbm::fed_t::exactRelation ( const dbm_t & arg ) const

relation_t dbm::fed_t::exactRelation ( const fed_t & arg ) const

fed_t & dbm::fed_t::expensiveConvexReduce ( )

Try to replace this by convexHull(this)-(convexHull(this)-this).

Returns:
this.

fed_t & dbm::fed_t::expensiveReduce ( )

Remove redundant DBMs (if included in the UNION of the other DBMs).

Postcondition:
same side effect as reduce().

Returns:
this.

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

const int32_t * upper

)

void dbm::fed_t::extrapolateMaxBounds ( const int32_t * max )

Extrapolations:.

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

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

fed_t & dbm::fed_t::freeAllDown ( )

fed_t & dbm::fed_t::freeAllUp ( )

fed_t & dbm::fed_t::freeClock ( cindex_t clock )

Free clock (unconstraint) for all the DBMs.

fed_t & dbm::fed_t::freeDown ( cindex_t clock )

fed_t & dbm::fed_t::freeUp ( cindex_t clock )

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::fed_t::ge ( const raw_t * arg,

cindex_t dim

) const [inline]

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

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

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

Returns:
the dimension of this federation.

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

Only for compatibility with priced federations.

int32_t dbm::fed_t::getUpperMinimumCost ( int 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::fed_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.
The point will belong to one DBM of this federation, it is unspecified which one.
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

Precondition:
same dimension.

bool dbm::fed_t::gt ( const raw_t * arg,

cindex_t dim

) const [inline]

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

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

bool dbm::fed_t::has ( const raw_t * arg,

cindex_t dim

) const

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

Identify test to know if this federation has a specific DBM.
If (dbm_t) arg is empty, then it is trivially true (if same dimension).

bool dbm::fed_t::hasEmpty ( ) const

Returns:
true if this fed_t has an empty dbm_t in its list. Normally this should never occur, unless you play with dbm_t manually with the iterator. This is used mainly for testing.

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

Returns:
a hash value that does not depend on the order of the DBMs but call reduce before to get a reliable value.

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

Similar but test with exact same dbm_t.
Note: an empty federation is an empty list and an empty DBM is an empty zone. Both are compatible since they contain no point but empty_fed.hasSame(empty_dbm) will return false even if the dimensions are the same since an empty fed_t contains no dbm_t at all.

bool dbm::fed_t::hasZero ( ) const

Returns:
true if this DBM contains the zero point.

const ifed_t * dbm::fed_t::ifed ( ) const [inline, private]

ifed_t * dbm::fed_t::ifed ( ) [inline, private]

Returns:
ifedPtr with basic checks.

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

void dbm::fed_t::intern ( )

Try to share the DBMs. Side-effect: affects all copies of this fed_t.

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

cindex_t dim

) const

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

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

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

Precondition:
same dimensions.

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

Returns:
true if it is empty.

bool dbm::fed_t::isIncludedInPredt ( const fed_t & good,

const fed_t & bad

) const

Returns:
true if this fed_t is included in predt(good,bad) This test may terminate earlier than calling le(predt(good,bad)) because predt does not have to be computed in full sometimes.

bool dbm::fed_t::isMutable ( ) const [inline, private]

Call-backs to ifed_t.

bool dbm::fed_t::isOK ( ) const [inline, private]

bool dbm::fed_t::isSubtractionEmpty ( const raw_t * dbm,

cindex_t dim,

const fed_t & fed

) [static]

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

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

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

cindex_t dim

) const

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:
dbm_isValid(arg, dim) and dim == getDimension()

bool dbm::fed_t::isSupersetEq ( const raw_t * arg,

cindex_t dim

) const

Specialized relation test: >= arg (approximate).

bool dbm::fed_t::isUnbounded ( ) const

Returns:
true if this federation has points that can delay infinitely.

bool dbm::fed_t::le ( const raw_t * arg,

cindex_t dim

) const

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

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

bool dbm::fed_t::lt ( const raw_t * arg,

cindex_t dim

) const [inline]

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

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

fed_t & dbm::fed_t::mergeReduce ( ) [inline]

Try to merge DBMs by pairs.

Postcondition:
same side effect as reduce().

Returns:
this.

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

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

fed_t& dbm::fed_t::noReduce ( ) [inline]

This method is useful only for experiments.

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

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

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

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

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

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

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

Intersection and constraint operator (&).

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

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

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

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

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

Overload of operator (): () or (i,j) make no sense here.
fed_t::(i) -> clock access for clock i.
See also:
ClockOperation for more details.

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

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

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

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

Convex union operator (+).
Every DBM of the federation is unified with the argument. To get the convex hull of everything, call this->convexHull() += arg;
Precondition:
same dimension.

fed_t & dbm::fed_t::operator-= ( const raw_t * )

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

fed_t & dbm::fed_t::operator-= ( const fed_t & )

(Set) subtraction operator (-).

Precondition:
same dimension.

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

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

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

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

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

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

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

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

fed_t & dbm::fed_t::operator= ( const fed_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::fed_t::operator== ( const raw_t * ) const [inline]

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

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

Comparisons have the semantics of set inclusion.
Comparisons agains fed_t are approximate and cheap since done between DBMs pair-wise. See dbm_t.
Precondition:
same dimension for the operators < > <= >=, use relation if you don't know.

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

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

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

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

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

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

fed_t & dbm::fed_t::operator|= ( const raw_t * )

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

fed_t & dbm::fed_t::operator|= ( const fed_t & )

(Set) union operator (|).
Inclusion is checked and the operation has the effect of reduce() on the argument.
Precondition:
same dimension.

fed_t & dbm::fed_t::partitionReduce ( )

Find partitions in the federation and reduce them separately.

Returns:
this.

double dbm::fed_t::possibleBackDelay ( const double * point,

cindex_t dim

) const

double dbm::fed_t::possibleBackDelay ( const DoubleValuation & point ) const [inline]

Returns:
the 'almost max' possible delay backward from a point while still staying inside the federation. It is 'almost max' since we want a discrete value, which cannot me the max when we have strict constraints. The precision is 0.5. 0.0 may be returned if the point is too close to a border.

Parameters:

point,: the point to go backward from.

Precondition:
dim = getDimension() && contains(point)

fed_t & dbm::fed_t::predt ( const raw_t * bad,

cindex_t dim

)

fed_t & dbm::fed_t::predt ( const dbm_t & bad )

fed_t & dbm::fed_t::predt ( const fed_t & bad )

predt operation: temporal predecessor of this federation avoiding 'bad'.

Postcondition:
the points in the resulting federation may delay (and stay in the result) until they belong to this federation without entering bad.

Precondition:
same dimension.

relation_t dbm::fed_t::ptr_relation ( const raw_t * arg,

cindex_t dim

) const [private]

Similarly with a DBM.

Precondition:
isPointer()

void dbm::fed_t::ptr_subtract ( const raw_t * arg,

cindex_t dim

) [private]

Internal subtraction implemention (*this - arg).

Precondition:
!isEmpty() && isMutable()

void dbm::fed_t::read ( fdbm_t ** fed,

size_t size

)

Symmetric: read.

Parameters:

fed,size,: a ifed_t[size]

Postcondition:
the ifed list is re-linked and belongs to this fed_t.

fed_t & dbm::fed_t::reduce ( ) [inline]

Remove redundant DBMs (if included in ONE other DBM).

Postcondition:
side effect: all copies of this fed_t are affected so do not mix iterators and reduce().

Returns:
this.

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

cindex_t dim

) const

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

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

Relation (wrt inclusion, approximate).

Returns:
this (relation) arg.

fed_t & dbm::fed_t::relaxAll ( )

Make all constraints (except infinity) non strict for all the DBMs.

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

fed_t & dbm::fed_t::relaxDownClock ( cindex_t clock )

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

Make upper or lower finite bounds non strict for all the DBMs.

See also:
dbm.h.

Returns:
this.

fed_t & dbm::fed_t::relaxUpClock ( cindex_t clock )

Similar for all bounds of a particular clock for all the DBMs.

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

void dbm::fed_t::removeEmpty ( )

Clean-up the federation of its empty dbm_t.
Normally this is never needed except if the mutable iterator is used and makes some dbm_t empty.

bool dbm::fed_t::removeIncludedIn ( const raw_t * arg,

cindex_t dim

)

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

void dbm::fed_t::removeIncludedIn ( const fed_t & arg )

Remove the DBMs that are included in DBMs of arg (pair-wise inclusion checking).
WARNING: If sameAs(arg) then you will empty this federation *and* the argument.
Precondition:
same dimension.

Returns:
!(arg <= *this) if arg is a dbm_t.

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

Remove a dbm_t from this fed_t.
The match uses dbm_t::sameAs(..)
Returns:
true if arg was removed, false otherwise.

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

const uint32_t * bitDst,

size_t bitSize,

cindex_t * table

)

Resize all the DBMs of this federation,.

See also:
dbm_t.
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::fed_t::sameAs ( const fed_t & arg ) const [inline]

Returns:
true if arg has the same internal ifedPtr.

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

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

cindex_t j,

raw_t c

) const

Returns:
true if this federation satisfies a constraint c_ij.

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

void dbm::fed_t::setDimension ( cindex_t dim )

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

void dbm::fed_t::setEmpty ( )

Empty this federation.

fed_t & dbm::fed_t::setInit ( )

(re-)initialize the federation with no constraint.

Postcondition:
size() == 1 if dim > 1, 0 otherwise.

void dbm::fed_t::setMutable ( ) [inline]

Ensure this ifed_t is mutable.

fed_t & dbm::fed_t::setZero ( )

Set this federation to zero (origin).

Postcondition:
size() == 1 if dim > 1, 0 otherwise.

size_t dbm::fed_t::size ( ) const [inline]

Returns:
the number of DBMs in this federation.

void dbm::fed_t::splitExtrapolate ( const constraint_t * begin,

const constraint_t * end,

const int32_t * max

)

"Split-extrapolation".
Split the DBMs with the diagonal constraints given in argument, apply extrapolateMaxBounds on the result, and make sure that the resulting DBMs are still constrained by these diagonals.
Parameters:

begin .. end give the diagonal constraints for splitting (from begin (inclusive) to end (exclusive)).

max is the array of maximal bounds.

fed_t dbm::fed_t::subtract ( const dbm_t & arg1,

const raw_t * arg2,

cindex_t dim

) [static]

fed_t dbm::fed_t::subtract ( const raw_t * arg1,

const raw_t * arg2,

cindex_t dim

) [static]

Subtract DBM arg1 - DBM arg2 wrapper function.

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

cindex_t y

)

Swap clocks x and y.

void dbm::fed_t::toArray ( const raw_t ** ar ) const [private]

Convert its linked list to an array.

Precondition:
ar is of size size()

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

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

fed_t & dbm::fed_t::unionWith ( fed_t & arg )

Union of 2 fed_t.

Postcondition:
arg.isEmpty()

fed_t & dbm::fed_t::unionWithC ( fed_t arg ) [inline]

fed_t & dbm::fed_t::up ( )

Delay (strongest post-condition) for all the DBMs.

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

cindex_t y,

int32_t v

)

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

cindex_t y

)

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

int32_t v

)

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

int32_t v

)

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.

size_t dbm::fed_t::write ( fdbm_t ** mem )

Dump its list of ifed_t and reload them.
This is useful for testing mainly but can be extended later for saving or loading a fed_t.
Parameters:

mem,: a ifed_t[size()]

Postcondition:
isEmpty()

Returns:
size()

Member Data Documentation

ifed_t* dbm::fed_t::ifedPtr [private]

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.cpp

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

1.4.2


Public Member Functions
	fed_t (cindex_t dim=1)
	Initialize a fed_t to empty federation of a given dimension.
	fed_t (const fed_t &arg)
	Standard copy constructor.
	fed_t (const dbm_t &arg)
	Wrap a DBM in a federation.
	fed_t (const raw_t *arg, cindex_t dim)
	Copy a DBM matrix in a federation.
	~fed_t ()
size_t	size () const
cindex_t	getDimension () const
void	setDimension (cindex_t dim)
	Change the dimension of this federation.
bool	isEmpty () const
void	setEmpty ()
	Empty this federation.
void	nil ()
	Short for setDimension(1), has the effect of deallocating the DBMs.
bool	hasZero () const
std::string	toString (const ClockAccessor &) const
int32_t	getUpperMinimumCost (int cost) const
	Computes the biggest lower cost in the zone.
int32_t	getInfimum () const
	Only for compatibility with priced federations.
uint32_t	hash (uint32_t seed=0) const
bool	sameAs (const fed_t &arg) const
void	intern ()
	Try to share the DBMs. Side-effect: affects all copies of this fed_t.
fed_t &	operator= (const fed_t &)
	Overload of standard operators.
fed_t &	operator= (const dbm_t &)
fed_t &	operator= (const raw_t *)
bool	operator== (const fed_t &) const
	Comparisons have the semantics of set inclusion.
bool	operator== (const dbm_t &) const
bool	operator== (const raw_t *) const
bool	operator!= (const fed_t &) const
bool	operator!= (const dbm_t &) const
bool	operator!= (const raw_t *) const
bool	operator< (const fed_t &) const
bool	operator< (const dbm_t &) const
bool	operator< (const raw_t *) const
bool	operator> (const fed_t &) const
bool	operator> (const dbm_t &) const
bool	operator> (const raw_t *) const
bool	operator<= (const fed_t &) const
bool	operator<= (const dbm_t &) const
bool	operator<= (const raw_t *) const
bool	operator>= (const fed_t &) const
bool	operator>= (const dbm_t &) const
bool	operator>= (const raw_t *) const
relation_t	relation (const fed_t &arg) const
	Relation (wrt inclusion, approximate).
relation_t	relation (const dbm_t &arg) const
relation_t	relation (const raw_t *arg, cindex_t dim) const
bool	isSupersetEq (const raw_t *arg, cindex_t dim) const
	Specialized relation test: >= arg (approximate).
bool	eq (const fed_t &arg) const
	Exact (expensive) relations.
bool	eq (const dbm_t &arg) const
bool	eq (const raw_t *arg, cindex_t dim) const
bool	lt (const fed_t &arg) const
bool	lt (const dbm_t &arg) const
bool	lt (const raw_t *arg, cindex_t dim) const
bool	gt (const fed_t &arg) const
bool	gt (const dbm_t &arg) const
bool	gt (const raw_t *arg, cindex_t dim) const
bool	le (const fed_t &arg) const
bool	le (const dbm_t &arg) const
bool	le (const raw_t *arg, cindex_t dim) const
bool	ge (const fed_t &arg) const
bool	ge (const dbm_t &arg) const
bool	ge (const raw_t *arg, cindex_t dim) const
relation_t	exactRelation (const fed_t &arg) const
relation_t	exactRelation (const dbm_t &arg) const
relation_t	exactRelation (const raw_t *arg, cindex_t dim) const
fed_t &	setZero ()
	Set this federation to zero (origin).
fed_t &	setInit ()
	(re-)initialize the federation with no constraint.
fed_t &	convexHull ()
	Convex union of its DBMs.
fed_t &	operator\|= (const fed_t &)
	(Set) union operator (\|).
fed_t &	operator\|= (const dbm_t &)
fed_t &	operator\|= (const raw_t *)
fed_t &	unionWith (fed_t &arg)
	Union of 2 fed_t.
fed_t &	unionWithC (fed_t arg)
fed_t &	add (const fed_t &arg)
	Simply add (list concatenation) DBMs to this federation.
fed_t &	add (const dbm_t &arg)
fed_t &	add (const raw_t *arg, cindex_t dim)
fed_t &	append (fed_t &arg)
	Append arg to 'this',.
fed_t &	appendC (fed_t arg)
void	append (fdbm_t *arg)
fed_t &	operator+= (const fed_t &)
	Convex union operator (+).
fed_t &	operator+= (const dbm_t &)
fed_t &	operator+= (const raw_t *)
fed_t &	operator &= (const fed_t &)
	Intersection and constraint operator (&).
fed_t &	operator &= (const dbm_t &)
fed_t &	operator &= (const raw_t *)
fed_t &	operator &= (const constraint_t &)
fed_t &	operator &= (const base::pointer_t< constraint_t > &)
fed_t &	operator &= (const std::vector< constraint_t > &)
fed_t &	operator-= (const fed_t &)
	(Set) subtraction operator (-).
fed_t &	operator-= (const dbm_t &)
fed_t &	operator-= (const raw_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 fed_t &) const
bool	intersects (const dbm_t &) const
bool	intersects (const raw_t *, cindex_t dim) const
fed_t &	up ()
	Delay (strongest post-condition) for all the DBMs.
fed_t &	down ()
	Inverse delay (weakest pre-condition) for all the DBMs.
fed_t &	freeClock (cindex_t clock)
	Free clock (unconstraint) for all the DBMs.
fed_t &	freeUp (cindex_t clock)
	Free upper or lower bounds only for a particular clock or for all clocks.
fed_t &	freeDown (cindex_t clock)
fed_t &	freeAllUp ()
fed_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
bool	satisfies (const constraint_t &c) const
bool	operator && (const constraint_t &c) const
bool	isUnbounded () const
fed_t &	relaxUp ()
	Make upper or lower finite bounds non strict for all the DBMs.
fed_t &	relaxDown ()
fed_t &	relaxUpClock (cindex_t clock)
	Similar for all bounds of a particular clock for all the DBMs.
fed_t &	relaxDownClock (cindex_t clock)
fed_t &	relaxAll ()
	Make all constraints (except infinity) non strict for all the DBMs.
fed_t &	reduce ()
	Remove redundant DBMs (if included in ONE other DBM).
fed_t &	noReduce ()
	This method is useful only for experiments.
fed_t &	expensiveReduce ()
	Remove redundant DBMs (if included in the UNION of the other DBMs).
fed_t &	mergeReduce ()
	Try to merge DBMs by pairs.
fed_t &	convexReduce ()
	Use a heuristic to recompute parts of the federation as part=convexHull(part)-(convexHull(part)-part).
fed_t &	expensiveConvexReduce ()
	Try to replace this by convexHull(this)-(convexHull(this)-this).
fed_t &	partitionReduce ()
	Find partitions in the federation and reduce them separately.
bool	contains (const IntValuation &point) const
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
double	possibleBackDelay (const DoubleValuation &point) const
double	possibleBackDelay (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	splitExtrapolate (const constraint_t begin, const constraint_t end, const int32_t *max)
	"Split-extrapolation".
void	resize (const uint32_t bitSrc, const uint32_t bitDst, size_t bitSize, cindex_t *table)
	Resize all the DBMs of this federation,.
void	changeClocks (const cindex_t *target, cindex_t newDim)
	Resize and change clocks of all the DBMs of this federation.
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.
fed_t &	predt (const fed_t &bad)
	predt operation: temporal predecessor of this federation avoiding 'bad'.
fed_t &	predt (const dbm_t &bad)
fed_t &	predt (const raw_t *bad, cindex_t dim)
bool	isIncludedInPredt (const fed_t &good, const fed_t &bad) const
bool	has (const dbm_t &arg) const
	Identify test to know if this federation has a specific DBM.
bool	has (const raw_t *arg, cindex_t dim) const
bool	hasSame (const dbm_t &arg) const
	Similar but test with exact same dbm_t.
void	removeIncludedIn (const fed_t &arg)
	Remove the DBMs that are included in DBMs of arg (pair-wise inclusion checking).
bool	removeIncludedIn (const dbm_t &arg)
bool	removeIncludedIn (const raw_t *arg, cindex_t dim)
	fed_t (const ClockOperation< fed_t > &op)
	Special constructor to copy the result of a pending operation.
ClockOperation< fed_t >	operator() (cindex_t clk)
	Overload of operator (): () or (i,j) make no sense here.
bool	isSubtractionEmpty (const raw_t *arg, cindex_t dim) const
bool	isSubtractionEmpty (const dbm_t &arg) const
bool	isSubtractionEmpty (const fed_t &arg) const
void	removeEmpty ()
	Clean-up the federation of its empty dbm_t.
bool	hasEmpty () const
const_iterator	begin () const
	Access to iterators.
const const_iterator	end () const
iterator	beginMutable ()
const iterator	endMutable () const
iterator	erase (iterator &iter)
size_t	write (fdbm_t **mem)
	Dump its list of ifed_t and reload them.
void	read (fdbm_t **fed, size_t size)
	Symmetric: read.
const dbm_t &	const_dbmt () const
bool	removeThisDBM (const dbm_t &dbm)
	Remove a dbm_t from this fed_t.
void	setMutable ()
	Ensure this ifed_t is mutable.
Static Public Member Functions
static bool	isSubtractionEmpty (const raw_t *dbm, cindex_t dim, const fed_t &fed)
static fed_t	subtract (const raw_t arg1, const raw_t arg2, cindex_t dim)
	Subtract DBM arg1 - DBM arg2 wrapper function.
static fed_t	subtract (const dbm_t &arg1, const raw_t *arg2, cindex_t dim)
Private Member Functions
	fed_t (ifed_t *ifed)
ifed_t *	ifed ()
const ifed_t *	ifed () const
bool	isMutable () const
	Call-backs to ifed_t.
bool	isOK () const
void	incRef () const
void	decRef () const
void	decRefImmutable () const
dbm_t &	dbmt ()
void	toArray (const raw_t **ar) const
	Convert its linked list to an array.
void	ptr_subtract (const raw_t *arg, cindex_t dim)
	Internal subtraction implemention (*this - arg).
relation_t	ptr_relation (const raw_t *arg, cindex_t dim) const
	Similarly with a DBM.
Private Attributes
ifed_t *	ifedPtr
Classes
class	const_iterator
	Const iterator -> iterate though dbm_t. More...
class	iterator
	Mutable iterator -> iterate though dbm_t. More...