dbm.c File Reference

#include <stdio.h>
#include <stdlib.h>
#include "base/intutils.h"
#include "base/bitstring.h"
#include "base/doubles.h"
#include "debug/macros.h"
#include "dbm/dbm.h"
#include "dbm/print.h"
#include "dbm.h"

Defines
#define	DBM(I, J)   dbm[(I)*dim+(J)]
#define	SRC(I, J)   src[(I)*dim+(J)]
#define	DST(I, J)   dst[(I)*dim+(J)]
#define	DBM1(I, J)   dbm1[(I)*dim+(J)]
#define	DBM2(I, J)   dbm2[(I)*dim+(J)]
#define	ASSERT_DIAG_OK(DBM, DIM)   ASSERT(dbm_isDiagonalOK(DBM,DIM), dbm_print(stderr, DBM, DIM))
	For debugging.
#define	ASSERT_NOT_EMPTY(DBM, DIM)   ASSERT(!dbm_isEmpty(DBM, DIM), dbm_print(stderr, DBM, DIM))
#define	DBM_CONSTRAIN(I, J, V)
Functions
void	dbm_closeLU (raw_t *dbm, cindex_t dim, const int32_t *lower, const int32_t *upper)
	Specialized close for extrapolation: can skip outer loop k if lower[k] == upper[k] == infinity.
void	dbm_init (raw_t *dbm, cindex_t dim)
	Initialize a DBM with: <= 0 on the diagonal and the 1st row <= infinity elsewhere.
BOOL	dbm_isEqualToInit (const raw_t *dbm, cindex_t dim)
	Equality test with trivial dbm as obtained from dbm_init(dbm, dim).
void	dbm_convexUnion (raw_t *dst, const raw_t *src, cindex_t dim)
	Convex hull union between 2 DBMs.
BOOL	dbm_intersection (raw_t *dst, const raw_t *src, cindex_t dim)
	Intersection of 2 DBMs.
BOOL	dbm_relaxedIntersection (raw_t *dst, const raw_t *dbm1, const raw_t *dbm2, cindex_t dim)
	Relaxed intersection of 2 DBMs.
BOOL	dbm_haveIntersection (const raw_t *dbm1, const raw_t *dbm2, cindex_t dim)
	Test if 2 DBMs have an intersection.
BOOL	dbm_constrain (raw_t *dbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint, uint32_t *touched)
	Constrain a DBM with a constraint.
BOOL	dbm_constrain1 (raw_t *dbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint)
	Constrain a DBM with one constraint.
BOOL	dbm_constrainN (raw_t *dbm, cindex_t dim, const constraint_t *constraints, size_t n)
	Constrain a DBM with several constraints.
BOOL	dbm_constrainIndexedN (raw_t *dbm, cindex_t dim, const cindex_t *indexTable, const constraint_t *constraints, size_t n)
	Constrain a DBM with several constraints using a table for index translation (translates absolute clock indices to local clock indices for this DBM).
void	dbm_up (raw_t *dbm, cindex_t dim)
	Delay operation.
void	dbm_downFrom (raw_t *dbm, cindex_t dim, cindex_t j)
	Internal dbm_down, don't use directly.
void	dbm_updateValue (raw_t *dbm, cindex_t dim, cindex_t k, int32_t value)
	Former "reset" operation, properly called update.
void	dbm_freeClock (raw_t *dbm, cindex_t dim, cindex_t k)
	Free operation.
void	dbm_freeUp (raw_t *dbm, cindex_t dim, cindex_t k)
	Free all upper bounds for a given clock.
void	dbm_freeAllUp (raw_t *dbm, cindex_t dim)
	Free all upper bounds for all clocks.
BOOL	dbm_isFreedAllUp (const raw_t *dbm, cindex_t dim)
void	dbm_freeDown (raw_t *dbm, cindex_t dim, cindex_t k)
	Free all lower bounds for a given clock.
void	dbm_freeAllDown (raw_t *dbm, cindex_t dim)
	Free all lower bounds for all clocks.
uint32_t	dbm_testFreeAllDown (const raw_t *dbm, cindex_t dim)
void	dbm_updateClock (raw_t *dbm, cindex_t dim, cindex_t i, cindex_t j)
	Clock copy operation = update clock: xi := xj, where xi and xj are clocks.
