dbm::pfed_t

dbm::pfed_t Class Reference

A priced federation is a list of priced DBMs. More...

#include <pfed.h>

List of all members.

Public Types

typedef std::slist< PDBM
>::const_iterator const_iterator

Public Member Functions

pfed_t ()

Allocate empty priced federation of dimension 0.

pfed_t (cindex_t dim)

Allocate empty priced federation of dimension dim.

pfed_t (const PDBM pdbm, cindex_t dim)

Allocate a priced federation of dimension dim initialised to pdbm.

pfed_t (const pfed_t &)

The copy constructor implements copy on write.

~pfed_t ()

The destructor decrements the reference count and deallocates the priced DBM when the count reaches zero.

bool constrain (cindex_t i, uint32_t value)

Constrain x(i) to value.

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

Constrain federation to valuations satisfying x(i) - x(j) ~ constraint.

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

Constrain federation to valuations satisfying x(i) - x(j) ~ (b, isStrict).

bool constrain (const constraint_t *constraints, size_t n)

Constrain federation to valuations satisfying the constraints.

bool constrain (const constraint_t &c)

Constrain federation to valuations satisfying c.

int32_t getInfimum () const

Returns the infimum of the federation.

bool satisfies (const constraint_t &c) const

Check if the federation satisfies a given constraint.

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

Check if the federation satisfies a given constraint.

bool isEmpty () const

Returns true iff the federation is empty.

bool isUnbounded () const

uint32_t hash (uint32_t seed) const

Contains a hash of the federation.

bool contains (const DoubleValuation &v) const

Returns true iff the federation contains .

bool contains (const IntValuation &v) const

Returns true iff the federation contains .

void up ()

Delay with the current delay rate.

void up (int32_t rate)

Delay with rate rate.

void updateValue (cindex_t clock, uint32_t value)

Set x(clock) to value.

void updateValueZero (cindex_t clock, int32_t value, cindex_t zero)

Set x(clock) to value.

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)

void setZero ()

Resets the federation to the federation containing only the origin, with a cost of 0.

void setInit ()

Resets the federation to the federation containing all valuations, with a cost of 0.

void setEmpty ()

Resets the federation to the empty federation.

const_iterator begin () const

Returns an iterator to the first zone of the federation.

const_iterator end () const

Returns an iterator to the position after the last zone of the federation.

bool operator== (const pfed_t &) const

pfed_t & operator= (const pfed_t &)

Assignment operator.

pfed_t & operator= (const PDBM)

Assignment operator.

pfed_t & operator|= (const pfed_t &)

Union operator.

pfed_t & operator|= (const PDBM)

Union operator.

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 *)

Not implemented.

relation_t relation (const pfed_t &fed) const

Relation between two priced federations: SUBSET is returned if all zones of this federation are contained in some zone of fed.

int32_t getInfimumValuation (IntValuation &valuation, const bool *free=NULL) const

Returns the infimum of the federation given a partial valuation.

size_t size () const

Returns the number of zones in the federation.

size_t getDimension () const

Returns the dimension of the federation.

void freeUp (cindex_t)

Implementation of the free up operation for priced federations.

void freeDown (cindex_t)

Implementation of the free down operation for priced federations.

template<typename Predicate>

void erase_if (Predicate p)

template<typename Predicate>

void erase_if_not (Predicate p)

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

Returns the bound on x(i) - x(j) of the first zone of the federation.

int32_t getRate (cindex_t) const

size_t analyzeForMinDBM (uint32_t *bitMatrix) const

int32_t getOffsetCost () const

int32_t getSlopeOfDelayTrajectory () const

void setOffsetCost (int32_t)

void setRate (cindex_t, int32_t)

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

relation_t relation (const int32_t *, raw_t *) const

bool isOnZeroCycle (cindex_t clock, cindex_t &result) const

Returns true and a clock in result that is on a zero cycle with clock or false if no such clock exists.

const pfed_t & const_dbmt () const

Static Public Member Functions

static size_t getSizeOfMinDBM (size_t dimension, const int32_t *)

static pfed_t readFromMinDBM (size_t dimension, const int32_t *)

Protected Types

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

Protected Member Functions

void incRef ()

Increment reference count.

void decRef ()

Decrement reference count.

void prepare ()

Prepare federation for modification.

iterator beginMutable ()

Returns a mutable iterator to the beginning of the federation.

iterator endMutable ()

Returns a mutable iterator to the end of the federation.

iterator erase (iterator)

Erases a DBM from the federation and returns an itertor to the successor element.

void add (const PDBM pdbm, size_t dim)

Adds pdbm to the federation.

Protected Attributes

pfed_s * ptr

Pointer to record holding the federation.

Static Protected Attributes

static std::allocator< pfed_s > alloc

