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

mingraph.h File Reference

Support for minimum graph representation. More...

#include "base/c_allocator.h"
#include "base/intutils.h"
#include "dbm/dbm.h"

Go to the source code of this file.

Typedefs

typedef const int32_t * mingraph_t
 Style typedef: to make the difference clear between just allocated memory and the minimal graph representation.

Enumerations

enum  representationOfMinDBM_t {
  dbm_MINDBM_TRIVIAL = 0, dbm_MINDBM_COPY32, dbm_MINDBM_BITMATRIX32, dbm_MINDBM_TUPLES32,
  dbm_MINDBM_COPY16, dbm_MINDBM_BITMATRIX16, dbm_MINDBM_TUPLES16, dbm_MINDBM_ERROR
}
 Simple type to allow for statistics on the different internal formats used. More...

Functions

int32_t * dbm_writeToMinDBMWithOffset (const raw_t *dbm, cindex_t dim, BOOL minimizeGraph, BOOL tryConstraints16, allocator_t c_alloc, size_t offset)
 Save a DBM in minimal representation.
int32_t * dbm_writeAnalyzedDBM (const raw_t *dbm, cindex_t dim, uint32_t *bitMatrix, size_t nbConstraints, BOOL tryConstraints16, allocator_t c_alloc, size_t offset)
 Save a pre-analyzed DBM in minimal representation.
size_t dbm_analyzeForMinDBM (const raw_t *dbm, cindex_t dim, uint32_t *bitMatrix)
 Analyze a DBM for its minimal graph representation.
size_t dbm_cleanBitMatrix (const raw_t *dbm, cindex_t dim, uint32_t *bitMatrix, size_t nbConstraints)
 This is a post-processing function for dbm_analyzeForMinDBM to remove constraints of the form x>=0 that are part of the minimal graph but that do not give much information.
size_t dbm_getBitMatrixFromMinDBM (uint32_t *bitMatrix, mingraph_t ming, BOOL isUnpacked, raw_t *buffer)
 Get back the minimal graph from the internal representation.
void dbm_bitMatrix2indices (const uint32_t *bitMatrix, size_t nbConstraints, uint32_t *index, cindex_t dim)
 Convert a bit matrix marking constraints to an array of indices.
cindex_t dbm_readFromMinDBM (raw_t *dbm, mingraph_t minDBM)
 Read a DBM from its minimal DBM representation.
cindex_t dbm_getDimOfMinDBM (mingraph_t minDBM)
 Dimension of a DBM from its packed minimal representation.
size_t dbm_getSizeOfMinDBM (mingraph_t minDBM)
 Size of the representation of the MinDBM.
BOOL dbm_isEqualToMinDBM (const raw_t *dbm, cindex_t dim, mingraph_t minDBM)
 Equality test with a full DBM.
static BOOL dbm_areMinDBMVerbatimEqual (mingraph_t mg1, mingraph_t mg2)
 Equality test between 2 minimal graphs (saved with the same function and flags).
BOOL dbm_isAnalyzedDBMEqualToMinDBM (const raw_t *dbm, cindex_t dim, uint32_t *bitMatrix, size_t *nbConstraints, mingraph_t minDBM)
 Equality test with a full DBM.
BOOL dbm_isUnpackedEqualToMinDBM (const raw_t *dbm, cindex_t dim, mingraph_t minDBM, raw_t *buffer)
 Another variant for equality checking: this one may unpack the minimal graph if needed.
relation_t dbm_relationWithMinDBM (const raw_t *dbm, cindex_t dim, mingraph_t minDBM, raw_t *unpackBuffer)
 Relation between a full DBM and a minimal representation DBM.
relation_t dbm_approxRelationWithMinDBM (const raw_t *dbm, cindex_t dim, mingraph_t minDBM, raw_t *unpackBuffer)
 Variant of the previous relation function.
void dbm_convexUnionWithMinDBM (raw_t *dbm, cindex_t dim, mingraph_t minDBM, raw_t *unpackBuffer)
 Convex union.