void	dbm_updateIncrement (raw_t *dbm, cindex_t dim, cindex_t k, int32_t value)
	Increment operation: xi := xi + value, where xi is a clock.
void	dbm_update (raw_t *dbm, cindex_t dim, cindex_t i, cindex_t j, int32_t value)
	More general update operation: xi := xj + value, where xi and yi are clocks.
BOOL	dbm_constrainClock (raw_t *dbm, cindex_t dim, cindex_t clock, int32_t value)
BOOL	dbm_close (raw_t *dbm, cindex_t dim)
	Close operation.
BOOL	dbm_isClosed (const raw_t *dbm, cindex_t dim)
	Check that a DBM is closed.
BOOL	dbm_closex (raw_t *dbm, cindex_t dim, const uint32_t *touched)
	Close operation.
BOOL	dbm_close1 (raw_t *dbm, cindex_t dim, cindex_t k)
	Close operation for 1 clock.
void	dbm_closeij (raw_t *dbm, cindex_t dim, cindex_t b, cindex_t a)
	Specialization of close valid if only one constraint cij is tightened, ie, DBM is closed, you tighten DBM[i,j] only, then this function recomputes the closure more efficiently than calling close1(i) and close1(j).
BOOL	dbm_isEmpty (const raw_t *dbm, cindex_t dim)
	Check if a DBM is empty by looking at its diagonal.
BOOL	dbm_isUnbounded (const raw_t *dbm, cindex_t dim)
	Check if a DBM is unbounded, i.e.
relation_t	dbm_relation (const raw_t *dbm1, const raw_t *dbm2, cindex_t dim)
	Relation between 2 dbms.
BOOL	dbm_isSubsetEq (const raw_t *dbm1, const raw_t *dbm2, cindex_t dim)
	Test only if dbm1 <= dbm2.
void	dbm_relaxAll (raw_t *dbm, cindex_t dim)
	Relax all bounds so that they are non strict (except for infinity).
void	dbm_relaxDownClock (raw_t *dbm, cindex_t dim, cindex_t clock)
	Relax lower bounds of a given clocks, ie, make them weak.
void	dbm_relaxUpClock (raw_t *dbm, cindex_t dim, cindex_t clock)
	Relax upper bounds of a given clocks, ie, make them weak.
BOOL	dbm_isPointIncluded (const int32_t *pt, const raw_t *dbm, cindex_t dim)
	Test if a (discrete) point is included in the zone represented by the DBM.
BOOL	dbm_isRealPointIncluded (const double *pt, const raw_t *dbm, cindex_t dim)
	Test if a (real) point is included in the zone represented by the DBM.
cindex_t	dbm_computeTables (const uint32_t *bitSrc, const uint32_t *bitDst, size_t bitSize, cindex_t *table, cindex_t *cols)
	Internal function: compute redirection tables table and cols (for update of DBM).
void	dbm_updateDBM (raw_t *dbmDst, const raw_t *dbmSrc, cindex_t dimDst, cindex_t dimSrc, const cindex_t *cols)
	Internal function: update a DBM (copy & and insert new rows).
cindex_t	dbm_shrinkExpand (const raw_t *dbmSrc, raw_t *dbmDst, cindex_t dimSrc, const uint32_t *bitSrc, const uint32_t *bitDst, size_t bitSize, cindex_t *table)
	Shrink and expand a DBM: takes 2 bit arrays: the source array marks which clocks are used in the source DBM, and the destination array marks the clocks in the destination DBM removes clock constraints in source and not in destination adds clock constraints not in source and in destination leaves clock constraints that are in source and in destination.
void	dbm_extrapolateMaxBounds (raw_t *dbm, cindex_t dim, const int32_t *max)
	Classical extrapolation based on maximal bounds, formerly called k-normalization.
void	dbm_diagonalExtrapolateMaxBounds (raw_t *dbm, cindex_t dim, const int32_t *max)
	Diagonal extrapolation based on maximal bounds.
void	dbm_extrapolateLUBounds (raw_t *dbm, cindex_t dim, const int32_t *lower, const int32_t *upper)
	Extrapolation based on lower-upper bounds.
void	dbm_diagonalExtrapolateLUBounds (raw_t *dbm, cindex_t dim, const int32_t *lower, const int32_t *upper)
	Diagonal extrapolation based on lower-upper bounds.