Classes

struct pfed_s

Detailed Description

A priced federation is a list of priced DBMs.

Priced federations implement copy on write using reference counting.

Member Typedef Documentation

typedef std::slist<PDBM>::const_iterator dbm::pfed_t::const_iterator

typedef std::slist<PDBM>::iterator dbm::pfed_t::iterator [protected]

Constructor & Destructor Documentation

dbm::pfed_t::pfed_t ( )

Allocate empty priced federation of dimension 0.

dbm::pfed_t::pfed_t ( cindex_t dim ) [explicit]

Allocate empty priced federation of dimension dim.

dbm::pfed_t::pfed_t ( const PDBM pdbm,

cindex_t dim

)

Allocate a priced federation of dimension dim initialised to pdbm.

dbm::pfed_t::pfed_t ( const pfed_t & ) [inline]

The copy constructor implements copy on write.

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

The destructor decrements the reference count and deallocates the priced DBM when the count reaches zero.

Member Function Documentation

void dbm::pfed_t::add ( const PDBM pdbm,

size_t dim

) [protected]

Adds pdbm to the federation.
The reference count on pdbm is incremented by one.

size_t dbm::pfed_t::analyzeForMinDBM ( uint32_t * bitMatrix ) const

Precondition:
size() == 1

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

Returns an iterator to the first zone of the federation.

pfed_t::iterator dbm::pfed_t::beginMutable ( ) [inline, protected]

Returns a mutable iterator to the beginning of the federation.

const pfed_t & dbm::pfed_t::const_dbmt ( ) const [inline]

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

Constrain federation to valuations satisfying c.

Returns:
Returns true if non-empty after operation.

bool dbm::pfed_t::constrain ( const constraint_t * constraints,

size_t n

)

Constrain federation to valuations satisfying the constraints.

Parameters:

constraints Array of length n of constraints.

n length of constraints.

Precondition:
n > 0

Returns:
Returns true if non-empty after operation.

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

cindex_t j,

int32_t b,

bool isStrict

) [inline]

Constrain federation to valuations satisfying x(i) - x(j) ~ (b, isStrict).

Returns:
Returns true if non-empty after operation.

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

cindex_t j,

raw_t constraint

)

Constrain federation to valuations satisfying x(i) - x(j) ~ constraint.

Returns:
Returns true if non-empty after operation.

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

uint32_t value

)

Constrain x(i) to value.

Returns:
Returns true if non-empty after operation.

bool dbm::pfed_t::contains ( const IntValuation & v ) const

Returns true iff the federation contains .

bool dbm::pfed_t::contains ( const DoubleValuation & v ) const

Returns true iff the federation contains .

void dbm::pfed_t::decRef ( ) [protected]

Decrement reference count.

void dbm::pfed_t::diagonalExtrapolateLUBounds ( int32_t * lower,

int32_t * upper

)

void dbm::pfed_t::diagonalExtrapolateMaxBounds ( int32_t * max )

void dbm::pfed_t::down ( )

Not implemented.

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

Returns an iterator to the position after the last zone of the federation.

pfed_t::iterator dbm::pfed_t::endMutable ( ) [inline, protected]

Returns a mutable iterator to the end of the federation.

pfed_t::iterator dbm::pfed_t::erase ( iterator ) [protected]

Erases a DBM from the federation and returns an itertor to the successor element.

template<typename Predicate>

void dbm::pfed_t::erase_if ( Predicate p ) [inline]

template<typename Predicate>

void dbm::pfed_t::erase_if_not ( Predicate p )

void dbm::pfed_t::extrapolateMaxBounds ( int32_t * max )

void dbm::pfed_t::freeClock ( cindex_t clock )

void dbm::pfed_t::freeDown ( cindex_t )

Implementation of the free down operation for priced federations.

See also:
pdbm_freeDown

void dbm::pfed_t::freeUp ( cindex_t )

Implementation of the free up operation for priced federations.

See also:
pdbm_freeUp

int32_t dbm::pfed_t::getCostOfValuation ( const IntValuation & valuation ) const

size_t dbm::pfed_t::getDimension ( ) const [inline]

Returns the dimension of the federation.

int32_t dbm::pfed_t::getInfimum ( ) const

Returns the infimum of the federation.

int32_t dbm::pfed_t::getInfimumValuation ( IntValuation & valuation,

const bool * free = NULL

) const

Returns the infimum of the federation given a partial valuation.

int32_t dbm::pfed_t::getOffsetCost ( ) const

Precondition:
size() == 1

int32_t dbm::pfed_t::getRate ( cindex_t ) const

Precondition:
size() == 1

size_t dbm::pfed_t::getSizeOfMinDBM ( size_t dimension,

const int32_t *

) [static]

