dbm::Federation Class Reference

#include <Federation.h>

List of all members.

Public Member Functions
	~Federation ()
	Destructor: purge all the zones from this federation, ie, give them back to the factory.
void	unshareAllocator ()
	Unshare its allocator.
Federation &	operator= (const Federation &original) throw (std::bad_alloc)
	Operator =.
void	stealDBMs (Federation *fed)
	Steal DBMs from a federation and computes the union with this federation: the argument federation looses its DBMs.
std::ostream &	serialize (std::ostream &os) const
	Serialize this federation to a stream.
void	unserialize (std::istream &is) throw (std::bad_alloc)
	Unserialize this federation from a stream.
std::ostream &	prettyPrint (std::ostream &os) const
	Pretty print this federation to a stream.
cindex_t	getNumberOfClocks () const
	Number of clocks used in this federation: all the zones have the same number of clocks.
void	initToZero ()
	(Re-)initialize the federation so that it contains only 0.
void	initUnconstrained ()
	(Re-)initialize the federation so that it is completely unconstrained.
bool	intersection (const raw_t *dbm)
	Intersection with one DBM.
bool	intersection (const Federation *anotherFed) throw (std::bad_alloc)
	Intersection with a federation.
bool	constrain (cindex_t clockIndexI, cindex_t clockIndexJ, raw_t rawBound)
	Apply a constraint to the federation = tighten a constraint.
bool	constrainN (const constraint_t *constraints, size_t n)
	Apply several constraints to the federation.
bool	constrain (constraint_t c)
	Wrapper for constrain(uint,uint,raw_t).
bool	constrain (cindex_t clockIndexI, cindex_t clockIndexJ, int32_t bound, bool isStrict)
	Wrapper for constrain(uint,uint,raw_t).
bool	constrain (cindex_t clockIndexI, cindex_t clockIndexJ, int32_t bound, strictness_t strictness)
	Wrapper for constrain(uint,uint,raw_t).
bool	satisfies (cindex_t clockIndexI, cindex_t clockIndexJ, raw_t rawConstraint) const
bool	satisfies (constraint_t constraint) const
	Wrapper for satisfies(uint,uint,raw_t).
bool	satisfies (cindex_t clockIndexI, cindex_t clockIndexJ, int32_t bound, bool isStrict) const
	Wrapper for satisfies(uint,uint,raw_t).
bool	satisfies (cindex_t clockIndexI, cindex_t clockIndexJ, int32_t bound, strictness_t strictness) const
	Wrapper for satisfies(uint,uint,raw_t).
void	up ()
	Up operation = strongest post-condition = delay = future computation.
void	down ()
	Down operation = weakest pre-condition = past computation.
bool	isUnbounded () const
bool	isEmpty () const
void	microDelay ()
	"Micro" delay operation: render upper bounds xi <= bound non strict: xi < bound
bool	substract (const raw_t *dbm) throw (std::bad_alloc)
	Substract a DBM from this federation.
bool	substract (const Federation *fed) throw (std::bad_alloc)
	Substract a federation from this federation.
Federation &	operator-= (const Federation &fed) throw (std::bad_alloc)
	For convenience: -= operator.
bool	isMaybeIncludedIn (const Federation *fed)
	Approximate inclusion check: if it is included then it is for sure but if it is not, then maybe it could have been.
bool	isReallyIncludedIn (const Federation *fed)
	Exact inclusion check.
void	freeClock (cindex_t clockIndex)
	Free a given clock: remove all the constraints (except >= 0) for a given clock.
void	updateValue (cindex_t clockIndex, int32_t value)
	Update of the form x := value, where x is a clock and value an integer.
void	updateClock (cindex_t clockIndexI, cindex_t clockIndexJ)
	Update of the form xi := xj, where xi and xj are clocks.
void	updateIncrement (cindex_t clockIndex, int32_t increment)
	Update of the form x += inc, where x is a clock and inc an integer.
void	update (cindex_t clockIndexI, cindex_t clockIndexJ, int32_t increment)
	General update of the form: xi := xj + inc, where xi and xj are clocks and inc an integer.
relation_t	partialRelation (const raw_t *dbm) const
	Partial relation with a DBM (from DBM point of view).
relation_t	relation (const raw_t *dbm) const throw (std::bad_alloc)
	Exact (and very expensive) relation with a DBM, in contrast to partialRelation.