void	dbm_swapClocks (raw_t *dbm, cindex_t dim, cindex_t x, cindex_t y)
	Swap clocks.
BOOL	dbm_isDiagonalOK (const raw_t *dbm, cindex_t dim)
	Test if the diagonal is correct.
BOOL	dbm_isValid (const raw_t *dbm, cindex_t dim)
	Test if dbm is closed dbm is not empty constraints in the 1st row are at most <=0.
const char *	dbm_relation2string (relation_t rel)
	Convert code to string.
raw_t	dbm_getMaxRange (const raw_t *dbm, cindex_t dim)
	Go through a DBM (dim*dim) and compute the max range needed to store the constraints, excluding infinity.

---

Define Documentation

#define ASSERT_DIAG_OK (  DBM, DIM   )     ASSERT(dbm_isDiagonalOK(DBM,DIM), dbm_print(stderr, DBM, DIM))

For debugging.

#define ASSERT_NOT_EMPTY (  DBM, DIM   )     ASSERT(!dbm_isEmpty(DBM, DIM), dbm_print(stderr, DBM, DIM))

#define DBM (  I, J   )     dbm[(I)*dim+(J)]

#define DBM1 (  I, J   )     dbm1[(I)*dim+(J)]

#define DBM2 (  I, J   )     dbm2[(I)*dim+(J)]

#define DBM_CONSTRAIN (  I, J, V   )

Value: cindex_t i = I; \ cindex_t j = J; \ raw_t v = V; \ assert(i < dim && j < dim && i != j); \ if (DBM(i,j) > v) \ { \ DBM(i,j) = v; \ if (dbm_negRaw(v) >= DBM(j,i)) \ { \ DBM(0,0) = -1; /* mark empty */\ return FALSE; \ } \ ++changed; \ base_setOneBit(touched, ci = i); \ base_setOneBit(touched, cj = j); \ }

#define DST (  I, J   )     dst[(I)*dim+(J)]

#define SRC (  I, J   )     src[(I)*dim+(J)]

---

Function Documentation

BOOL dbm_close (  raw_t *  dbm, cindex_t  dim )

Close operation. Complexity cubic in dim. Algorithm: for all k < dim do for all i < dim do for all j < dim do if dbm[i,j] > dbm[i,k]+dbm[k,j] dbm[i,j] = dbm[i,k]+dbm[k,j]

BOOL dbm_close1 (  raw_t *  dbm, cindex_t  dim, cindex_t  k )

Close operation for 1 clock. Complexity quadratic in dim * # of clocks to iterate on. Algorithm: for one k < dim do for all i < dim do for all j < dim do if dbm[i,j] > dbm[i,k]+dbm[k,j] dbm[i,j] = dbm[i,k]+dbm[k,j]

void dbm_closeij (  raw_t *  dbm, cindex_t  dim, cindex_t  i, cindex_t  j )

Specialization of close valid if only one constraint cij is tightened, ie, DBM is closed, you tighten DBM[i,j] only, then this function recomputes the closure more efficiently than calling close1(i) and close1(j). Parameters: dbm,:  DBM dim,:  dimension i,j,:  the constraint that was tightened See also: Rokicki's thesis page 171. Precondition: dim > 1 induced by i!=j & i < dim & j < dim i != j, i < dim, j < dim DBM non empty: DBM[i,j] + DBM[j,i] >= 0, ie, the tightening still results in a non empty DBM. If we have < 0 then this close should not be called at all because we know the DBM is empty. Postcondition: DBM is not empty

void dbm_closeLU (  raw_t *  dbm, cindex_t  dim, const int32_t *  lower, const int32_t *  upper )

Specialized close for extrapolation: can skip outer loop k if lower[k] == upper[k] == infinity.

BOOL dbm_closex (  raw_t *  dbm, cindex_t  dim, const uint32_t *  touched )

Close operation. Complexity quadratic in dim * # of clocks to iterate on. Algorithm: for all k < dim s.t. clock k is touched do for all i < dim do for all j < dim do if dbm[i,j] > dbm[i,k]+dbm[k,j] dbm[i,j] = dbm[i,k]+dbm[k,j]

cindex_t dbm_computeTables (  const uint32_t *  bitSrc, const uint32_t *  bitDst, size_t  bitSize, cindex_t *  table, cindex_t *  cols )