representationOfMinDBM_t dbm_getRepresentationType (mingraph_t minDBM)

Detailed Description

Support for minimum graph representation.

The minimal graph is represented internally by the cheapest format possible, and in some cases it may even not be reduced. In addition to this, the size of the minimal graph depends on the actual input DBM, which makes the size of the allocated memory unpredictable from the caller point of view.

How allocation works

The idea is to have generic implementation that can be used with standard allocation schemes (malloc, new) and with custom allocators. This interface is in C to make it easy to wrap to other languages so we use a generic function to allocate memory. The type of this function is 
 int32_t* function(uint32_t size, void *data)
where:

Possible wrappers are:

The allocator function and the custom data are packed together inside the allocator_t type.

See also:
base/c_allocator.h

dbm_writeToMinDBMWithOffset()

Typedef Documentation

typedef const int32_t* mingraph_t
 

Style typedef: to make the difference clear between just allocated memory and the minimal graph representation.

Enumeration Type Documentation

enum representationOfMinDBM_t
 

Simple type to allow for statistics on the different internal formats used.

The format are not user controllable and should not be read from outside. For the tuple representation, it is not said here if it is (i,j,c_ij) or a bunch of c_ij and (i,j).

Enumeration values:
dbm_MINDBM_TRIVIAL  only clock ref, dim == 1
dbm_MINDBM_COPY32  32 bits, dbm copy without diagonal
dbm_MINDBM_BITMATRIX32  32 bits, c_ij and a bit matrix
dbm_MINDBM_TUPLES32  32 bits, c_ij and tuples (i,j)
dbm_MINDBM_COPY16  16 bits, dbm copy without diagonal
dbm_MINDBM_BITMATRIX16  16 bits, c_ij and a bit matrix
dbm_MINDBM_TUPLES16  16 bits, c_ij and tuples (i,j)
dbm_MINDBM_ERROR  should never be the case

Function Documentation

size_t dbm_analyzeForMinDBM (  const raw_t *  dbm,
cindex_t  dim,
uint32_t *  bitMatrix
) 
 

Analyze a DBM for its minimal graph representation.

Computes the smallest number of constraints needed to represent the same zone as the full DBM in dbm. The result in returned in bitMatrix: If the bit $ i \cdot dim + j$ is set, then the constraint $(i,j)$ of dbm is needed.

Parameters:
dbm,: DBM.
dim,: dimension.
bitMatrix,: bit matrix.
Returns:
  • number of needed constraints to save
  • bit matrix that marks which constraints belong to the minimal graph
Precondition:
bitMatrix is a uint32_t[bits2intsize(dim*dim)]

relation_t dbm_approxRelationWithMinDBM (  const raw_t *  dbm,
cindex_t  dim,
mingraph_t  minDBM,
raw_t *  unpackBuffer
) 
 

Variant of the previous relation function.

This may be cheaper if what count is to know (subset or equal) or different or superset. if unpackBuffer != NULL then dbm_EQUAL or dbm_SUBSET is returned if dbm == minDBM dbm_SUBSET is returned if dbm < minDBM dbm_SUPERSET is returned if dbm > minDBM dbm_DIFFERENT is returned if dbm not comparable with minDBM else dbm_SUBSET is returned if dbm <= minDBM dbm_DIFFERENT is returned otherwise

Parameters:
dbm,: full DBM to test.
dim,: its dimension.
minDBM,: minimal DBM representation.
unpackBuffer,: memory space to unpack. if unpackBuffer == NULL then the relation is not exact if unpackBuffer != NULL then assume that buffer = raw_t[dim*dim] to be able to unpack the DBM and compute an exact relation.
Precondition:
  • dbm is closed and not empty
  • dbm is a raw_t[dim*dim] (full DBM)
  • dim > 0 (at least ref clock)
Returns:
relation as described above.

