gen.h File Reference

#include "dbm/constraints.h"

Go to the source code of this file.

Functions
BOOL	dbm_generate (raw_t *dbm, cindex_t dim, raw_t range)
	Generate a random closed and non empty DBM.
BOOL	dbm_generateConstrained (raw_t *dbm, cindex_t dim, raw_t range, const constraint_t *constraints, size_t n)
	Generate a random closed and non empty DBM that satisfy a number of constraints.
void	dbm_generatePreConstrained (raw_t *dbm, cindex_t dim, raw_t range, const uint32_t *bitMatrix)
	Constrain randomly an already constrained DBM.
void	dbm_generateArgDBM (raw_t *arg, const raw_t *dbm, cindex_t dim)
	Generate 2nd DBM argument for intersection/substraction with a first DBM.
void	dbm_generateSuperset (raw_t *dst, const raw_t *src, cindex_t dim)
	Generate a superset DBM.
BOOL	dbm_generateSubset (raw_t *dst, const raw_t *src, cindex_t dim)
	Generate a subset DBM.
BOOL	dbm_generatePoint (int32_t *pt, const raw_t *dbm, cindex_t dim)
	Generate a random discrete point that belongs to the zone.
BOOL	dbm_generateRealPoint (double *pt, const raw_t *dbm, cindex_t dim)
	Generate a random real point that belongs to the zone.

---

Function Documentation

BOOL dbm_generate (  raw_t *  dbm, cindex_t  dim, raw_t  range )

Generate a random closed and non empty DBM. Parameters: dbm,:  where to write the DBM. dim,:  dimension. range,:  approximate range for the values. Returns: TRUE if it is a non trivial one (sometimes the generation may fail and fall back to a trivial DBM). A trivial DBM is created by dbm_init. Precondition: dbm is a raw_t[dim*dim]

void dbm_generateArgDBM (  raw_t *  arg, const raw_t *  dbm, cindex_t  dim )

Generate 2nd DBM argument for intersection/substraction with a first DBM. Parameters: dbm,dim,:  first DBM of dimension dim to generate a second DBM argument from. arg,:  where to generate a DBM of dimension dim to test for intersection or substraction. Precondition: dbm closed and not empty, arg is a raw_t[dim*dim] Postcondition: arg is closed and not empty

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

Generate a random closed and non empty DBM that satisfy a number of constraints. Parameters: dbm,:  where to write the DBM. dim,:  dimension. range,:  approximate range for the values. constraints,n,:  the n constraints the DBM has to satisfy. Precondition: constraints[n] do not result in an empty DBM dbm is a raw_t[dim*dim], dim > 0 Postcondition: the result is non empty Returns: TRUE if generation succeeded, FALSE if it failed.

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

Generate a random discrete point that belongs to the zone. Parameters: pt,:  memory where to write the point (x0,x1,x2..) dbm,:  DBM. dim,:  dimension. Precondition: dbm is a raw_t[dim*dim] and ptr is a int32_t[dim] dbm is closed and non empty, dim > 0 Returns: TRUE if generated point is included in the DBM.

void dbm_generatePreConstrained (  raw_t *  dbm, cindex_t  dim, raw_t  range, const uint32_t *  bitMatrix )

Constrain randomly an already constrained DBM. Parameters: dbm,dim,:  DBM of dimension dim to constrain. range,:  maximal range for the generated valued. bitMatrix,:  bit matrix marking the constraints that should be kept. Precondition: dbm is closed and non empty, dim > 0. Postcondition: dbm is closed and non empty.

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

Generate a random real point that belongs to the zone. Always succeeds if zone is not empty (pre-condition). Parameters: pt,:  memory where to write the point (x0,x1,x2..) dbm,:  DBM. dim,:  dimension. Precondition: dbm is a raw_t[dim*dim] and ptr is a int32_t[dim] dbm is closed and non empty, dim > 0 Returns: TRUE if generation succeeded Postcondition: pt is valid only if the generation succeeded

BOOL dbm_generateSubset (  raw_t *  dst, const raw_t *  src, cindex_t  dim )

Generate a subset DBM. Parameters: src,:  the original DBM. dst,:  where to write subset. dim,:  dimension. Precondition: src and dst are raw_t[dim*dim] src is non empty and closed Postcondition: dst is non empty and closed dst >= src Returns: TRUE if the subset is strict

void dbm_generateSuperset (  raw_t *  dst, const raw_t *  src, cindex_t  dim )

Generate a superset DBM. Parameters: src,:  the original DBM. dst,:  where to write superset. dim,:  dimension. Precondition: src and dst are raw_t[dim*dim] src is non empty and closed Postcondition: dst is non empty and closed dst >= src

---