Internal function: compute redirection tables table and cols (for update of DBM). See also: dbm_shrinkExpand for table cols redirects indices from the source DBM to the destination DBM for copy purposes: copy row i to destination[i] from source[cols[i]] Parameters: bitSrc,:  source array bits bitDst,:  destination array bits bitSize,:  size of the arrays table,cols,:  tables to compute Returns: dimension of the new DBM

BOOL dbm_constrain (  raw_t *  dbm, cindex_t  dim, cindex_t  i, cindex_t  j, raw_t  constraint, uint32_t *  touched )

Constrain a DBM with a constraint. USAGE: dbm must be closed. reset touched: base_resetBits(touched, size) apply constraints: dbm_constrain(...) if not empty dbm_close(dbm, dim, touched) Parameters: dbm,:  DBM. dim,:  dimension. i,j,constraint,:  the clock constraint xi-xj <= constraint (or < constraint) according to the clock constraint encoding. touched,:  bit table to keep track of modified clocks. Returns: : FALSE if the DBM is empty, TRUE otherwise, the constrained DBM, and which clocks were modified (touched). It is not guaranteed that the DBM is non empty, but if FALSE is returned then the DBM is guaranteed to be empty. Precondition: touched is at least a uint32_t[bits2intsize(dim)] constraint is finite dim > 1 induced by i < dim & j < dim & i != j i < dim, j < dim, i != j Postcondition: THE RESULTING DBM MAY NOT BE CLOSED, calls to isEmpty can return erroneous results.

BOOL dbm_constrain1 (  raw_t *  dbm, cindex_t  dim, cindex_t  i, cindex_t  j, raw_t  constraint )

Constrain a DBM with one constraint. If you have several constraints, it may be better to use the previous functions. Parameters: dbm,:  DBM, ASSUME: closed. dim,:  dimension. i,j,constraint,:  constraint for xi-xj to use Precondition: DBM is closed and non empty dim > 1 induced by i < dim & j < dim & i != j as a consequence: i>=0 & j>=0 & i!=j => (i or j) > 0 and dim > (i or j) > 0 => dim > 1 i < dim, j < dim, i != j Returns: TRUE if the DBM is non empty and the constrained DBM. Postcondition: the resulting DBM is closed if it is non empty.

BOOL dbm_constrainClock (  raw_t *  dbm, cindex_t  dim, cindex_t  clock, int32_t  value )

Returns: constraint clock to == value, and return if the result is non empty. Parameters: dbm,dim,:  DBM of dimension dim clock,:  clock index for the reset value,:  reset value to apply Precondition: clock != 0 (not ref clock) && clock < dim

BOOL dbm_constrainIndexedN (  raw_t *  dbm, cindex_t  dim, const cindex_t *  indexTable, const constraint_t *  constraints, size_t  n )

Constrain a DBM with several constraints using a table for index translation (translates absolute clock indices to local clock indices for this DBM). USAGE: Parameters: dbm,:  DBM dim,:  dimension. indexTable,:  table for index translation constraints,n,:  the n constraints to use. Precondition: DBM closed and non empty. valid constraint: not of the form xi-xi <= something dim > 1 induced by i < dim & j < dim & i != j constraints[*].{i,j} < dim Returns: TRUE if the DBM is non empty, the constrained DBM Postcondition: the resulting DBM is closed if it is non empty.

BOOL dbm_constrainN (  raw_t *  dbm, cindex_t  dim, const constraint_t *  constraints, size_t  n )

Constrain a DBM with several constraints. USAGE: Parameters: dbm,:  DBM dim,:  dimension. constraints,n,:  the n constraints to use. Precondition: DBM closed and non empty. valid constraint: not of the form xi-xi <= something dim > 1 induced by i < dim & j < dim & i != j constraints[*].{i,j} < dim Returns: TRUE if the DBM is non empty, the constrained DBM Postcondition: the resulting DBM is closed if it is non empty.

void dbm_convexUnion (  raw_t *  dbm1, const raw_t *  dbm2, cindex_t  dim )

Convex hull union between 2 DBMs. Parameters: dbm1,dbm2,:  DBMs. dim,:  dimension Precondition: both DBMs have the same dimension both DBMs are closed and non empty Returns: dbm1 = dbm1 U dbm2 Postcondition: dbm1 is closed.