static BOOL dbm_areMinDBMVerbatimEqual (  mingraph_t  mg1,
mingraph_t  mg2
)  [inline, static]
 

Equality test between 2 minimal graphs (saved with the same function and flags).

Parameters:
mg1,mg2,: minimal graph arguments.
Returns:
TRUE if the graphs are the same, provided they were saved with the same flags, FALSE otherwise.

void dbm_bitMatrix2indices (  const uint32_t *  bitMatrix,
size_t  nbConstraints,
uint32_t *  index,
cindex_t  dim
) 
 

Convert a bit matrix marking constraints to an array of indices.

Encoding: i[k] = (index[k] & 0xffff) and j[k] = (index[k] >> 16)

Parameters:
bitMatrix,: the bit matrix to convert.
nbConstraints,: number of set bit in the matrix.
index,: the index array to write.
dim,: dimension of the bit matrix.
Precondition:
index is a indexij_t[dim*(dim-1)] and bits on the diagonal are not marked, nbConstraints <= dim*(dim-1).

size_t dbm_cleanBitMatrix (  const raw_t *  dbm,
cindex_t  dim,
uint32_t *  bitMatrix,
size_t  nbConstraints
) 
 

This is a post-processing function for dbm_analyzeForMinDBM to remove constraints of the form x>=0 that are part of the minimal graph but that do not give much information.

Parameters:
dbm,dim,: DBM of dimension dim
bitMatrix,: bit matrix (already computed minimal graph)
nbConstraints,: the number of constraints of the minimal graph.
Returns:
the updated number of constraints of the modified minimal graph where constraints x>=0 may have been removed.
Precondition:
dbm_analyzeForMinDBM has been called before and nbConstraints corresponds to the number of constraints of the minimal graph.

void dbm_convexUnionWithMinDBM (  raw_t *  dbm,
cindex_t  dim,
mingraph_t  minDBM,
raw_t *  unpackBuffer
) 
 

Convex union.

This may cost dim^3 in time since the minimal DBM has to be unpacked to a full DBM. Computes dbm = dbm + minDBM

Parameters:
dbm,: dbm to make the union with.
dim,: its dimension.
minDBM,: minDBM to add to dbm (without offset).
unpackBuffer,: memory space to unpack the DBM.
Precondition:
  • dbm is a raw_t[dim*dim] and dim > 0 (at least ref clock).
  • DBMs have the same dimensions
  • unpackBuffer != NULL and is a raw_t[dim*dim]

size_t dbm_getBitMatrixFromMinDBM (  uint32_t *  bitMatrix,
mingraph_t  ming,
BOOL  isUnpacked,
raw_t *  buffer
) 
 

Get back the minimal graph from the internal representation.

It might be the case that the minimal graph is recomputed if the DBM was copied.

Parameters:
ming,: internal representation of the minimal graph.
bitMatrix,: bit matrix of the minimal graph to write.
isUnpacked,: says if buffer contains the unpacked DBM already.
buffer,: where to uncompress the full DBM if needed.
Returns:
the number of constraints part of the minimal graph.
Precondition:
let dim be the dimension of ming, bitMatrix is a uint32_t[bit2intsize(dim*dim)], buffer is a raw_t[dim*dim], and if isUnpacked is true then buffer contains the full DBM of ming.
Postcondition:
if ming is the result of saving a given dbm A, then the resulting bitMatrix is the same as the one given by dbm_analyzeForMinDBM(A,dim,bitMatrix) + buffer always contains the unpacked mingraph.

cindex_t dbm_getDimOfMinDBM (  mingraph_t  minDBM  ) 
 

Dimension of a DBM from its packed minimal representation.

Parameters:
minDBM,: the minimal DBM data directly, without offset.
Returns:
dimension of DBM.

representationOfMinDBM_t dbm_getRepresentationType (  mingraph_t  minDBM  ) 
 

Returns:
the type of the internal format used.
Parameters:
minDBM,: minimal representation (without offset) to read.