void	unionWith (DBMList_t *fed)
	Compute union of federations with inclusion checking.
void	unionWithCopy (const DBMList_t *fed) throw (std::bad_alloc)
	As unionWith but copy the argument when needed.
void	convexUnion ()
	Compute convex union of the DBMs of this federation.
void	stretchUp ()
	Stretch-up: remove all upper bounds for all clocks.
void	stretchDown (cindex_t clockIndex)
	Stretch-down: remove all lower bounds for a given clock.
void	predt (Federation *bad)
	Operation similar to down but constrained: predecessors of fed avoiding the states that could reach bad.
void	add (const DBMList_t *dbmList) throw (std::bad_alloc)
	Add DBMs to this federation.
Federation *	add (const Federation *arg) throw (std::bad_alloc)
	Add DBMs of a federation to this federation.
Federation &	operator+= (const Federation &arg) throw (std::bad_alloc)
	Operator +=: add DBMs of another federation.
void	reduce ()
	Simple reduce: try to remove redundant DBMs.
void	expensiveReduce ()
	Very EXPENSIVE reduce, follows full semantics of federation.
bool	removePartialIncludedIn (const Federation *arg)
	Remove partially included DBMs in the argument federation.
DBMAllocator_t *	getAllocator ()
	Access to the factory: for allocation/deallocation.
const DBMAllocator_t *	getAllocator () const
	const access to factory, only for debug (use in assert).
const DBMList_t *	getDBMList () const
	const access to the DBMs.
DBMList_t *	getDBMList ()
	Access to the DBMs.
DBMList_t **	getAtDBMList ()
	Access to the DBMs.
raw_t *	getFirstDBM ()
	Access to the first DBM.
size_t	getSize () const
	Size of federation.
raw_t *	newDBM () throw (std::bad_alloc())
	Allocate and add a DBM.
void	reset ()
	Reset the federation to empty.
void	extrapolateMaxBounds (const int32_t *max)
	Classical extrapolation based on maximal bounds, formerly called k-normalization.
void	diagonalExtrapolateMaxBounds (const int32_t *max)
	Diagonal extrapolation based on maximal bounds.
void	extrapolateLUBounds (const int32_t *lower, const int32_t *upper)
	Extrapolation based on lower-upper bounds.
void	diagonalExtrapolateLUBounds (const int32_t *lower, const int32_t *upper)
	Diagonal extrapolation based on lower-upper bounds.
void	initIndexTable (cindex_t newDim)
	Initialize the indirection table to identity.
void	initIndexTable (const uint32_t *activeClocks, size_t size)
	Initialize the indirection table according to a bitstring marking active clocks.
void	initFederation (DBMAllocator_t *dbmf, cindex_t nbClocks)
	Initialize a federation, given a factory and a number of clocks.
void	initFederation (DBMAllocator_t *dbmf, cindex_t nbClocks, const uint32_t *activeClocks, size_t size)
	Initialize a federation, given a factory, a number of clocks, and a bitstring marking the active clocks.
void	changeClocks (const uint32_t *oldClocks, const uint32_t *newClocks, size_t size)
	Change the set of active clocks.
Static Public Member Functions
static Federation *	createFederation (DBMAllocator_t *factory, cindex_t nbClocks) throw (std::bad_alloc)
	Create a federation, given a factory and a number of clocks.
static Federation *	createFederation (const Federation *original) throw (std::bad_alloc)
	Create a federation, given an original federation, ie, copy.
static Federation *	createFederation (DBMAllocator_t *factory, cindex_t nbClocks, const uint32_t *activeClocks, size_t size) throw (std::bad_alloc)
	Create a federation, given a factory, a number of clocks, and an active clock mapping (bit string).
Private Member Functions
void	copyFromFederation (const Federation *original) throw (std::bad_alloc)
	Copy the federation without the index table.
	Federation (DBMAllocator_t *dbmf, cindex_t nbClocks)
	Constructor.
	Federation (const Federation &original) throw (std::bad_alloc)
	Copy constructor.
	Federation (DBMAllocator_t *dbmf, cindex_t nbClocks, const uint32_t *activeClocks, size_t size)
	Constructor with active clocks given.
Static Private Member Functions
static void *	allocateFor (cindex_t maxDim)
	Allocate memory for a Federation of maxDim clocks.