void dbm_diagonalExtrapolateLUBounds (  raw_t *  dbm, cindex_t  dim, const int32_t *  lower, const int32_t *  upper )

Diagonal extrapolation based on lower-upper bounds. Most general approximation. Update dbm[i,j] with infinity if dbm[i,j] > lower_xi infinity if dbm[0,i] < -lower_xi infinity if dbm[0,j] < -upper_xj for i != 0 <-upper_xj if dbm[0,j] < -upper_xj for i = 0 dbm[i,j] otherwise Parameters: dbm,:  DBM. dim,:  dimension. lower,:  lower bounds. upper,:  upper bounds. Precondition: DBM is closed and non empty lower and upper are int32_t[dim] lower[0] = upper[0] = 0 (reference clock) Postcondition: DBM is closed.

void dbm_diagonalExtrapolateMaxBounds (  raw_t *  dbm, cindex_t  dim, const int32_t *  max )

Diagonal extrapolation based on maximal bounds. Update dbm[i,j] with infinity if dbm[i,j] > max_xi infinity if dbm[0,i] < -max_xi infinity if dbm[0,j] < -max_xj, i != 0 <-max_xj if dbm[i,j] < -max_xj, i == 0 dbm[i,j] otherwise Parameters: dbm,:  DBM. dim,:  dimension. max,:  table of maximal constants. Precondition: DBM is closed and non empty max is a int32_t[dim] max[0] = 0 (reference clock) Postcondition: DBM is closed.

void dbm_downFrom (  raw_t *  dbm, cindex_t  dim, cindex_t  j )

Internal dbm_down, don't use directly.

void dbm_extrapolateLUBounds (  raw_t *  dbm, cindex_t  dim, const int32_t *  lower, const int32_t *  upper )

Extrapolation based on lower-upper bounds. if dbm[i,j] > lower_xi then dbm[i,j] = infinity if dbm[i,j] < -upper_xj then dbm[i,j] = < -upper_xj Parameters: dbm,:  DBM. dim,:  dimension. lower,:  lower bounds. upper,:  upper bounds. Precondition: DBM is closed lower and upper are int32_t[dim] lower[0] = upper[0] = 0 (reference clock) Postcondition: DBM is closed.

void dbm_extrapolateMaxBounds (  raw_t *  dbm, cindex_t  dim, const int32_t *  max )

Classical extrapolation based on maximal bounds, formerly called k-normalization. Extrapolate the zone using maximal constants: if dbm[i,j] > max_xi then set it to infinity if dbm[i,j] < -max_xj then set it to < -max_xj otherwise don't touch dbm[i,j] Parameters: dbm,:  DBM. dim,:  dimension. max,:  table of maximal constants to use for the clocks. Precondition: DBM is closed and non empty max is a int32_t[dim] max[0] = 0 (reference clock) Postcondition: DBM is closed

void dbm_freeAllDown (  raw_t *  dbm, cindex_t  dim )

Free all lower bounds for all clocks. Parameters: dbm,:  DBM. dim,:  dimension. Precondition: DBM closed and non empty. Postcondition: DBM closed and non empty.

void dbm_freeAllUp (  raw_t *  dbm, cindex_t  dim )

Free all upper bounds for all clocks. Parameters: dbm,:  DBM. dim,:  dimension. Precondition: DBM closed and non empty. Postcondition: DBM closed and non empty.

void dbm_freeClock (  raw_t *  dbm, cindex_t  dim, cindex_t  index )

Free operation. Remove all constraints (lower and upper bounds) for a given clock, i.e., set them to infinity, except for x0-xk <= 0. Parameters: dbm,:  DBM. dim,:  dimension. index,:  the clock to free. Precondition: DBM is closed and non empty dim > 1 induced by index > 0 && index < dim index > 0, index < dim Postcondition: DBM is closed.

void dbm_freeDown (  raw_t *  dbm, cindex_t  dim, cindex_t  index )

Free all lower bounds for a given clock. Parameters: dbm,:  DBM. dim,:  dimension. index,:  index of the clock to "down-free" Precondition: dim > 1 induced by index > 0 && index < dim index > 0, index < dim DBM closed and non empty Postcondition: DBM is closed and non empty.

