Main Page | Namespace List | Class Hierarchy | Alphabetical List | Class List | Directories | File List | Namespace Members | Class Members | File Members
include / dbm

dbmfederation.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include "dbm/dbm.h"
#include "debug/monitor.h"
#include <iostream>

Go to the source code of this file.

Defines

#define SIZEOF_DBMLIST(DIM)   (sizeof(DBMList_t) + (DIM)*(DIM)*sizeof(raw_t))
#define dbmf_CHECKDIM(FACTORY, DIM)
 Assertion to check that requested DBMs have their dim <= max dim of the factory.
#define dbmf_checkFactory(F)   assert(dbmf_internCheckFactory(F))
 Check a factory -- for debugging.
#define dbmf_allocate(F)   dbmf_internAllocate(F)
#define dbmf_deallocate(F, D)   dbmf_internDeallocate(F,D)
#define dbmf_deallocateList(F, L)   dbmf_internDeallocateList(F,L)
#define APPLY_TO_FEDERATION(FED, OPERATION)
 Apply the same operation to all DBMs of a federation.

Typedefs

typedef dbmlist_s DBMList_t
 DBM Federation type: such federations have one dimension and several DBMs of the same dimension.

Functions

static void dbmf_initFactory (DBMAllocator_t *factory, cindex_t dim)
 Initialize a factory.
BOOL dbmf_internCheckFactory (const DBMAllocator_t *factory)
DBMList_t * dbmf_internAllocate (DBMAllocator_t *factory)
 Allocate DBMs with the factory.
static void dbmf_internDeallocate (DBMAllocator_t *factory, DBMList_t *dbm)
 Give back ONE DBM to its factory.
void dbmf_internDeallocateList (DBMAllocator_t *factory, DBMList_t *dbmList)
 Give back a LIST of DBMs to its factory.
static void dbmf_deallocateFederation (DBMAllocator_t *factory, DBMFederation_t *fed)
 Same as deallocateList but for a federation.
void dbmf_clearFactory (DBMAllocator_t *factory)
 Clear a factory.
static void dbmf_initFederation (DBMFederation_t *fed, cindex_t dim)
 Initialize a federation.
static void dbmf_addDBM (DBMList_t *dbm, DBMFederation_t *fed)
 Add a DBM in the federation (at the beginning of the list).
void dbmf_cleanUp (DBMFederation_t *fed, DBMAllocator_t *factory)
 Clean up the federation from empty DBMs.
static void dbmf_appendList (DBMList_t *dbmList, DBMList_t *endList)
 Append a list to another.
BOOL dbmf_hasDBM (const DBMList_t *fed, const raw_t *dbm, cindex_t dim)
 Test if a federation has a particular DBM.
static BOOL dbmf_federationHasDBM (const DBMFederation_t fed, const raw_t *dbm)
 Wrapper for DBMFederation_t.
size_t dbmf_getSize (const DBMList_t *dbmList)
 Size of a federation.
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.
DBMList_t * dbmf_copyDBMList (const DBMList_t *dbmList, cindex_t dim, BOOL *valid, DBMAllocator_t *factory)
 Copy a list of DBMs.
static DBMFederation_t dbmf_copyFederation (const DBMFederation_t fed, BOOL *valid, DBMAllocator_t *factory)
 Similar to dbmf_copyDBMList: wrapper for federations.
static int dbmf_addCopy (DBMFederation_t *fed, const DBMList_t *dbmList, DBMAllocator_t *factory)
 Copy a list of DBMs and append the result to a federation.
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.
static void dbmf_convexUnionWithFederation (raw_t *dbm, const DBMFederation_t fed)
 Computes the convex hull union between one DBM and a federation: dbm = dbm + federation.
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.
static BOOL dbmf_federationHasIntersection (const DBMFederation_t fed, const raw_t *dbm)
 Test if a federation and a DBM have an intersection.
static BOOL dbmf_federationsHaveIntersection (const DBMFederation_t fed1, const DBMFederation_t fed2)
 Test if 2 federations 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.