static size_t	getSizeOfFederationFor (cindex_t maxDim)
static size_t	getPaddedIntOffsetFor (cindex_t maxDim)
Private Attributes
DBMFederation_t	dbmFederation
	wrapped federation (C struct)
DBMAllocator_t *	dbmAllocator
	allocator to (de-)allocate DBMs
cindex_t	indexTable []
	indirection index table
Friends
class	state::SymbolicState

---

Constructor & Destructor Documentation

dbm::Federation::~Federation (   )

Destructor: purge all the zones from this federation, ie, give them back to the factory. Warning: the factory does not belong to this federation so it is not destroyed.

dbm::Federation::Federation (  DBMAllocator_t *  dbmf, cindex_t  nbClocks )  [inline, private]

Constructor. Parameters: dbmf,:  zone factory nbClocks,:  number of clocks for all the DBMs in this federation. Postcondition: the federation is empty

dbm::Federation::Federation (  const Federation &  original  )  throw (std::bad_alloc) [inline, private]

Copy constructor. Warning: this calls copy, which means, be careful, therefor it is private.

dbm::Federation::Federation (  DBMAllocator_t *  dbmf, cindex_t  nbClocks, const uint32_t *  activeClocks, size_t  size )  [inline, private]

Constructor with active clocks given. Parameters: dbmf,:  zone factory nbClocks,:  number of clocks for all the DBMs in this federation. activeClocks,size,:  bitstring (of 'size' ints) marking the active clocks. Postcondition: the federation is empty

---

Member Function Documentation

Federation* dbm::Federation::add (  const Federation *  arg  )  throw (std::bad_alloc) [inline]

Add DBMs of a federation to this federation. Precondition: DBMs have the same dimension as this federation.

void dbm::Federation::add (  const DBMList_t *  dbmList  )  throw (std::bad_alloc) [inline]

Add DBMs to this federation. dbmList: list of DBMs Precondition: DBMs have the same dimension as this federation.

static void* dbm::Federation::allocateFor (  cindex_t  maxDim  )  [inline, static, private]

Allocate memory for a Federation of maxDim clocks. The index table is allocated rounded up to the next 32 multiple of maxDim.

void dbm::Federation::changeClocks (  const uint32_t *  oldClocks, const uint32_t *  newClocks, size_t  size )  [inline]

Change the set of active clocks. Parameters: oldClocks,:  old set of active clocks, MUST correspond to the current index table. newClocks,:  new set of active clocks, the index table will be updated according to these clocks size,:  size (int ints) of the bitstrings

bool dbm::Federation::constrain (  cindex_t  clockIndexI, cindex_t  clockIndexJ, int32_t  bound, strictness_t  strictness )  [inline]

Wrapper for constrain(uint,uint,raw_t). Parameters: clockIndexI,clockIndexJ,bound,strictness,:  bound with a strictness for the constraint xi-xj. Precondition: clockIndexI and clockIndexJ < maximal number of clocks and indexTable[clockIndexI and clockIndexJ] < getNumberOfClocks()

bool dbm::Federation::constrain (  cindex_t  clockIndexI, cindex_t  clockIndexJ, int32_t  bound, bool  isStrict )  [inline]

Wrapper for constrain(uint,uint,raw_t). Parameters: clockIndexI,clockIndexJ,bound,isStrict,:  bound with a isStrict flag for the constraint xi-xj. Precondition: clockIndexI and clockIndexJ < maximal number of clocks and indexTable[clockIndexI and clockIndexJ] < getNumberOfClocks()

bool dbm::Federation::constrain (  constraint_t  c  )  [inline]

Wrapper for constrain(uint,uint,raw_t). Parameters: c,:  constraint to set

bool dbm::Federation::constrain (  cindex_t  clockIndexI, cindex_t  clockIndexJ, raw_t  rawBound )  [inline]

Apply a constraint to the federation = tighten a constraint. Parameters: clockIndexI,clockIndexJ,rawBound,:  bound for the constraint xi-xj (raw format) Precondition: clockIndexI and clockIndexJ < maximal number of clocks and indexTable[clockIndexI and clockIndexJ] < getNumberOfClocks() Returns: true if the federation is non empty.

bool dbm::Federation::constrainN (  const constraint_t *  constraints, size_t  n )  [inline]