void dbm_freeUp (  raw_t *  dbm, cindex_t  dim, cindex_t  index )

Free all upper bounds for a given clock. Parameters: dbm,:  DBM. dim,:  dimension. index,:  the concerned clock. Precondition: DBM closed and non empty and 0 < index < dim Postcondition: DBM is closed and non empty.

raw_t dbm_getMaxRange (  const raw_t *  dbm, cindex_t  dim )

Go through a DBM (dim*dim) and compute the max range needed to store the constraints, excluding infinity. Parameters: dbm,:  DBM. dim,:  dimension. Returns: max range, positive value.

BOOL dbm_haveIntersection (  const raw_t *  dbm1, const raw_t *  dbm2, cindex_t  dim )

Test if 2 DBMs have an intersection. Parameters: dbm1,dbm2,:  DBMs to test. dim,:  dimension of both DBMs. Returns: FALSE if dbm1 intersection dbm2 is empty and TRUE if it *may* be non empty (not guaranteed).

void dbm_init (  raw_t *  dbm, cindex_t  dim )

Initialize a DBM with: <= 0 on the diagonal and the 1st row <= infinity elsewhere. Parameters: dbm,:  DBM to initialize. dim,:  dimension. Returns: initialized DBM. Postcondition: DBM is closed.

BOOL dbm_intersection (  raw_t *  dbm1, const raw_t *  dbm2, cindex_t  dim )

Intersection of 2 DBMs. Parameters: dbm1,dbm2,:  DBMs. dim,:  dimension. Precondition: both DBMs have the same dimension both DBMs are closed and non empty Returns: dbm1 = dbm1 intersected with dbm2 and TRUE if dbm1 is non empty. Postcondition: dbm1 is closed and non empty OR dbm1 is empty.

BOOL dbm_isClosed (  const raw_t *  dbm, cindex_t  dim )

Check that a DBM is closed. Complexity cubic in dim. Algorithm: for all k < dim do for all i < dim do for all j < dim do if dbm[i,j] > dbm[i,k]+dbm[k,j] needs update -> return false

BOOL dbm_isDiagonalOK (  const raw_t *  dbm, cindex_t  dim )

Test if the diagonal is correct. Constraints on the diagonal should be <0 if the DBM is empty or <=0 for non empty DBMs. Positive constraints are allowed in principle but such DBMs are not canonical. Parameters: dbm,:  DBM. dim,:  dimension. Returns: TRUE if the diagonal <=0.

BOOL dbm_isEmpty (  const raw_t *  dbm, cindex_t  dim )

Check if a DBM is empty by looking at its diagonal. There should be only == 0 constraints. NOTE: one should never need to call this function manually, unless for debugging. Parameters: dbm,:  DBM. dim,:  dimension. Precondition: the close function was run before on the dbm Returns: : TRUE if empty, FALSE otherwise.

BOOL dbm_isEqualToInit (  const raw_t *  dbm, cindex_t  dim )

Equality test with trivial dbm as obtained from dbm_init(dbm, dim). Parameters: dbm,:  DBM to test dim,:  dimension.

BOOL dbm_isFreedAllUp (  const raw_t *  dbm, cindex_t  dim )

Returns: true if dbm_freeAllUp(dbm,dim) has no effect on dbm. Parameters: dbm,dim,:  DBM of dimension dim to test.

BOOL dbm_isPointIncluded (  const int32_t *  pt, const raw_t *  dbm, cindex_t  dim )

Test if a (discrete) point is included in the zone represented by the DBM. Parameters: pt,:  the point dbm,:  DBM dim,:  dimension Precondition: pt is a int32_t[dim] dbm is a raw_t[dim*dim] dbm is closed Returns: TRUE if the pt satisfies the constraints of dbm

BOOL dbm_isRealPointIncluded (  const double *  pt, const raw_t *  dbm, cindex_t  dim )

Test if a (real) point is included in the zone represented by the DBM. Parameters: pt,:  the point dbm,:  DBM dim,:  dimension Precondition: pt is a int32_t[dim] dbm is a raw_t[dim*dim] dbm is closed Returns: TRUE if the pt satisfies the constraints of dbm

BOOL dbm_isSubsetEq (  const raw_t *  dbm1, const raw_t *  dbm2, cindex_t  dim )