size_t dbm_getSizeOfMinDBM (  mingraph_t  minDBM  ) 
 

Size of the representation of the MinDBM.

This is the size of the allocated memory (without offset) for the minimal representation. It is at most dim*(dim-1)+1 because in the worst case the DBM is copied without its diagonal and we need one integer to store the size.

Parameters:
minDBM,: minimal DBM representation (without offset).
Returns:
size in int32_t allocated for the representation. NOTE: the write function allocates exactly int32_t[offset+dbm_getSizeOfMinDBM(minDBM)]

BOOL dbm_isAnalyzedDBMEqualToMinDBM (  const raw_t *  dbm,
cindex_t  dim,
uint32_t *  bitMatrix,
size_t *  nbConstraints,
mingraph_t  minDBM
) 
 

Equality test with a full DBM.

This variant of the equality test may be used if the DBM has already been analyzed or if you need to reuse the result of the analysis.

Parameters:
dbm,: full DBM.
dim,: dimension of dbm.
bitMatrix,: bit matrix resulting from the analysis of dbm (dbm_analyzeforMinDBM).
nbConstraints,: number of constraints marked in the bit matrix = number of bits set.
minDBM,: minimal DBM representation (without offset).
Precondition:
Returns:
TRUE if the DBMs are the same, FALSE otherwise.
Postcondition:
the bitMatrix may have the bits for the constraints on the 1st row cleaned and nbConstraints will be updated accordingly.

BOOL dbm_isEqualToMinDBM (  const raw_t *  dbm,
cindex_t  dim,
mingraph_t  minDBM
) 
 

Equality test with a full DBM.

Unfortunately, this may be expensive (dim^3) if the minimal graph format is used.

Parameters:
dbm,: full DBM.
dim,: dimension of dbm.
minDBM,: minimal DBM representation (without offset).
Precondition:
dbm is a raw_t[dim*dim] and dim > 0 (at least ref clock)
Returns:
TRUE if the DBMs are the same, FALSE otherwise.

BOOL dbm_isUnpackedEqualToMinDBM (  const raw_t *  dbm,
cindex_t  dim,
mingraph_t  minDBM,
raw_t *  buffer
) 
 

Another variant for equality checking: this one may unpack the minimal graph if needed.

It needs a buffer as an input to do so.

Parameters:
dbm,dim,: full DBM of dimension dim.
minDBM,: minimal DBM representation (without offset).
buffer,: buffer to unpack the DBM if needed
Precondition:
  • dbm is a raw_t[dim*dim] and dim > 0 (at leat ref clock)
  • buffer != NULL is a raw_t[dim*dim]
Postcondition:
  • buffer may be written or not. If you want to know it, you can set buffer[0] = 0, and test afterwards if buffer[0] == 0. If mingraph is unpacked then it is guaranteed that buffer[0] == dbm_LE_ZERO, otherwise buffer is untouched.
Returns:
TRUE if the DBMs are the same, FALSE otherwise.

cindex_t dbm_readFromMinDBM (  raw_t *  dbm,
mingraph_t  minDBM
) 
 

Read a DBM from its minimal DBM representation.

Parameters:
dbm,: where to write.
minDBM,: the minimal representation to read from.
Precondition:
  • dbm is a raw_t[dim*dim] where dim = dbm_getDimOfMinDBM(minDBM)
  • minDBM points to the data of the minDBM directly. There is no offset.
Returns:
dimension of DBM and unpacked DBM in dbm.

relation_t dbm_relationWithMinDBM (  const raw_t *  dbm,
cindex_t  dim,
mingraph_t  minDBM,
raw_t *  unpackBuffer
) 
 

Relation between a full DBM and a minimal representation DBM.

The relation may be exact or not: if the relation is exact then dbm_EQUAL is returned if dbm == minDBM dbm_SUBSET is returned if dbm < minDBM dbm_SUPERSET is returned if dbm > minDBM dbm_DIFFERENT is returned if dbm not comparable with minDBM else dbm_SUBSET is returned if dbm <= minDBM dbm_DIFFERENT otherwise