Apply several constraints to the federation. Parameters: constraints,:  constraints to apply n,:  number of constraints Precondition: constraints is a constraint_t[n], indices i must be s.t. indexTable[i] < getNumberOfClocks() and i < dbmAllocator->maxDim Returns: true if the federation is non empty.

void dbm::Federation::convexUnion (   )  [inline]

Compute convex union of the DBMs of this federation.

void dbm::Federation::copyFromFederation (  const Federation *  original  )  throw (std::bad_alloc) [inline, private]

Copy the federation without the index table. Parameters: original,:  original federation.

static Federation* dbm::Federation::createFederation (  DBMAllocator_t *  factory, cindex_t  nbClocks, const uint32_t *  activeClocks, size_t  size )  throw (std::bad_alloc) [inline, static]

Create a federation, given a factory, a number of clocks, and an active clock mapping (bit string). Parameters: factory,:  factory to (de-)allocate DBMs nbClocks,:  number of clocks (=dimension of the DBMs) activeClocks,size,:  bitstring (of 'size' ints) marking the active clocks Precondition: (activeClocks[0] & 1) == 1 (reference clock), size <= factory->maxDim.

static Federation* dbm::Federation::createFederation (  const Federation *  original  )  throw (std::bad_alloc) [inline, static]

Create a federation, given an original federation, ie, copy. Parameters: original,:  the original federation to copy. Returns: a new federation

static Federation* dbm::Federation::createFederation (  DBMAllocator_t *  factory, cindex_t  nbClocks )  throw (std::bad_alloc) [inline, static]

Create a federation, given a factory and a number of clocks. Parameters: factory,:  factory to (de-)allocate DBMs nbClocks,:  number of clocks for this federation (=dimension of the DBMs) Returns: a new federation

void dbm::Federation::diagonalExtrapolateLUBounds (  const int32_t *  lower, const int32_t *  upper )  [inline]

Diagonal extrapolation based on lower-upper bounds. Most general approximation. See also: dbm_diagonalExtrapolateLUBounds Parameters: lower,:  lower bounds for the active clocks. upper,:  upper bounds for the active clocks. Precondition: lower and upper are a int32_t[getNumberOfClocks()] lower[0] = upper[0] = 0

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

Diagonal extrapolation based on maximal bounds. See also: dbm_diagonalExtrapolateMaxBounds Parameters: max,:  table of maximal constants for the active clocks. Precondition: max is a int32_t[getNumberOfClocks()] max[0] = 0 (reference clock)

void dbm::Federation::down (   )  [inline]

Down operation = weakest pre-condition = past computation.

void dbm::Federation::expensiveReduce (   )  [inline]

Very EXPENSIVE reduce, follows full semantics of federation.

void dbm::Federation::extrapolateLUBounds (  const int32_t *  lower, const int32_t *  upper )  [inline]

Extrapolation based on lower-upper bounds. See also: dbm_extrapolateLUBounds Parameters: lower,:  lower bounds for the active clocks. upper,:  upper bounds for the active clocks. Precondition: lower and upper are int32_t[getNumberOfClocks()] lower[0] = upper[0] = 0 (reference clock)

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

Classical extrapolation based on maximal bounds, formerly called k-normalization. See also: dbm_classicExtrapolateMaxBounds Parameters: max,:  table of maximal constants to use for the active clocks. max is a int32_t[getNumberOfClocks()] max[0] = 0 (reference clock)

void dbm::Federation::freeClock (  cindex_t  clockIndex  )  [inline]

Free a given clock: remove all the constraints (except >= 0) for a given clock. Parameters: clockIndex,:  index of the clock to free Precondition: clockIndex < dbmAllocator->maxDim && indexTable[clockIndex] < getNumberOfClocks()

const DBMAllocator_t* dbm::Federation::getAllocator (   )  const [inline]

const access to factory, only for debug (use in assert).

DBMAllocator_t* dbm::Federation::getAllocator (   )  [inline]

Access to the factory: for allocation/deallocation. Returns: this factory.

DBMList_t** dbm::Federation::getAtDBMList (   )  [inline]

Access to the DBMs. Returns: the pointer to the head of the list of DBMs.

DBMList_t* dbm::Federation::getDBMList (   )  [inline]

Access to the DBMs. Returns: the head of the list of DBMs.