Test only if dbm1 <= dbm2. Parameters: dbm1,dbm2,:  DBMs to be tested. dim,:  dimension of the DBMs. Precondition: dbm1 and dbm2 have the same dimension dbm_isValid for both DBMs Returns: TRUE if dbm1 <= dbm2, FALSE otherwise.

BOOL dbm_isUnbounded (  const raw_t *  dbm, cindex_t  dim )

Check if a DBM is unbounded, i.e. , if one point can delay infinitely. Parameters: dbm,:  DBM. dim,:  dimension. Returns: TRUE if unbounded, FALSE otherwise. Precondition: dbm_isValid(dbm, dim)

BOOL dbm_isValid (  const raw_t *  dbm, cindex_t  dim )

Test if dbm is closed dbm is not empty constraints in the 1st row are at most <=0.

relation_t dbm_relation (  const raw_t *  dbm1, const raw_t *  dbm2, cindex_t  dim )

Relation between 2 dbms. See relation_t. Parameters: dbm1,dbm2,:  DBMs to be tested. dim,:  dimension of the DBMS. Precondition: dbm1 and dbm2 have the same dimension dbm_isValid for both DBMs Returns: : exact relation result, See also: relation_t.

const char* dbm_relation2string (  relation_t  rel  )

Convert code to string. Parameters: rel,:  relation result to translate. Returns: string to print. DO NOT deallocate or touch the result string.

void dbm_relaxAll (  raw_t *  dbm, cindex_t  dim )

Relax all bounds so that they are non strict (except for infinity). Parameters: dbm,dim,:  DBM of dimension dim. Precondition: dbm_isValid(dbm, dim) Postcondition: dbm_isValid(dbm, dim)

void dbm_relaxDownClock (  raw_t *  dbm, cindex_t  dim, cindex_t  clock )

Relax lower bounds of a given clocks, ie, make them weak. Parameters: dbm,dim,:  DBM of dimension dim clock,:  clock to relax. Precondition: (dim > 0 induced by) clock >= 0 && clock < dim && dbm_isValid(dbm,dim) Postcondition: DBM is closed and non empty

BOOL dbm_relaxedIntersection (  raw_t *  dst, const raw_t *  dbm1, const raw_t *  dbm2, cindex_t  dim )

Relaxed intersection of 2 DBMs. Parameters: dbm1,dbm2,:  DBMs. dim,:  dimension. Precondition: both DBMs have the same dimension both DBMs are closed and non empty dim > 0 Returns: dst = relaxed(dbm1) intersected with relaxed(dbm2) and TRUE if dst is non empty. Postcondition: dst is closed and non empty OR dst is empty.

void dbm_relaxUpClock (  raw_t *  dbm, cindex_t  dim, cindex_t  clock )

Relax upper bounds of a given clocks, ie, make them weak. Parameters: dbm,dim,:  DBM of dimension dim clock,:  clock to relax. Precondition: (dim > 0 induced by) clock >= 0 && clock < dim && dbm_isValid(dbm,dim) Postcondition: DBM is closed and non empty

cindex_t dbm_shrinkExpand (  const raw_t *  dbmSrc, raw_t *  dbmDst, cindex_t  dimSrc, const uint32_t *  bitSrc, const uint32_t *  bitDst, size_t  bitSize, cindex_t *  table )

Shrink and expand a DBM: takes 2 bit arrays: the source array marks which clocks are used in the source DBM, and the destination array marks the clocks in the destination DBM removes clock constraints in source and not in destination adds clock constraints not in source and in destination leaves clock constraints that are in source and in destination. Parameters: dbmSrc,:  source DBM dimSrc,:  dimension of dbmSrc dbmDst,:  destination DBM bitSrc,:  source bit array bitDst,:  destination bit array bitSize,:  size in int of the bit arrays bitSrc and bitDst table,:  where to write the indirection table for the destination DBM, dbmDst. If bit i is set in the bitDst, then table[i] gives the index used in the dbmDst. Returns: dimDst = dimension of dbmDst. Precondition: let maxDim = bitSize * 32: dbmDst is at least a raw_t[resultDim*resultDim] where resultDim = base_countBitsN(bitDst, bitSize) dimSrc = number of bits set in bitSrc bitSrc and bitDst are uint32_t[bitSize] table is at least a uint32_t[maxDim] bitSize <= bits2intsize(maxDim) dimSrc > 0 first bit in bitSrc is set first bit in bitDst is set bitSrc and bitDst are different (contents): the function is supposed to be called only if there is work to do dbmSrc != dbmDst (pointers): we do not modify the source DBM bitSize > 0 because at least ref clock Postcondition: dimDst (returned) == number of bits in bitDst for all bits set in bitDst at positions i, then table[i] is defined and gives the proper indirection ; for other bits, table[i] is untouched.