int32_t dbm::pfed_t::getSlopeOfDelayTrajectory ( ) const

Precondition:
size() == 1

int32_t dbm::pfed_t::getUpperMinimumCost ( cindex_t ) const

Not implemented.

void dbm::pfed_t::getValuation ( DoubleValuation & cval,

bool * freeC = NULL

) const

Not implemented.

uint32_t dbm::pfed_t::hash ( uint32_t seed ) const

Contains a hash of the federation.

void dbm::pfed_t::incRef ( ) [inline, protected]

Increment reference count.

void dbm::pfed_t::incrementCost ( int32_t value )

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

Not implemented.

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

Returns true iff the federation is empty.

bool dbm::pfed_t::isOnZeroCycle ( cindex_t clock,

cindex_t & result

) const

Returns true and a clock in result that is on a zero cycle with clock or false if no such clock exists.

bool dbm::pfed_t::isUnbounded ( ) const

pfed_t dbm::pfed_t::operator & ( const pfed_t & b ) const

Not implemented.

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

Not implemented.

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

cindex_t j

) const

Returns the bound on x(i) - x(j) of the first zone of the federation.

Precondition:
size() == 1

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

Not implemented.

pfed_t dbm::pfed_t::operator- ( const pfed_t & b ) const

Not implemented.

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

Not implemented.

pfed_t & dbm::pfed_t::operator= ( const PDBM ) [inline]

Assignment operator.

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

Assignment operator.

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

pfed_t & dbm::pfed_t::operator|= ( const PDBM )

Union operator.

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

Union operator.

void dbm::pfed_t::prepare ( ) [protected]

Prepare federation for modification.

pfed_t dbm::pfed_t::readFromMinDBM ( size_t dimension,

const int32_t *

) [static]

relation_t dbm::pfed_t::relation ( const int32_t * ,

raw_t *

) const

See also:
pdbm_relationWithMinDBM()

relation_t dbm::pfed_t::relation ( const pfed_t & fed ) const

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

void dbm::pfed_t::relax ( )

void dbm::pfed_t::relaxUp ( )

Not implemented.

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

cindex_t j,

raw_t constraint

) const

Check if the federation satisfies a given constraint.

Returns:
Returns true if the federation satisfies x(i) - x(j) ~ constraint.

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

Check if the federation satisfies a given constraint.

Returns:
Returns true if the federation satisfies c.

void dbm::pfed_t::setEmpty ( )

Resets the federation to the empty federation.

void dbm::pfed_t::setInit ( )

Resets the federation to the federation containing all valuations, with a cost of 0.

void dbm::pfed_t::setOffsetCost ( int32_t )

void dbm::pfed_t::setRate ( cindex_t ,

int32_t

)

void dbm::pfed_t::setZero ( )

Resets the federation to the federation containing only the origin, with a cost of 0.

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

Returns the number of zones in the federation.

void dbm::pfed_t::splitExtrapolate ( const constraint_t * ,

const constraint_t * ,

const int32_t *

)

Not implemented.

void dbm::pfed_t::swapClocks ( cindex_t ,

cindex_t

)

Not implemented.

void dbm::pfed_t::up ( int32_t rate )

Delay with rate rate.

void dbm::pfed_t::up ( )

Delay with the current delay rate.

void dbm::pfed_t::updateValue ( cindex_t clock,

uint32_t value

)

Set x(clock) to value.

void dbm::pfed_t::updateValueZero ( cindex_t clock,

int32_t value,

cindex_t zero

)

Set x(clock) to value.
x(zero) must be on a zero-cycle with x(clock).

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

bool tryConstraints16,

allocator_t c_alloc,

uint32_t offset

) const

See also:
dbm_writeToMinDBMWithOffset()

Member Data Documentation

std::allocator< pfed_t::pfed_s > dbm::pfed_t::alloc [static, protected]

struct pfed_s* dbm::pfed_t::ptr [protected]

Pointer to record holding the federation.

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

/home/adavid/UPPAAL/trunk/server/modules/include/dbm/pfed.h
/home/adavid/UPPAAL/trunk/server/modules/dbm/pfed.cpp

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

1.4.2


Public Types
typedef std::slist< PDBM >::const_iterator	const_iterator
Public Member Functions
	pfed_t ()
	Allocate empty priced federation of dimension 0.
	pfed_t (cindex_t dim)
	Allocate empty priced federation of dimension dim.
	pfed_t (const PDBM pdbm, cindex_t dim)
	Allocate a priced federation of dimension dim initialised to pdbm.
	pfed_t (const pfed_t &)
	The copy constructor implements copy on write.
	~pfed_t ()
	The destructor decrements the reference count and deallocates the priced DBM when the count reaches zero.
bool	constrain (cindex_t i, uint32_t value)
	Constrain x(i) to value.