const DBMList_t* dbm::Federation::getDBMList (   )  const [inline]

const access to the DBMs. Returns: the head of the list of DBMs.

raw_t* dbm::Federation::getFirstDBM (   )  [inline]

Access to the first DBM. Precondition: federation not empty.

cindex_t dbm::Federation::getNumberOfClocks (   )  const [inline]

Number of clocks used in this federation: all the zones have the same number of clocks. Returns: number of clocks.

static size_t dbm::Federation::getPaddedIntOffsetFor (  cindex_t  maxDim  )  [inline, static, private]

Returns: size needed in ints in addition to this class. If pointers are on 64 bits then we pad on 64 bits and not 32. The Federation object must be padded on 64 bits too on 64 bits, which is done by the compiler since Federation contains pointers.

size_t dbm::Federation::getSize (   )  const [inline]

Size of federation. Returns: the number of zones in the federation.

static size_t dbm::Federation::getSizeOfFederationFor (  cindex_t  maxDim  )  [inline, static, private]

Returns: needed size for a federation with a given maximal dimension.

void dbm::Federation::initFederation (  DBMAllocator_t *  dbmf, cindex_t  nbClocks, const uint32_t *  activeClocks, size_t  size )  [inline]

Initialize a federation, given a factory, a number of clocks, and a bitstring marking the active clocks. Parameters: dbmf,:  DBM factory nbClocks,:  number of clocks (=dimension of the DBMs) activeClocks,size,:  bitstring (of 'size' ints) marking the active clocks Precondition: nbClocks < dbmf->maxDim and (activeClocks[0] & 1) == 1 (reference clock), size <= dbmf->maxDim/32 rounded up, and the index of the highest bit in activeClocks < dbmAllocator->maxDim.

void dbm::Federation::initFederation (  DBMAllocator_t *  dbmf, cindex_t  nbClocks )  [inline]

Initialize a federation, given a factory and a number of clocks. Parameters: dbmf,:  DBM factory nbClocks,:  number of clocks (=dimension of the DBMs) Precondition: nbClocks < dbmf->maxDim

void dbm::Federation::initIndexTable (  const uint32_t *  activeClocks, size_t  size )  [inline]

Initialize the indirection table according to a bitstring marking active clocks. Warning: the DBMs are all deallocated. Parameters: activeClocks,size,:  bitstring (of 'size' ints) marking active clocks Precondition: (activeClocks[0] & 1) == 1 (always reference clock) and n <= getBitTableSize(), and size > 0 (reference clock).

void dbm::Federation::initIndexTable (  cindex_t  newDim  )  [inline]

Initialize the indirection table to identity. Warning: the DBMs are all deallocated. Parameters: newDim,:  new dimension of all the DBMs

void dbm::Federation::initToZero (   )

(Re-)initialize the federation so that it contains only 0. The federation may be empty or not, it does not matter.

void dbm::Federation::initUnconstrained (   )

(Re-)initialize the federation so that it is completely unconstrained. The federation may be empty or not, it does not matter.

bool dbm::Federation::intersection (  const Federation *  anotherFed  )  throw (std::bad_alloc) [inline]

Intersection with a federation. Parameters: anotherFed,:  federation to intersec with. Returns: true if federation is not empty.

bool dbm::Federation::intersection (  const raw_t *  dbm  )  [inline]

Intersection with one DBM. Parameters: dbm,:  DBM to intersect with. Precondition: DBM dimension == getNumberOfClocks() Returns: true if federation is not empty.

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

Returns: true if the federation is empty.

bool dbm::Federation::isMaybeIncludedIn (  const Federation *  fed  )  [inline]

Approximate inclusion check: if it is included then it is for sure but if it is not, then maybe it could have been. Parameters: fed,:  federation to test Returns: true if this federation is maybe included in fed

bool dbm::Federation::isReallyIncludedIn (  const Federation *  fed  )  [inline]

Exact inclusion check. EXPENSIVE. Parameters: fed,:  federation to test Returns: true if this federation is really included in fed

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

Returns: true if the federation is unbounded, ie, if one zone is unbounded.

void dbm::Federation::microDelay (   )  [inline]

"Micro" delay operation: render upper bounds xi <= bound non strict: xi < bound

raw_t* dbm::Federation::newDBM (   )  throw (std::bad_alloc()) [inline]