static BOOL dbmf_isEmpty (const DBMFederation_t fed)
 Test for emptiness.
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.
relation_t dbmf_relation (const raw_t *dbm, const DBMFederation_t fed, BOOL *valid, DBMAllocator_t *factory)
 Relation between one DBM and a federation.
BOOL dbmf_removePartialIncluded (DBMFederation_t *fed, const DBMList_t *arg, DBMAllocator_t *factory)
 Remove DBMs of fed that are (partially) included in arg.
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.
static BOOL dbmf_isReallyIncludedIn (const raw_t *dbm, const DBMFederation_t fed, BOOL *valid, DBMAllocator_t *factory)
 Test if a DBM is really included in a federation semantically.
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.
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.
DBMList_t * dbmf_substractFederationFromDBM (const raw_t *dbm, const DBMFederation_t fed, BOOL *valid, DBMAllocator_t *factory)
 Substraction operation: computes C = A - B.
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.
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 *fed2, DBMAllocator_t *factory)
 Substraction operation: computes A = A - B.
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.
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.
void dbm_printFederation (FILE *out, const DBMList_t *dbmList, cindex_t dim)
 Pretty print of a federation.
std::ostream & dbm_cppPrintFederation (std::ostream &out, const DBMList_t *dbmList, cindex_t dim)
 Pretty print of a DBM federation.

Define Documentation

#define APPLY_TO_FEDERATION (  FED,
OPERATION   ) 
 

Value:

do {                                        \
    DBMList_t *_first = (FED).dbmList;      \
    while(_first)                           \
    {                                       \
        OPERATION;                          \
        _first = _first->next;              \
    }                                       \
} while(0)
Apply the same operation to all DBMs of a federation.

#define dbmf_allocate (  F   )     dbmf_internAllocate(F)
 

#define dbmf_CHECKDIM (  FACTORY,
DIM   ) 
 

Value:

assert((FACTORY) && (FACTORY)->sizeOfAlloc >= SIZEOF_DBMLIST(DIM) && \
       (DIM) <= (FACTORY)->maxDim && SIZEOF_DBMLIST((FACTORY)->maxDim) == (FACTORY)->sizeOfAlloc)
Assertion to check that requested DBMs have their dim <= max dim of the factory.

#define dbmf_checkFactory (  F   )     assert(dbmf_internCheckFactory(F))
 

Check a factory -- for debugging.

May detect memory corruption.

Parameters:
factory,: allocator to check.

#define dbmf_deallocate (  F,
D   )     dbmf_internDeallocate(F,D)
 

#define dbmf_deallocateList (  F,
L   )     dbmf_internDeallocateList(F,L)
 

#define SIZEOF_DBMLIST (  DIM   )     (sizeof(DBMList_t) + (DIM)*(DIM)*sizeof(raw_t))
 

Typedef Documentation

typedef struct dbmlist_s DBMList_t
 

DBM Federation type: such federations have one dimension and several DBMs of the same dimension.

This is the list of DBMs for the federation.

Function Documentation

std::ostream& dbm_cppPrintFederation (  std::ostream &  out,
const DBMList_t *  dbmList,
cindex_t  dim
) 
 

Pretty print of a DBM federation.

Parameters:
dbmList,: list of DBMs to print.
dim,: dimension of all the DBMs.
out,: output stream.

void dbm_printFederation (  FILE *  out,
const DBMList_t *  dbmList,
cindex_t  dim
) 
 

Pretty print of a federation.

Parameters:
dbmList,: list of DBMs.
dim,: dimension of all the DBMs.
out,: output stream.

static int dbmf_addCopy (  DBMFederation_t *  fed,
const DBMList_t *  dbmList,
DBMAllocator_t *  factory
)  [inline, static]
 

Copy a list of DBMs and append the result to a federation.

Parameters:
fed,: federation that collects the copy.
dbmList,: the list of DBMs to copy.
factory,: DBM allocator.
Precondition:
factory->dim >= fed->dim, valid!=NULL, all DBMS of dbmList are of dimension fed->dim.
Returns:
-1 if out-of-memory, 0 otherwise.

static void dbmf_addDBM (  DBMList_t *  dbm,
DBMFederation_t *  fed
)  [inline, static]
 

