#include "base/intutils.h"
#include "base/bitstring.h"
#include "dbm/mingraph.h"
#include "dbm/dbmfederation.h"
#include "dbm/print.h"
#include "debug/macros.h"
#include "debug/malloc.h"
#include "dbm.h"

Functions
DBMList_t *	dbmf_internAllocate (DBMAllocator_t *factory)
	Allocate DBMs with the factory.
void	dbmf_internDeallocateList (DBMAllocator_t *factory, DBMList_t *dbmList)
	Give back a LIST of DBMs to its factory.
BOOL	dbmf_internCheckFactory (const DBMAllocator_t *factory)
void	dbmf_clearFactory (DBMAllocator_t *factory)
	Clear a factory.
BOOL	dbmf_hasDBM (const DBMList_t *fed, const raw_t *dbm, cindex_t dim)
	Test if a federation has a particular DBM.
size_t	dbmf_getSize (const DBMList_t *dbmList)
	Size of a federation.
void	dbmf_cleanUp (DBMFederation_t *fed, DBMAllocator_t *factory)
	Clean up the federation from empty DBMs.
int	dbmf_copy (DBMFederation_t *dst, const DBMFederation_t src, DBMAllocator_t *factory)
	Copy a federation.
DBMFederation_t	dbmf_copyDBM (const raw_t *dbm, cindex_t dim, DBMAllocator_t *factory)
	Copy a DBM to a federation.
DBMList_t *	dbmf_copyDBM2List (const raw_t *dbm, cindex_t dim, DBMAllocator_t *factory)
	Copy a DBM to a DBMList_t.
static DBMList_t *	dbmf_validCopyDBM2List (const raw_t *dbm, cindex_t dim, BOOL *valid, DBMAllocator_t *factory)
	Internal function: another way to copy and to use *valid instead of a null return code.
DBMList_t *	dbmf_copyDBMList (const DBMList_t *dbmList, cindex_t dim, BOOL *valid, DBMAllocator_t *factory)
	Copy a list of DBMs.
int	dbmf_addZero (DBMFederation_t *fed, DBMAllocator_t *factory)
	Add to the federation 1 DBM that contains only 0.