Allocate and add a DBM. Returns: newly added and allocated DBM. Postcondition: the DBM is not initialized and is invalid. It *must* be written afterwards.

Federation& dbm::Federation::operator+= (  const Federation &  arg  )  throw (std::bad_alloc) [inline]

Operator +=: add DBMs of another federation.

Federation& dbm::Federation::operator-= (  const Federation &  fed  )  throw (std::bad_alloc) [inline]

For convenience: -= operator. See also: substract

Federation& dbm::Federation::operator= (  const Federation &  original  )  throw (std::bad_alloc) [inline]

Operator =. Precondition: factories are the same.

relation_t dbm::Federation::partialRelation (  const raw_t *  dbm  )  const [inline]

Partial relation with a DBM (from DBM point of view). The result is partial in the sense that it can be dbm_DIFFERENT although it could be refined as dbm_SUBSET. Parameters: dbm,:  DBM to test Precondition: dimension of dbm == getNumberOfClocks() Returns: relation dbm (?) this federation where (?) can be dbm_EQUAL: this federation represents exactly the zone of dbm dbm_SUBSET: dbm is a subset of this federation, ie, is included in one of the DBMs of this federation dbm_SUPERSET: dbm is a superset of this federation, ie, includes all the DBMs of this federation dbm_DIFFERENT: dbm is not (easily) comparable to this federation.

void dbm::Federation::predt (  Federation *  bad  )  [inline]

Operation similar to down but constrained: predecessors of fed avoiding the states that could reach bad. Parameters: bad,:  the list of DBMs to avoid. Precondition: the list of DBMs has the same number of clocks as this federation and the active clocks match. Postcondition: DBMs of bad are deallocated.

std::ostream & dbm::Federation::prettyPrint (  std::ostream &  os  )  const

Pretty print this federation to a stream. Parameters: os,:  output stream.

void dbm::Federation::reduce (   )  [inline]

Simple reduce: try to remove redundant DBMs.

relation_t dbm::Federation::relation (  const raw_t *  dbm  )  const throw (std::bad_alloc) [inline]

Exact (and very expensive) relation with a DBM, in contrast to partialRelation. Parameters: dbm,:  DBM to test Precondition: dimension of dbm == getNumberOfClocks() Returns: relation dbm (?) this federation as partialRelation.

bool dbm::Federation::removePartialIncludedIn (  const Federation *  arg  )  [inline]

Remove partially included DBMs in the argument federation. Returns: TRUE if this federation is not empty afterwards. Parameters: arg,:  argument federation.

void dbm::Federation::reset (   )  [inline]

Reset the federation to empty.

bool dbm::Federation::satisfies (  cindex_t  clockIndexI, cindex_t  clockIndexJ, int32_t  bound, strictness_t  strictness )  const [inline]

Wrapper for satisfies(uint,uint,raw_t). Parameters: clockIndexI,clockIndexJ,bound,strictness,:  bound with a strictness for the constraint xi-xj. Precondition: see satisfies(cindex_t,cindex_t,raw_t)

bool dbm::Federation::satisfies (  cindex_t  clockIndexI, cindex_t  clockIndexJ, int32_t  bound, bool  isStrict )  const [inline]

Wrapper for satisfies(uint,uint,raw_t). Parameters: clockIndexI,clockIndexJ,bound,isStrict,:  bound with a isStrict flag for the constraint xi-xj. Precondition: see satisfies(cindex_t,cindex_t,raw_t)

bool dbm::Federation::satisfies (  constraint_t  constraint  )  const [inline]

Wrapper for satisfies(uint,uint,raw_t). Parameters: constraint,:  the constraint to test Precondition: see satisfies(cindex_t,cindex_t,raw_t)

bool dbm::Federation::satisfies (  cindex_t  clockIndexI, cindex_t  clockIndexJ, raw_t  rawConstraint )  const [inline]

Returns: true if the federation satisfies the constraint. Parameters: clockIndexI,clockIndexJ,rawConstraint,:  constraint (raw format) to be satisfied by xi-xj. Precondition: clockIndexI and clockIndexJ < maximal number of clocks and indexTable[clockIndexI and clockIndexJ] < getNumberOfClocks()

std::ostream & dbm::Federation::serialize (  std::ostream &  os  )  const

Serialize this federation to a stream. Parameters: os,:  output stream.