bool	constrain (cindex_t i, cindex_t j, raw_t constraint)
	Constrain federation to valuations satisfying x(i) - x(j) ~ constraint.
bool	constrain (cindex_t i, cindex_t j, int32_t b, bool isStrict)
	Constrain federation to valuations satisfying x(i) - x(j) ~ (b, isStrict).
bool	constrain (const constraint_t *constraints, size_t n)
	Constrain federation to valuations satisfying the constraints.
bool	constrain (const constraint_t &c)
	Constrain federation to valuations satisfying c.
int32_t	getInfimum () const
	Returns the infimum of the federation.
bool	satisfies (const constraint_t &c) const
	Check if the federation satisfies a given constraint.
bool	satisfies (cindex_t i, cindex_t j, raw_t constraint) const
	Check if the federation satisfies a given constraint.
bool	isEmpty () const
	Returns true iff the federation is empty.
bool	isUnbounded () const
uint32_t	hash (uint32_t seed) const
	Contains a hash of the federation.
bool	contains (const DoubleValuation &v) const
	Returns true iff the federation contains .
bool	contains (const IntValuation &v) const
	Returns true iff the federation contains .
void	up ()
	Delay with the current delay rate.
void	up (int32_t rate)
	Delay with rate rate.
void	updateValue (cindex_t clock, uint32_t value)
	Set x(clock) to value.
void	updateValueZero (cindex_t clock, int32_t value, cindex_t zero)
	Set x(clock) to value.
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)
void	setZero ()
	Resets the federation to the federation containing only the origin, with a cost of 0.
void	setInit ()
	Resets the federation to the federation containing all valuations, with a cost of 0.
void	setEmpty ()
	Resets the federation to the empty federation.
const_iterator	begin () const
	Returns an iterator to the first zone of the federation.
const_iterator	end () const
	Returns an iterator to the position after the last zone of the federation.
bool	operator== (const pfed_t &) const
pfed_t &	operator= (const pfed_t &)
	Assignment operator.
pfed_t &	operator= (const PDBM)
	Assignment operator.
pfed_t &	operator\|= (const pfed_t &)
	Union operator.
pfed_t &	operator\|= (const PDBM)
	Union operator.
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 *)
	Not implemented.
relation_t	relation (const pfed_t &fed) const
	Relation between two priced federations: SUBSET is returned if all zones of this federation are contained in some zone of fed.
int32_t	getInfimumValuation (IntValuation &valuation, const bool *free=NULL) const
	Returns the infimum of the federation given a partial valuation.
size_t	size () const
	Returns the number of zones in the federation.
size_t	getDimension () const
	Returns the dimension of the federation.
void	freeUp (cindex_t)
	Implementation of the free up operation for priced federations.
void	freeDown (cindex_t)
	Implementation of the free down operation for priced federations.
template<typename Predicate>
void	erase_if (Predicate p)
template<typename Predicate>
void	erase_if_not (Predicate p)
raw_t	operator() (cindex_t i, cindex_t j) const
	Returns the bound on x(i) - x(j) of the first zone of the federation.
int32_t	getRate (cindex_t) const
size_t	analyzeForMinDBM (uint32_t *bitMatrix) const
int32_t	getOffsetCost () const
int32_t	getSlopeOfDelayTrajectory () const
void	setOffsetCost (int32_t)
void	setRate (cindex_t, int32_t)
int32_t *	writeToMinDBMWithOffset (bool minimizeGraph, bool tryConstraints16, allocator_t c_alloc, uint32_t offset) const
relation_t	relation (const int32_t , raw_t ) const
bool	isOnZeroCycle (cindex_t clock, cindex_t &result) const
	Returns true and a clock in result that is on a zero cycle with clock or false if no such clock exists.
const pfed_t &	const_dbmt () const
Static Public Member Functions
static size_t	getSizeOfMinDBM (size_t dimension, const int32_t *)
static pfed_t	readFromMinDBM (size_t dimension, const int32_t *)
Protected Types
typedef std::slist< PDBM >::iterator	iterator
Protected Member Functions
void	incRef ()
	Increment reference count.
void	decRef ()
	Decrement reference count.
void	prepare ()
	Prepare federation for modification.
iterator	beginMutable ()
	Returns a mutable iterator to the beginning of the federation.
iterator	endMutable ()
	Returns a mutable iterator to the end of the federation.
iterator	erase (iterator)
	Erases a DBM from the federation and returns an itertor to the successor element.
void	add (const PDBM pdbm, size_t dim)
	Adds pdbm to the federation.
Protected Attributes
pfed_s *	ptr
	Pointer to record holding the federation.
Static Protected Attributes
static std::allocator< pfed_s >	alloc
Classes
struct	pfed_s