void dbm_swapClocks (  raw_t *  dbm, cindex_t  dim, cindex_t  x, cindex_t  y )

Swap clocks. Parameters: dbm,dim,:  DBM of dimension dim. x,y,:  clocks to swap.

uint32_t dbm_testFreeAllDown (  const raw_t *  dbm, cindex_t  dim )

Returns: 0 if dbm_freeAllDown(dbm,dim) has no effect on dbm, or (j << 16)|i otherwise where i and j are the indices from where dbm differs from its expected result. Parameters: dbm,dim,:  DBM of dimension dim to test.

void dbm_up (  raw_t *  dbm, cindex_t  dim )

Delay operation. Remove constraints of the form xi-x0 <= ci and replace them by xi-x0 < infinity. It is also called strongest post-condition. Parameters: dbm,:  DBM. dim,:  dimension. Precondition: DBM closed and non empty Postcondition: DBM is closed.

void dbm_update (  raw_t *  dbm, cindex_t  dim, cindex_t  i, cindex_t  j, int32_t  value )

More general update operation: xi := xj + value, where xi and yi are clocks. WARNING: if offset is negative it may be incorrect to use this. Parameters: dbm,:  DBM. dim,:  dimension. i,j,:  indices of the clocks. value,:  the increment. Precondition: DBM is closed and non empty. dim > 1 induced by i > 0 && i < dim i > 0, j > 0, j < dim, i < dim if value < 0 then |value| <= min bound of clock j Postcondition: DBM is closed.

void dbm_updateClock (  raw_t *  dbm, cindex_t  dim, cindex_t  i, cindex_t  j )

Clock copy operation = update clock: xi := xj, where xi and xj are clocks. Parameters: dbm,:  DBM. dim,:  dimension. i,j,:  indices of the clocks. Precondition: DBM closed and non empty. dim > 1 induced by i > 0 & i < dim i > 0, j > 0, i < dim, j < dim Postcondition: DBM is closed.

void dbm_updateDBM (  raw_t *  dbmDst, const raw_t *  dbmSrc, cindex_t  dimDst, cindex_t  dimSrc, const cindex_t *  cols )

Internal function: update a DBM (copy & and insert new rows). Parameters: dbmDst,dimDst,:  destination DBM of dimension dimDst dbmSrc,dimSrc,:  source DBM of dimension dimSrc cols,:  indirection table to copy the DBM, ie, rows (and columns) i of the destination come from cols[i] in the source if ~cols[i] (ie != ~0). Precondition: cols is a cindex_t[dimDst], cols[0] is ignored since the ref clock is always at 0, and for all i < dimDst: cols[i] < dimSrc.

void dbm_updateIncrement (  raw_t *  dbm, cindex_t  dim, cindex_t  i, int32_t  value )

Increment operation: xi := xi + value, where xi is a clock. WARNING: if offset is negative it may be incorrect to use this. Parameters: dbm,:  DBM. dim,:  dimension. i,:  index of the clock. value,:  the increment. Precondition: DBM closed and non empty. dim > 1 induced by i > 0 && i < dim i > 0, i < dim if value < 0, then |value| <= min bound of clock i Postcondition: DBM is closed.

void dbm_updateValue (  raw_t *  dbm, cindex_t  dim, cindex_t  index, int32_t  value )

Former "reset" operation, properly called update. Implement the operation x := v, where x is a clock and v a positive integer. Parameters: dbm,:  DBM dim,:  dimension. index,:  clock index. value,:  value to reset to (may be non null), must be >=0.. Precondition: DBM closed and non empty dim > 1 induced by index > 0 and index < dim index > 0: never reset reference clock, index < dim value is finite and not an encoded clock constraint value >= 0 (int used for type convenience and compatibility). Postcondition: DBM is closed.

---