int	dbmf_addInit (DBMFederation_t *fed, DBMAllocator_t *factory)
	Add to the federation 1 DBM that is not constrained (all clocks >= 0, that's all).
BOOL	dbmf_union (DBMFederation_t *fed, DBMList_t *dbmList, DBMAllocator_t *factory)
	Union of a list of DBMs and a federation: add DBMs to the federation.
BOOL	dbmf_unionWithCopy (DBMFederation_t *fed, const DBMList_t *dbmList, DBMAllocator_t *factory, BOOL *valid)
	Union of a list of DBMs and a federation: add DBMs to the federation.
void	dbmf_convexUnion (raw_t *dbm, cindex_t dim, const DBMList_t *dbmList)
	Computes the convex hull union between one DBM and a list of DBMs: dbm = dbm + list of dbm.
void	dbmf_convexUnionWithSelf (DBMFederation_t *fed, DBMAllocator_t *factory)
	Computes the convex hull union from all the DBMs of a federation.
DBMList_t *	dbmf_intersection (const raw_t *dbm, cindex_t dim, const DBMList_t *dbmList, BOOL *valid, DBMAllocator_t *factory)
	Computes the intersection between one DBM and a list of DBMs = dbm intersec list of dbm.
DBMList_t *	dbmf_intersectionWithFederation (const DBMList_t *fed1, const DBMList_t *fed2, cindex_t dim, BOOL *valid, DBMAllocator_t *factory)
	Computes the intersection between 2 federations.
BOOL	dbmf_intersectsDBM (DBMFederation_t *fed, const raw_t *dbm, DBMAllocator_t *factory)
	Computes the intersection between one DBM and a federation.
int	dbmf_intersectsFederation (DBMFederation_t *fed1, const DBMList_t *fed2, DBMAllocator_t *factory)
	Computes the intersection between one federation and a federation.
BOOL	dbmf_DBMsHaveIntersection (const DBMList_t *dbmList, const raw_t *dbm, cindex_t dim)
	Test if a list of DBMs and a DBM have an intersection.
void	dbmf_constrainN (DBMFederation_t *fed, const constraint_t *constraints, size_t n, DBMAllocator_t *factory)
	Constrain a federation with several constraints.
void	dbmf_constrainIndexedN (DBMFederation_t *fed, const cindex_t *indexTable, const constraint_t *constraints, size_t n, DBMAllocator_t *factory)
	Constrain a federation with several constraints using an index table to translate constraint indices to DBM indices.
void	dbmf_constrain1 (DBMFederation_t *fed, cindex_t i, cindex_t j, raw_t constraint, DBMAllocator_t *factory)
	Constrain a federation with one constraint constraint1 once is cheaper than constrainN with 1 constraintN with n > 1 is cheaper than constrain1 n times.
void	dbmf_up (DBMFederation_t fed)
	Up/delay operation (strongest post-condition).
void	dbmf_down (DBMFederation_t fed)
	Down operation (weakest pre-condition).
void	dbmf_reduce (DBMFederation_t *fed, DBMAllocator_t *factory)
	Reduce a federation: remove DBMs that are included in other DBMs of the same federation.
int	dbmf_expensiveReduce (DBMFederation_t *fed, DBMAllocator_t *factory)
	Reduce a federation: remove DBMs that are redundant.
void	dbmf_freeClock (DBMFederation_t fed, cindex_t clock)
	Free operation: remove all constraints for a given clock.
void	dbmf_updateValue (DBMFederation_t fed, cindex_t clock, int32_t value)
	Update a clock value: x := value.
void	dbmf_updateClock (DBMFederation_t fed, cindex_t x, cindex_t y)
	Copy a clock: x := y.
void	dbmf_updateIncrement (DBMFederation_t fed, cindex_t clock, int32_t value)
	Increment a clock: x += value.
void	dbmf_update (DBMFederation_t fed, cindex_t x, cindex_t y, int32_t value)
	General update: x := x + value.
BOOL	dbmf_satisfies (const DBMFederation_t fed, cindex_t i, cindex_t j, raw_t constraint)
	Check if a federation satisfies a constraint.
BOOL	dbmf_isUnbounded (const DBMFederation_t fed)
	Test if a federation is unbounded, ie, if one of its DBM is unbounded.
relation_t	dbmf_partialRelation (const raw_t *dbm, const DBMFederation_t fed)
	Partial relation between one DBM and a federation: apply the relation to all the DBMs of a federation.
BOOL	dbmf_isIncludedIn (const raw_t *dbm, const DBMList_t *dbmList, cindex_t dim)
	Test if a DBM is included in a list of DBMs.
BOOL	dbmf_areDBMsIncludedIn (const DBMList_t *l1, const DBMList_t *l2, cindex_t dim)
	Test if all the DBMs of l1 are included in some DBMs of l2.
BOOL	dbmf_areDBMsReallyIncludedIn (const DBMList_t *l1, const DBMFederation_t l2, BOOL *valid, DBMAllocator_t *factory)
	Test if all the DBMs of l1 are included semantically in l2.
BOOL	dbmf_removePartialIncluded (DBMFederation_t *fed, const DBMList_t *arg, DBMAllocator_t *factory)
	Remove DBMs of fed that are (partially) included in arg.
relation_t	dbmf_relation (const raw_t *dbm, const DBMFederation_t fed, BOOL *valid, DBMAllocator_t *factory)
	Relation between one DBM and a federation.
void	dbmf_stretchUp (DBMFederation_t fed)
	Stretch-up operation for approximation.
void	dbmf_stretchDown (DBMFederation_t fed, cindex_t clock)
	Stretch-down operation for approximation.
void	dbmf_microDelay (DBMFederation_t fed)
	Smallest possible delay.
BOOL	dbmf_areEqual (const DBMFederation_t fed1, const DBMFederation_t fed2, BOOL *valid, DBMAllocator_t *factory)
	Test semantic equality.
BOOL	dbmf_isPointIncluded (const int32_t *pt, const DBMFederation_t fed)
	Check if a discrete point is included in a federation.
BOOL	dbmf_isRealPointIncluded (const double *pt, const DBMFederation_t fed)
	Check if a real point is included in a federation.
static BOOL	dbmf_isSubstractEqualToIdentity (const raw_t *dbm1, const raw_t *dbm2, cindex_t dim, const uint32_t *bitMatrix, size_t nbConstraints)
static DBMList_t *	dbmf_internSubstractDBMFromDBM (const raw_t *dbm1, const raw_t *dbm2, cindex_t dim, BOOL *valid, DBMAllocator_t *factory, const uint32_t *bits, size_t nbConstraints)
DBMList_t *	dbmf_substractDBMFromDBM (const raw_t *dbm1, const raw_t *dbm2, cindex_t dim, BOOL *valid, DBMAllocator_t *factory)
	Substraction operation: computes C = A - B.
DBMFederation_t	dbmf_substractDBMFromFederation (const DBMFederation_t fed, const raw_t *dbm, BOOL *valid, DBMAllocator_t *factory)
	Substraction operation: computes C = A - B.
DBMFederation_t	dbmf_substractFederationFromFederation (const DBMFederation_t fed1, const DBMFederation_t fed2, BOOL *valid, DBMAllocator_t *factory)
	Substraction operation: computes C = A - B.
DBMList_t *	dbmf_substractFederationFromDBM (const raw_t *dbm, const DBMFederation_t fed, BOOL *valid, DBMAllocator_t *factory)
	Substraction operation: computes C = A - B.
int	dbmf_substractDBM (DBMFederation_t *fed, const raw_t *dbm, DBMAllocator_t *factory)
	Substraction operation: computes A = A - B.
int	dbmf_substractFederation (DBMFederation_t *fed1, const DBMList_t *toSubstract, DBMAllocator_t *factory)
	Substraction operation: computes A = A - B.
BOOL	simpleBad (const raw_t *good, const raw_t *bad, cindex_t dim, DBMList_t **toSubtract, BOOL *valid, DBMAllocator_t *factory)
int	dbmf_predt (DBMFederation_t *goodF, DBMFederation_t *badF, DBMAllocator_t *factory)
	Operation similar to down but constrained: predecessors of fed avoiding the states that could reach bad.
void	dbmf_shrinkExpand (DBMFederation_t *fed, const uint32_t *bitSrc, const uint32_t *bitDst, size_t bitSize, cindex_t *table, DBMAllocator_t *factory)
	Similarly, on federations.
void	dbmf_extrapolateMaxBounds (DBMFederation_t fed, const int32_t *max)
	Classical extrapolation based on maximal bounds, formerly called k-normalization.
void	dbmf_diagonalExtrapolateMaxBounds (DBMFederation_t fed, const int32_t *max)
	Diagonal extrapolation based on maximal bounds.
void	dbmf_extrapolateLUBounds (DBMFederation_t fed, const int32_t *lower, const int32_t *upper)
	Extrapolation based on lower-upper bounds.
void	dbmf_diagonalExtrapolateLUBounds (DBMFederation_t fed, const int32_t *lower, const int32_t *upper)
	Diagonal extrapolation based on lower-upper bounds.
Variables
int	allocatedhop

---

Function Documentation

int dbmf_addInit (  DBMFederation_t *  fed, DBMAllocator_t *  factory )

Add to the federation 1 DBM that is not constrained (all clocks >= 0, that's all). Parameters: fed,:  federation factory,:  compatible factory Returns: 0 if success, -1 if out-of-memory Precondition: factory != NULL && factory->dim >= fed->dim

int dbmf_addZero (  DBMFederation_t *  fed, DBMAllocator_t *  factory )

Add to the federation 1 DBM that contains only 0. See also: dbm_zero. Parameters: fed,:  federation factory,:  compatible factory Returns: 0 if success, -1 if out-of-memory Precondition: factory != NULL & factory->dim >= fed->dim fed is initialized or contains valid DBMs

BOOL dbmf_areDBMsIncludedIn (  const DBMList_t *  l1, const DBMList_t *  l2, cindex_t  dim )

Test if all the DBMs of l1 are included in some DBMs of l2. Parameters: l1,l2,:  lists of DBMs to test. dim,:  dimension of all the DBMs. Returns: TRUE if forall DBMs d1 of l1, there exists d2 in l2 s.t. d1 included in d2.

BOOL dbmf_areDBMsReallyIncludedIn (  const DBMList_t *  l1, const DBMFederation_t  l2, BOOL *  valid, DBMAllocator_t *  factory )

Test if all the DBMs of l1 are included semantically in l2. Parameters: l1,l2,:  lists of DBMs to test. valid,:  to tell if the result is valid (invalid = out of memory occured) factory,:  the DBM allocator Precondition: all DBMs of fed are of dimension fed.dim factory->maxDim >= fed.dim Returns: TRUE if forall DBMs d of l1, d included in federation l2.

BOOL dbmf_areEqual (  const DBMFederation_t  fed1, const DBMFederation_t  fed2, BOOL *  valid, DBMAllocator_t *  factory )

Test semantic equality. Expensive test, computes fed1-fed2 and fed2-fed1. This is *very* expensive. Parameters: fed1,fed2,:  federations to test. factory,:  compatible factory valid,:  pointer to validate internal memory allocation. Returns: TRUE if fed1 == fed2, FALSE otherwise. Precondition: factory->dim >= fed1.dim && factory->dim >= fed2.dim, valid != NULL Postcondition: if *valid == FALSE then the result cannot be trusted and the factory is reset.

void dbmf_cleanUp (  DBMFederation_t *  fed, DBMAllocator_t *  factory )

Clean up the federation from empty DBMs. Operations on federations assume that the DBMs in the federation are not empty, so if for some strange reason you have empty DBMs there then remove them. Parameters: fed,:  federation to clean up. factory,:  allocator for deallocation. Precondition: factory->dim >= fed->dim

void dbmf_clearFactory (  DBMAllocator_t *  factory  )

Clear a factory. Parameters: factory,:  factory to clear (deallocate its freeDBM)

void dbmf_constrain1 (  DBMFederation_t *  fed, cindex_t  i, cindex_t  j, raw_t  constraint, DBMAllocator_t *  factory )

Constrain a federation with one constraint constraint1 once is cheaper than constrainN with 1 constraintN with n > 1 is cheaper than constrain1 n times. Parameters: fed,:  federation i,j,constraint,:  constraint for xi-xj to use factory,:  compatible factory Precondition: valid constraint: i != j & i < fed->dim & j < fed->dim factory != NULL & factory->dim >= fed->dim

void dbmf_constrainIndexedN (  DBMFederation_t *  fed, const cindex_t *  indexTable, const constraint_t *  constraints, size_t  n, DBMAllocator_t *  factory )

Constrain a federation with several constraints using an index table to translate constraint indices to DBM indices. Parameters: fed,:  federation indexTable,:  table for index translation constraints,n,:  the n constraints to use. factory,:  compatible factory Precondition: valid constraints: not of the form xi-xi <= something indexTable[constraints[*].{i,j}] < fed->dim and no out-of-bound for indexTable factory != NULL & factory->dim >= fed->dim

void dbmf_constrainN (  DBMFederation_t *  fed, const constraint_t *  constraints, size_t  n, DBMAllocator_t *  factory )

Constrain a federation with several constraints. Parameters: fed,:  federation constraints,n,:  the n constraints to use. factory,:  compatible factory Precondition: valid constraints: not of the form xi-xi <= something constraints[*].{i,j} < fed->dim factory != NULL & factory->dim >= fed->dim

void dbmf_convexUnion (  raw_t *  dbm, cindex_t  dim, const DBMList_t *  dbmList )

Computes the convex hull union between one DBM and a list of DBMs: dbm = dbm + list of dbm. Parameters: dbm,:  DBM dim,:  dimension of all the DBMs dbmList,:  list of DBMs Precondition: all the DBMs are of dimension dim dbmList != NULL dbm != NULL

void dbmf_convexUnionWithSelf (  DBMFederation_t *  fed, DBMAllocator_t *  factory )

Computes the convex hull union from all the DBMs of a federation. Parameters: fed,:  federation factory,:  compatible factory Precondition: factory != NULL & factory->dim >= fed->dim Postcondition: the federation has only one DBM = union of all previous DBMs.

int dbmf_copy (  DBMFederation_t *  dst, const DBMFederation_t  src, DBMAllocator_t *  factory )

Copy a federation. Parameters: src,:  source dst,:  destination factory,:  compatible factory Returns: 0 if success, -1 if out-of-memory Precondition: factory != NULL && factory->dim >= src->dim && factory->dim >= dst->dim all DBMs were obtained from factory dst is initialized or contains DBMs Postcondition: order of DBMs is preserved if out-of-memory then dst is emptied

DBMFederation_t dbmf_copyDBM (  const raw_t *  dbm, cindex_t  dim, DBMAllocator_t *  factory )

Copy a DBM to a federation. Parameters: dbm,:  DBM to copy dim,:  dimension of the DBM factory,:  compatible factory Precondition: factory != NULL && factory->dim >= dim && dim && dim > 0 Returns: federation with a copy of dbm Postcondition: if out-of-memory then the federation is empty.

DBMList_t* dbmf_copyDBM2List (  const raw_t *  dbm, cindex_t  dim, DBMAllocator_t *  factory )

Copy a DBM to a DBMList_t. Parameters: dbm,:  DBM to copy dim,:  dimension of the DBM factory,:  compatible factory Precondition: factory != NULL && factory->dim >= dim && dim && dim > 0 Returns: a copy of dbm as a DBMList_t or NULL if out-of-memory

DBMList_t* dbmf_copyDBMList (  const DBMList_t *  dbmList, cindex_t  dim, BOOL *  valid, DBMAllocator_t *  factory )

Copy a list of DBMs. Parameters: dbmList,:  list to copy dim,:  dimension of the DBMs factory,:  compatible factory valid,:  pointer for validation (memory allocation) Returns: copy of dbmList. Precondition: factory->maxDim >= dim, valid != NULL Postcondition: order is respected, *valid = FALSE if out-of-memory (and nothing is copied), TRUE if allocation successful.

BOOL dbmf_DBMsHaveIntersection (  const DBMList_t *  dbmList, const raw_t *  dbm, cindex_t  dim )

Test if a list of DBMs and a DBM have an intersection. Parameters: dbmList,:  list of DBMs. dbm,:  DBM to test. dim,:  dimension of all the DBMs. Returns: TRUE if there is an intersection, FALSE otherwise.

void dbmf_diagonalExtrapolateLUBounds (  DBMFederation_t  fed, const int32_t *  lower, const int32_t *  upper )

Diagonal extrapolation based on lower-upper bounds. Most general approximation. Note: you may want to call dbmf_reduce afterwards. See also: dbm_diagonalExtrapolateLUBounds Parameters: fed,:  federation lower,:  lower bounds. upper,:  upper bounds. Precondition: fed->dim > 0 lower and upper are a int32_t[fed->dim] lower[0] = upper[0] = 0

void dbmf_diagonalExtrapolateMaxBounds (  DBMFederation_t  fed, const int32_t *  max )

Diagonal extrapolation based on maximal bounds. Note: you may want to call dbmf_reduce afterwards. See also: dbm_diagonalExtrapolateMaxBounds Parameters: fed,:  federation max,:  table of maximal constants. Precondition: fed->dim > 0 max is a int32_t[fed->dim] max[0] = 0 (reference clock)

void dbmf_down (  DBMFederation_t  fed  )

Down operation (weakest pre-condition). Parameters: fed,:  federation.

int dbmf_expensiveReduce (  DBMFederation_t *  fed, DBMAllocator_t *  factory )

Reduce a federation: remove DBMs that are redundant. This computes substractions to determine if a DBM should be kept or not. This function is here only for experimental purposes and should not be used in practice because of its horrible complexity: O(dim^(4*size)). Memory consumption may explode just for the needs of one "reduce" computation (and thus it is not a reduce anymore). Parameters: fed,:  federation to reduce factory,:  compatible factory Precondition: factory != NULL & fed != NULL & factory->dim >= fed->dim Returns: 0 if internal allocations were successful, -1 otherwise. If -1 is returned then there is no guarantee that fed is reduced. The factory is reset if -1 is returned to try to free memory.

void dbmf_extrapolateLUBounds (  DBMFederation_t  fed, const int32_t *  lower, const int32_t *  upper )

Extrapolation based on lower-upper bounds. Note: you may want to call dbmf_reduce afterwards. See also: dbm_extrapolateLUBounds Parameters: fed,:  federation lower,:  lower bounds. upper,:  upper bounds. Precondition: fed->dim > 0 lower and upper are int32_t[fed->dim] lower[0] = upper[0] = 0 (reference clock)

void dbmf_extrapolateMaxBounds (  DBMFederation_t  fed, const int32_t *  max )

Classical extrapolation based on maximal bounds, formerly called k-normalization. Note: you may want to call dbmf_reduce afterwards. See also: dbm_classicExtrapolateMaxBounds Parameters: fed,:  federation max,:  table of maximal constants to use for the clocks. max is a int32_t[fed->dim] max[0] = 0 (reference clock)

void dbmf_freeClock (  DBMFederation_t  fed, cindex_t  clock )

Free operation: remove all constraints for a given clock. Parameters: fed,:  federation clock,:  clock to free Precondition: clock > 0 & clock < fed->dim

size_t dbmf_getSize (  const DBMList_t *  dbmList  )

Size of a federation. Parameters: dbmList,:  list of DBMs (maybe NULL). Returns: size of the list.

BOOL dbmf_hasDBM (  const DBMList_t *  fed, const raw_t *  dbm, cindex_t  dim )

Test if a federation has a particular DBM. Useful for testing. This is not an inclusion check, only a DBM match function. Parameters: fed,:  federation. dbm,:  DBM to test. Returns: TRUE if dbm is in fed, FALSE otherwise.

DBMList_t* dbmf_internAllocate (  DBMAllocator_t *  factory  )

Allocate DBMs with the factory. Parameters: factory  Returns: allocated DBMList_t or NULL if out-of-memory Precondition: factory != NULL

BOOL dbmf_internCheckFactory (  const DBMAllocator_t *  factory  )

void dbmf_internDeallocateList (  DBMAllocator_t *  factory, DBMList_t *  dbmList )

Give back a LIST of DBMs to its factory. Parameters: factory,:  factory (= owner) dbmList,:  DBM list to deallocate Precondition: dbm was obtained from dbmf_allocate(factory)

static DBMList_t* dbmf_internSubstractDBMFromDBM (  const raw_t *  dbm1, const raw_t *  dbm2, cindex_t  dim, BOOL *  valid, DBMAllocator_t *  factory, const uint32_t *  bits, size_t  nbConstraints )  [static]

DBMList_t* dbmf_intersection (  const raw_t *  dbm, cindex_t  dim, const DBMList_t *  dbmList, BOOL *  valid, DBMAllocator_t *  factory )

Computes the intersection between one DBM and a list of DBMs = dbm intersec list of dbm. result = dbm intersected with dbmList Parameters: dbm,:  DBM dim,:  dimension of all the DBMs dbmList,:  list of DBMs factory,:  compatible factory valid,:  where to validate the result Precondition: all the DBMs are of dimension dim dbmList != NULL dbm != NULL valid != NULL Returns: the result of dbm intersec dbmList (may be NULL) and set valid to FALSE if out-of-memory (and return NULL), TRUE otherwise

DBMList_t* dbmf_intersectionWithFederation (  const DBMList_t *  fed1, const DBMList_t *  fed2, cindex_t  dim, BOOL *  valid, DBMAllocator_t *  factory )

Computes the intersection between 2 federations. The arguments are preserved, the result is a newly allocated federation (list of DBMs). Arguments are DBMList_t* for more flexibility. Parameters: fed1,fed2,:  federations (lists of DBMs) to compute intersection of (may be both NULL). dim,:  dimension of all the DBMs valid,:  where to validate the result factory,:  compatible factory Precondition: all the DBMs are of dimension dim valid != NULL Returns: the result as a newly allocated DBM list (maybe NULL if intersection is empty).

BOOL dbmf_intersectsDBM (  DBMFederation_t *  fed, const raw_t *  dbm, DBMAllocator_t *  factory )

Computes the intersection between one DBM and a federation. result = updated fed = fed intersected with dbm. Parameters: fed,:  federation dbm,:  DBM factory,:  factory for deallocation of DBMs Returns: fed->dbmList != NULL

int dbmf_intersectsFederation (  DBMFederation_t *  fed1, const DBMList_t *  fed2, DBMAllocator_t *  factory )

Computes the intersection between one federation and a federation. result = updated fed1 = fed1 intersected with fed2. Parameters: fed1,fed2,:  federations factory,:  factory for deallocation of DBMs Precondition: DBMs in fed2 have the same dimension as those in fed1. fed1 != NULL, fed2 may be NULL factory is a compatible factory Returns: -1 if out-of-memory, 0 otherwise.

BOOL dbmf_isIncludedIn (  const raw_t *  dbm, const DBMList_t *  dbmList, cindex_t  dim )

Test if a DBM is included in a list of DBMs. Parameters: dbm,:  dbm to test. dbmList,:  list argument. dim,:  dimension of all the DBMs. Returns: TRUE if dbm is included in a DBM of dbmList, FALSE otherwise.

BOOL dbmf_isPointIncluded (  const int32_t *  pt, const DBMFederation_t  fed )

Check if a discrete point is included in a federation. Parameters: fed,:  federation pt,:  point Precondition: pt is a int32_t[fed->dim] Returns: TRUE if pt satisfies the constraints of one DBM in fed, FALSE otherwise

BOOL dbmf_isRealPointIncluded (  const double *  pt, const DBMFederation_t  fed )

Check if a real point is included in a federation. Parameters: fed,:  federation pt,:  point Precondition: pt is a int32_t[fed->dim] Returns: TRUE if pt satisfies the constraints of one DBM in fed, FALSE otherwise

static BOOL dbmf_isSubstractEqualToIdentity (  const raw_t *  dbm1, const raw_t *  dbm2, cindex_t  dim, const uint32_t *  bitMatrix, size_t  nbConstraints )  [static]

BOOL dbmf_isUnbounded (  const DBMFederation_t  fed  )

Test if a federation is unbounded, ie, if one of its DBM is unbounded. Parameters: fed,:  federation to test Returns: TRUE if one of its DBM is unbounded, FALSE otherwise

void dbmf_microDelay (  DBMFederation_t  fed  )

Smallest possible delay. Render upper bounds xi-x0 <= ci0 non strict. Parameters: fed,:  federation

relation_t dbmf_partialRelation (  const raw_t *  dbm, const DBMFederation_t  fed )

Partial relation between one DBM and a federation: apply the relation to all the DBMs of a federation. This relation computation is partial in the sense that it will miss inclusions that result from the (non-convex) union of several DBMs, ie, the true semantics of a federation. Parameters: dbm,:  DBM to test fed,:  federation Precondition: dbm is of dimension fed->dim, dbm closed non empty Returns: safe approximate relation: dbm_SUBSET if dbm included in one DBM of fed dbm_SUPERSET if dbm includes all DBMs of fed dbm_EQUAL if subset & superset dbm_DIFFERENT otherwise

int dbmf_predt (  DBMFederation_t *  fed, DBMFederation_t *  bad, DBMAllocator_t *  factory )

Operation similar to down but constrained: predecessors of fed avoiding the states that could reach bad. Parameters: fed,:  federation to compute the predecessors from. bad,:  list of DBMs to avoid factory,:  DBM allocator Precondition: fed->dim <= factory->dim, all DBMs of bad are of dimension fed->dim, fed!=NULL, factory!=NULL. Postcondition: bad is deallocated fed contains all the (symbolic) states from which you can reach the original fed while avoiding bad. Returns: -1 if out-of-memory and fed is empty, 0 otherwise. THIS IMPLEMENTATION IS KNOWN TO BE WRONG. Please use the API from DBM v2.x. fed_t::predt is correct.

void dbmf_reduce (  DBMFederation_t *  fed, DBMAllocator_t *  factory )

Reduce a federation: remove DBMs that are included in other DBMs of the same federation. Cost: 1/2 * dim^2 * (nb DBMs)^2 This performs simple inclusion checks between the DBMs. Parameters: fed,:  federation to reduce factory,:  compatible factory Precondition: factory != NULL & fed != NULL & factory->dim >= fed->dim

relation_t dbmf_relation (  const raw_t *  dbm, const DBMFederation_t  fed, BOOL *  valid, DBMAllocator_t *  factory )

Relation between one DBM and a federation. This computation is more expensive but it is correct with respect to the semantics of a federation. Parameters: dbm,:  DBM to test fed,:  federation factory,:  compatible factory valid,:  pointer to validate internal memory allocation. Precondition: dbm is of dimension fed->dim, dbm closed non empty, factory->dim >= fed.dim, valid != NULL Returns: the relation between dbm and fed. The result is validated by the flag *valid. Postcondition: if *valid = FALSE then the relation cannot be computed, dbm_DIFFERENT is returned, and the factory is reset.

BOOL dbmf_removePartialIncluded (  DBMFederation_t *  fed, const DBMList_t *  arg, DBMAllocator_t *  factory )

Remove DBMs of fed that are (partially) included in arg. Returns: TRUE if fed is not empty afterwards, FALSE otherwise. Parameters: fed,:  federation to shrink arg,:  list of DBM to test for inclusion factory,:  the DBM allocator Precondition: DBMs of arg are of dimension fed->dim fed!=NULL factory->maxDim>=fed->dim

BOOL dbmf_satisfies (  const DBMFederation_t  fed, cindex_t  i, cindex_t  j, raw_t  constraint )

Check if a federation satisfies a constraint. Parameters: fed,:  federation i,j,constraint,:  constraint xi-xj to check Returns: TRUE if there is one DBM that satisfies the constraint, FALSE otherwise Precondition: i != j, i < fed->dim, j < fed->dim

void dbmf_shrinkExpand (  DBMFederation_t *  fed, const uint32_t *  bitSrc, const uint32_t *  bitDst, size_t  bitSize, cindex_t *  table, DBMAllocator_t *  factory )

Similarly, on federations. Parameters: fed,:  federation bitSrc,:  source bit array bitDst,:  destination bit array bitSize,:  size in int of the bit arrays table,:  indirection table to write factory,:  compatible factory Precondition: factory->dim >= fed->dim & factory->dim >= resulting dim factory->dim == max possible dim See also: dbm_shrinkExpand Postcondition: fed->dim updated table written as by dbm_shrinkExpand

void dbmf_stretchDown (  DBMFederation_t  fed, cindex_t  clock )

Stretch-down operation for approximation. Remove all lower bounds for a given clock. Parameters: fed,:  federation clock,:  clock to "down-free" Precondition: clock > 0, clock < fed->dim

void dbmf_stretchUp (  DBMFederation_t  fed  )

Stretch-up operation for approximation. Remove all upper bounds for all clocks. Parameters: fed,:  federation

int dbmf_substractDBM (  DBMFederation_t *  fed, const raw_t *  dbm, DBMAllocator_t *  factory )

Substraction operation: computes A = A - B. Parameters: fed,:  input federation to substract from (A) dbm,:  DBM to substract (B) factory,:  compatible factory Returns: A = A - B, 0 if allocation successful, -1 if out-of-memory and the federation is empty. Precondition: dbm is of dimension fed.dim factory->dim >= fed.dim

DBMList_t* dbmf_substractDBMFromDBM (  const raw_t *  dbm1, const raw_t *  dbm2, cindex_t  dim, BOOL *  valid, DBMAllocator_t *  factory )

Substraction operation: computes C = A - B. Parameters: dbm1,:  DBM to substract from (A) dbm2,:  DBM to substract (B) dim,:  dimension of the DBMs factory,:  compatible factory valid,:  pointer to validate memory allocation Returns: C as a list of DBMs (may be NULL if empty) Precondition: both DBMs have same dimension factory->dim >= dim valid != NULL Postcondition: the result (if != NULL) is allocated by the factory the resulting federation may be non disjoint if *valid == FALSE then memory went out and the result =NULL

DBMFederation_t dbmf_substractDBMFromFederation (  const DBMFederation_t  fed, const raw_t *  dbm, BOOL *  valid, DBMAllocator_t *  factory )

Substraction operation: computes C = A - B. Parameters: fed,:  input federation to substract from (A) dbm,:  DBM to substract (B) factory,:  compatible factory valid,:  pointer to validate memory allocation Returns: C Precondition: dbm is of dimension fed.dim factory->dim >= fed.dim valid != NULL Postcondition: the DBMList of the result (if != NULL) is allocated by the factory if *valid == FALSE then memory went out and result =NULL

int dbmf_substractFederation (  DBMFederation_t *  fed1, const DBMList_t *  fed2, DBMAllocator_t *  factory )

Substraction operation: computes A = A - B. Parameters: fed1,:  input federation to substract from (A) fed2,:  federation to substract (B) factory,:  compatible factory Returns: A = A - B (maybe NULL), 0 if allocation successful, -1 if out-of-memory and the federation is empty. Precondition: fed1->dim == dim of fed2 (if fed2 != NULL) factory->dim >= fed1->dim Postcondition: fed1 is deallocated if out-of-memory

DBMList_t* dbmf_substractFederationFromDBM (  const raw_t *  dbm, const DBMFederation_t  fed, BOOL *  valid, DBMAllocator_t *  factory )

Substraction operation: computes C = A - B. Parameters: dbm,:  input DBM to substract from (A) fed,:  federation to substract (B) factory,:  compatible factory valid,:  pointer to validate memory allocation Returns: C as a list of DBMs (may be NULL if empty) Precondition: dbm is of dimension fed.dim factory->dim >= fed.dim valid != NULL Postcondition: the result (if != NULL) is allocated by the factory if *valid == FALSE then memory went out and the result =NULL

DBMFederation_t dbmf_substractFederationFromFederation (  const DBMFederation_t  fed1, const DBMFederation_t  fed2, BOOL *  valid, DBMAllocator_t *  factory )

Substraction operation: computes C = A - B. Parameters: fed1,:  input federation to substract from (A) fed2,:  federation to substract (B) factory,:  compatible factory valid,:  pointer to validate memory allocation Returns: C Precondition: fed1.dim == fed2.dim factory->dim >= fed1.dim valid != NULL Postcondition: the DBMList of the result (if != NULL) is allocated by the factory if *valid == FALSE then memory went out and the result =NULL

BOOL dbmf_union (  DBMFederation_t *  fed, DBMList_t *  dbmList, DBMAllocator_t *  factory )

Union of a list of DBMs and a federation: add DBMs to the federation. fed += DBMs. Note: union means that inclusion check is done. Parameters: fed,:  federation dbmList,:  list of DBMs to add factory,:  compatible factory Returns: TRUE if one dbm was accepted, FALSE otherwise Precondition: all DBMs were allocated by factory DBMs are of dimension fed->dim factory->dim >= fed->dim dbmList is a list, ie, dbmList->next is initialized. Postcondition: DBMs in dbmList are deallocated or belong to fed.

BOOL dbmf_unionWithCopy (  DBMFederation_t *  fed, const DBMList_t *  dbmList, DBMAllocator_t *  factory, BOOL *  valid )

Union of a list of DBMs and a federation: add DBMs to the federation. fed += DBMs. The argument is copied this time. Note: union means that inclusion check is done. It is possible to encode this function with other functions but useless intermediate copies may be produced. Parameters: fed,:  federation dbmList,:  list of DBMs to add factory,:  compatible factory valid,:  return flag for the allocation. Returns: TRUE if one dbm was accepted, FALSE otherwise Precondition: all DBMs were allocated by factory DBMs are of dimension fed->dim factory->dim >= fed->dim dbmList is a list, ie, dbmList->next is initialized. Postcondition: *valid = TRUE if the allocation succeeded, FALSE otherwise. If the allocation failed then fed has an incomplete result.

void dbmf_up (  DBMFederation_t  fed  )

Up/delay operation (strongest post-condition). Parameters: fed,:  federation.

void dbmf_update (  DBMFederation_t  fed, cindex_t  x, cindex_t  y, int32_t  value )

General update: x := x + value. Parameters: fed,:  federation x,:  clock to copy to y,:  clock to copy from value,:  value to increment Precondition: x > 0, y > 0, x < fed->dim, y < fed->dim if value < 0 then |value| <= min bound of y

void dbmf_updateClock (  DBMFederation_t  fed, cindex_t  x, cindex_t  y )

Copy a clock: x := y. Parameters: fed,:  federation x,:  clock to copy to y,:  clock to copy from Precondition: x > 0, y > 0, x < fed->dim, y < fed->dim

void dbmf_updateIncrement (  DBMFederation_t  fed, cindex_t  clock, int32_t  value )

Increment a clock: x += value. Parameters: fed,:  federation clock,:  clock to increment value,:  value to increment Precondition: clock > 0 && clock < fed->dim if value < 0 then |value| <= min bound of clock

void dbmf_updateValue (  DBMFederation_t  fed, cindex_t  clock, int32_t  value )

Update a clock value: x := value. Parameters: fed,:  federation clock,:  clock to update value,:  new value Precondition: clock > 0 & clock < fed->dim

static DBMList_t* dbmf_validCopyDBM2List (  const raw_t *  dbm, cindex_t  dim, BOOL *  valid, DBMAllocator_t *  factory )  [static]

Internal function: another way to copy and to use *valid instead of a null return code. Parameters: dbm,dim,:  DBM of dimension dim valid,:  pointer to validate the memory allocation factory,:  factory to allocate Precondition: factory->dim >= dim, valid && *valid == TRUE

BOOL simpleBad (  const raw_t *  good, const raw_t *  bad, cindex_t  dim, DBMList_t **  toSubtract, BOOL *  valid, DBMAllocator_t *  factory )

---

Variable Documentation

int allocatedhop

---