void dbm::Federation::stealDBMs (  Federation *  fed  )  [inline]

Steal DBMs from a federation and computes the union with this federation: the argument federation looses its DBMs. Parameters: fed,:  federation to steal from. Precondition: getNumberOfClocks() == fed->getNumberOfClocks()

void dbm::Federation::stretchDown (  cindex_t  clockIndex  )  [inline]

Stretch-down: remove all lower bounds for a given clock. Parameters: clockIndex,:  index of the concerned clock. Precondition: clockIndex < dbmAllocator->maxDim && indexTable[clockIndex] < getNumberOfClocks()

void dbm::Federation::stretchUp (   )  [inline]

Stretch-up: remove all upper bounds for all clocks.

bool dbm::Federation::substract (  const Federation *  fed  )  throw (std::bad_alloc) [inline]

Substract a federation from this federation. Parameters: fed,:  federation to substract Precondition: fed->getNumberOfClocks() == getNumberOfClocks() and fed has the same factory. Returns: true if this federation is non empty

bool dbm::Federation::substract (  const raw_t *  dbm  )  throw (std::bad_alloc) [inline]

Substract a DBM from this federation. Parameters: dbm,:  DBM to substract Precondition: dimension of the DBM = getNumberOfClocks() Returns: true if this federation is non empty

void dbm::Federation::unionWith (  DBMList_t *  fed  )  [inline]

Compute union of federations with inclusion checking. Argument is deallocated or belongs to this federation. Parameters: fed,:  list of DBMs to add to this federation.

void dbm::Federation::unionWithCopy (  const DBMList_t *  fed  )  throw (std::bad_alloc) [inline]

As unionWith but copy the argument when needed. Parameters: fed,:  list of DBMs to add.

void dbm::Federation::unserialize (  std::istream &  is  )  throw (std::bad_alloc)

Unserialize this federation from a stream. Parameters: is,:  input stream.

void dbm::Federation::unshareAllocator (   )  [inline]

Unshare its allocator.

void dbm::Federation::up (   )  [inline]

Up operation = strongest post-condition = delay = future computation.

void dbm::Federation::update (  cindex_t  clockIndexI, cindex_t  clockIndexJ, int32_t  increment )  [inline]

General update of the form: xi := xj + inc, where xi and xj are clocks and inc an integer. Warning: same remark as for updateIncrement. Parameters: clockIndexI,clockIndexJ,:  clock indices of clocks (xi,xj) increment,:  increment to apply Precondition: clockIndexI/J < dbmAllocator->maxDim && indexTable[clockIndexI/J] < getNumberOfClocks()

void dbm::Federation::updateClock (  cindex_t  clockIndexI, cindex_t  clockIndexJ )  [inline]

Update of the form xi := xj, where xi and xj are clocks. Parameters: clockIndexI,clockIndexJ,:  clock indices of xi and xj. Precondition: clockIndexI/J < dbmAllocator->maxDim && indexTable[clockIndexI/J] < getNumberOfClocks()

void dbm::Federation::updateIncrement (  cindex_t  clockIndex, int32_t  increment )  [inline]

Update of the form x += inc, where x is a clock and inc an integer. Warning: inc may be < 0. The operation may be wrong when used on an unbounded federation, or if the "decrement" is too big (negative time). The operation is there but be careful in its usage. Decidability is at stake. Parameters: clockIndex,:  index of the clock (x) to increment increment,:  increment to apply Precondition: clockIndex < dbmAllocator->maxDim && indexTable[clockIndex] < getNumberOfClocks()

void dbm::Federation::updateValue (  cindex_t  clockIndex, int32_t  value )  [inline]

Update of the form x := value, where x is a clock and value an integer. Parameters: clockIndex,:  index of the clock (x) to update. value,:  value to set. Precondition: clockIndex < dbmAllocator->maxDim && indexTable[clockIndex] < getNumberOfClocks()

---

Friends And Related Function Documentation

friend class state::SymbolicState [friend]

---

Member Data Documentation

DBMAllocator_t* dbm::Federation::dbmAllocator [private]

allocator to (de-)allocate DBMs

DBMFederation_t dbm::Federation::dbmFederation [private]

wrapped federation (C struct)

cindex_t dbm::Federation::indexTable[] [private]

indirection index table

---

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

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

---