Add a DBM in the federation (at the beginning of the list).

Parameters:
dbm,: dbm to add
fed,: federation
Precondition:
dbm->next is NULL or invalid: if there is a linked list then it is lost.

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

static void dbmf_appendList (  DBMList_t *  dbmList,
DBMList_t *  endList
)  [inline, static]
 

Append a list to another.

Parameters:
dbmList,: list argument
endList,: list to append at the tail of dbmList
Precondition:
dbmList != NULL

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

static void dbmf_convexUnionWithFederation (  raw_t *  dbm,
const DBMFederation_t  fed
)  [inline, static]
 

Computes the convex hull union between one DBM and a federation: dbm = dbm + federation.

Parameters:
dbm,: DBM
fed,: federation
Precondition:
  • dbm is of dimension fed->dim

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.

static DBMFederation_t dbmf_copyFederation (  const DBMFederation_t  fed,
BOOL *  valid,
DBMAllocator_t *  factory
)  [inline, static]
 

Similar to dbmf_copyDBMList: wrapper for federations.

Parameters:
fed,: original federation to copy.
factory,: allocator.
valid,: pointer for validation (memory allocation).
Precondition:
factory->maxDim >= fed.dim, valid!=NULL.

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.

static void dbmf_deallocateFederation (  DBMAllocator_t *  factory,
DBMFederation_t *  fed
)  [inline, static]
 

Same as deallocateList but for a federation.

Precondition:
federation not empty.
Parameters:
fed,: federation to deallocate.
factory,: allocator.

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)

static BOOL dbmf_federationHasDBM (  const DBMFederation_t  fed,
const raw_t *  dbm
)  [inline, static]
 

Wrapper for DBMFederation_t.

See also:
dbmf_hasDBM

static BOOL dbmf_federationHasIntersection (  const DBMFederation_t  fed,
const raw_t *  dbm
)  [inline, static]
 

Test if a federation and a DBM have an intersection.

Parameters:
fed,: federation.
dbm,: DBM to test.
Precondition:
dbm is of dimension fed->dim.
Returns:
TRUE if there is an intersection, FALSE otherwise.

static BOOL dbmf_federationsHaveIntersection (  const DBMFederation_t  fed1,
const DBMFederation_t  fed2
)  [inline, static]
 

Test if 2 federations have an intersection.

Parameters:
fed1,fed2,: federations to test.
Precondition:
the federations have the same dimension.

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.

static void dbmf_initFactory (  DBMAllocator_t *  factory,
cindex_t  dim
)  [inline, static]
 

Initialize a factory.

Parameters:
factory,: the factory to initialize.
dim,: maximal dimension of used DBMs.

static void dbmf_initFederation (  DBMFederation_t *  fed,
cindex_t  dim
)  [inline, static]
 

Initialize a federation.

Parameters:
fed,: federation
dim,: dimension of the DBMs
Precondition:
  • fed != NULL
  • dim > 0 (at least reference clock)
  • fed is a new uninitialized federation (the list of DBMs is reset)

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  ) 
 

static void dbmf_internDeallocate (  DBMAllocator_t *  factory,
DBMList_t *  dbm
)  [inline, static]
 

Give back ONE DBM to its factory.

Parameters:
factory,: factory (= owner)
dbm,: DBM to deallocate
Precondition:
dbm was obtained from dbmf_allocate(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)

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.

static BOOL dbmf_isEmpty (  const DBMFederation_t  fed  )  [inline, static]
 

Test for emptiness.

Parameters:
fed,: federation
Returns:
TRUE if federation is empty, FALSE 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

static BOOL dbmf_isReallyIncludedIn (  const raw_t *  dbm,
const DBMFederation_t  fed,
BOOL *  valid,
DBMAllocator_t *  factory
)  [inline, static]
 

Test if a DBM is really included in a federation semantically.

This is MORE EXPENSIVE than the dbmf_isIncludedIn function.

Parameters:
dbm,: dbm to test.
fed,: federation 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 dbm is included in a DBM of dbmList, 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

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

Generated on Fri Jun 30 00:02:46 2006 for Module dbm by  doxygen 1.4.2