Parameters:
dbm,: full DBM to test.
dim,: its dimension.
minDBM,: minimal DBM representation.
unpackBuffer,: memory space to unpack. if unpackBuffer == NULL then the relation is not exact if unpackBuffer != NULL then assume that buffer = raw_t[dim*dim] to be able to unpack the DBM and compute an exact relation.
NOTE: unpackBuffer is sent as an argument to avoid stackoverflow if using stack allocation. The needed size is in dim*dim*sizeof(int). It is NOT guaranteed that unpackBuffer will be written. The dbm MAY be unpacked only if relation != subset and unpackBuffer != NULL.

Precondition:
  • dbm is closed and not empty
  • dbm is a raw_t[dim*dim] (full DBM)
  • dim > 0 (at least ref clock)
Returns:
relation as described above.

int32_t* dbm_writeAnalyzedDBM (  const raw_t *  dbm,
cindex_t  dim,
uint32_t *  bitMatrix,
size_t  nbConstraints,
BOOL  tryConstraints16,
allocator_t  c_alloc,
size_t  offset
) 
 

Save a pre-analyzed DBM in minimal representation.

Parameters:
dbm,: the DBM to save.
dim,: its dimension.
bitMatrix,: bit matrix resulting from the analysis (ie dbm_analyzeForMinDBM).
nbConstraints,: number of constraints in the bit matrix.
tryConstraints16,: flag to try to save constraints on 16 bits, will cost dim*dim time.
allocFunction,: the allocation function.
offset,: offset for allocation.
Returns:
allocated memory.
Precondition:
  • dbm is a raw_t[dim*dim]
  • allocFunction allocates memory in integer units
  • dbm is closed.
  • dim > 0 (at least ref clock)
  • bitMatrix != NULL, obtained from dbm_analyzeForMinDBM
  • nbConstraints = number of bits set in bitMatrix
  • bitMatrix is a uint32_t[bits2intsize(dim*dim)]
Postcondition:
  • the returned memory is of size offset+something unknown from the caller point of view.
  • bitMatrix is cleaned from the constraints xi >= 0

int32_t* dbm_writeToMinDBMWithOffset (  const raw_t *  dbm,
cindex_t  dim,
BOOL  minimizeGraph,
BOOL  tryConstraints16,
allocator_t  c_alloc,
size_t  offset
) 
 

Save a DBM in minimal representation.

The API supports allocation of larger data structures than needed for the actual zone representation. When the offset argument is bigger than zero, offset extra integers are allocated and the zone is written with the given offset. Thus when int32_t[data_size] is needed to represent the reduced zone, an int32_t array of size +data_sizeis allocated. The first offset elements can be used by the caller. It is important to notice that the other functions typically expect a pointer to the actual zone data and not to the beginning of the allocated block. Thus in the following piece of code, most functions expect mg and not memory: 

 int32_t *memory = dbm_writeToMinDBMWithOffset(...);
 mingraph_t mg = &memory[offset];

NOTES:

  • if offset is 0 and dim is 1, NULL may be returned. NULL is valid as an input to the other functions.
  • it could be possible to send as argument the maximal value of the constraints that can be deduced from the maximal constants but this would tie the algorithm to the extrapolation.

Parameters:
dbm,: the DBM to save.
dim,: its dimension.
minimizeGraph,: activate minimized graph reduction. If it is FALSE, then the DBM is copied without its diagonal.
tryConstraints16,: flag to try to save constraints on 16 bits, will cost dim*dim time.
c_alloc,: C allocator wrapper
offset,: offset for allocation.
Returns:
allocated memory.
Precondition:
  • dbm is a raw_t[dim*dim]
  • allocFunction allocates memory in integer units
  • dbm is closed.
  • dim > 0 (at least ref clock)
Postcondition:
the returned memory is of size offset+something unknown from the caller point of view.

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