priced.cpp File Reference

#include <cstdlib>
#include <algorithm>
#include <functional>
#include <stdexcept>
#include <iostream>
#include "debug/macros.h"
#include "dbm/priced.h"
#include "infimum.h"
#include "dbm/fed.h"
#include "dbm/print.h"

Defines
#define	DBM(I, J)   dbm[(I)*dim+(J)]
	Convenient macro for accessing DBM entries.
#define	pdbm_cost(pdbm)   ((pdbm)->cost)
	Returns the cost at the offset point.
#define	pdbm_rates(pdbm)   ((pdbm)->data)
	Returns the vectors of coefficients.
#define	pdbm_matrix(pdbm)   ((pdbm)->data + dim)
	Returns the matrix.
#define	pdbm_cache(pdbm)   ((pdbm)->infimum)
	Returns the cache infimum.
#define	pdbm_count(pdbm)   ((pdbm)->count)
	Returns the reference count.
#define	INVALID   INT_MAX
	Constant to mark the cached infimum as void.
Functions
static bool	pdbm_areOnZeroCycle (const PDBM pdbm, cindex_t dim, cindex_t i, cindex_t j)
	Returns true if two clocks form a zero cycle in a priced DBM.
static void	dbm_findZeroCycles (const raw_t *dbm, cindex_t dim, cindex_t *next)
	Find the zero cycles of a DBM.
static void	pdbm_prepare (PDBM &pdbm, cindex_t dim)
	Prepares a priced DBM for modification.
size_t	pdbm_size (cindex_t dim)
	Computes the size in number of bytes of a priced dbm of the given dimension.
PDBM	pdbm_reserve (cindex_t dim, void *p)
	Reserves a memory area for use as a priced DBM.
PDBM	pdbm_allocate (cindex_t dim)
	Allocates a new priced DBM.
void	pdbm_deallocate (PDBM &pdbm)
	Deallocates a priced DBM.
PDBM	pdbm_copy (PDBM dst, const PDBM src, cindex_t dim)
	Copy a priced DBM.
void	pdbm_init (PDBM &pdbm, cindex_t dim)
	Initialises a priced DBM to the DBM containing all valuations.
void	pdbm_zero (PDBM &pdbm, cindex_t dim)
	Initialize a priced DBM to only contain the origin with a cost of 0.
bool	pdbm_constrain1 (PDBM &pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint)
	Constrain a priced DBM.
bool	pdbm_constrainN (PDBM &pdbm, cindex_t dim, const constraint_t *constraints, size_t n)
	Constrain a priced DBM with multiple constraints.
static int32_t	costAtOtherOffset (const raw_t *dbm1, const int32_t *rates1, uint32_t cost1, const raw_t *dbm2, cindex_t dim)
	Returns the cost of the offset point of dbm2 in dbm1.
static bool	leq (const int32_t *first, const int32_t *last, const int32_t *rate)
	Given two planes, returns true if the slope of the first is less than or equal to the slope of the other.
static int32_t	infOfDiff (const raw_t *dbm, uint32_t dim, int32_t cost1, const int32_t *rate1, int32_t cost2, const int32_t *rate2)
	Given a zone and two hyperplanes over that zone, returns the infimum of the difference of the two planes.
relation_t	pdbm_relation (const PDBM pdbm1, const PDBM pdbm2, cindex_t dim)
	Relation between two priced DBMs.
relation_t	pdbm_relationWithMinDBM (const PDBM pdbm1, cindex_t dim, const mingraph_t pdbm2, raw_t *dbm2)
	Relation between 2 priced dbms where one is in compressed.
int32_t	pdbm_getInfimum (const PDBM pdbm, cindex_t dim)
	Computes the infimum cost of the priced DBM.
int32_t	pdbm_getInfimumValuation (const PDBM pdbm, cindex_t dim, int32_t *valuation, const bool *free)
	Generates a valuation which has the infimum cost of the priced DBM.
bool	pdbm_satisfies (const PDBM pdbm, cindex_t dim, cindex_t i, cindex_t j, raw_t constraint)
	Check if a priced DBM satisfies a given constraint.
bool	pdbm_isEmpty (const PDBM pdbm, cindex_t dim)
	Returns true if the priced DBM is empty.
bool	pdbm_isUnbounded (const PDBM pdbm, cindex_t dim)
	Check if at least one point can delay infinitely.
uint32_t	pdbm_hash (const PDBM pdbm, cindex_t dim, uint32_t seed)
	Compute a hash value for a priced DBM.
bool	pdbm_containsInt (const PDBM pdbm, cindex_t dim, const int32_t *pt)
	Test if a point is included in the priced DBM.
bool	pdbm_containsDouble (const PDBM pdbm, cindex_t dim, const double *pt)
	Test if a point is included in the priced DBM.
void	pdbm_up (PDBM &pdbm, cindex_t dim)
	Delay with the current delay rate.
void	pdbm_upZero (PDBM &pdbm, cindex_t dim, uint32_t rate, cindex_t zero)
	Delay with delay rate rate.
void	pdbm_updateValue (PDBM &pdbm, cindex_t dim, cindex_t clock, uint32_t value)
	Updates clock to value.
void	pdbm_updateValueZero (PDBM &pdbm, cindex_t dim, cindex_t clock, uint32_t value, cindex_t zero)
	Updates clock to value.
void	pdbm_extrapolateMaxBounds (PDBM &pdbm, cindex_t dim, int32_t *max)
	Unfinished extrapolation function.
void	pdbm_diagonalExtrapolateMaxBounds (PDBM &pdbm, cindex_t dim, int32_t *max)
	Unfinished extrapolation function.
void	pdbm_diagonalExtrapolateLUBounds (PDBM &pdbm, cindex_t dim, int32_t *lower, int32_t *upper)
	Extrapolate a priced zone.
void	pdbm_incrementCost (PDBM &pdbm, cindex_t dim, int32_t value)
	Increments the cost of each point in a priced DBM by value.
void	pdbm_close (PDBM &pdbm, cindex_t dim)
	Compute the closure of a priced DBM.
uint32_t	pdbm_analyzeForMinDBM (const PDBM pdbm, cindex_t dim, uint32_t *bitMatrix)
	Analyze a priced DBM for its minimal graph representation.
int32_t *	pdbm_writeToMinDBMWithOffset (const PDBM pdbm, cindex_t dim, bool minimizeGraph, bool tryConstraints16, allocator_t allocator, uint32_t offset)
	Convert the DBM to a more compact representation.
void	pdbm_readFromMinDBM (PDBM &dst, cindex_t dim, mingraph_t src)
	Uncompresses a compressed priced DBM.
bool	pdbm_findNextZeroCycle (const PDBM pdbm, cindex_t dim, cindex_t x, cindex_t *out)
	Finds a clock that is on a zero cycle with clock.
bool	pdbm_findZeroCycle (const PDBM pdbm, cindex_t dim, cindex_t x, cindex_t *out)
	Finds a clock that is on a zero cycle with clock.
int32_t	pdbm_getSlopeOfDelayTrajectory (const PDBM pdbm, cindex_t dim)
	Returns the slope of the cost plane along the delay trajectory.
int32_t	pdbm_getRate (const PDBM pdbm, cindex_t dim, cindex_t clock)
	Returns the rate (coefficient of the hyperplane) of clock.
uint32_t	pdbm_getCostAtOffset (const PDBM pdbm, cindex_t dim)
	Returns the cost of the offset point.
void	pdbm_setCostAtOffset (PDBM &pdbm, cindex_t dim, uint32_t value)
	Sets the cost at the offset point.
static bool	isRedundant (const raw_t *dbm, cindex_t dim, cindex_t i, cindex_t j, cindex_t *next)
uint32_t	pdbm_getLowerRelativeFacets (PDBM &pdbm, cindex_t dim, cindex_t clock, cindex_t *facets)
	Computes the lower facets of a priced DBM relative to clock.
uint32_t	pdbm_getUpperRelativeFacets (PDBM &pdbm, cindex_t dim, cindex_t clock, cindex_t *facets)
	Computes the upper facets of a priced DBM relative to clock.
uint32_t	pdbm_getLowerFacets (PDBM &pdbm, cindex_t dim, cindex_t *facets)
	Computes the lower facets of a priced DBM.
uint32_t	pdbm_getUpperFacets (PDBM &pdbm, cindex_t dim, cindex_t *facets)
	Computes the upper facets of a priced DBM.
int32_t	pdbm_getCostOfValuation (const PDBM pdbm, cindex_t dim, const int32_t *valuation)
	Computes the cost of a valuation in a priced DBM.
void	pdbm_relax (PDBM &pdbm, cindex_t dim)
	Makes all strong constraints of a priced DBM weak.
bool	pdbm_isValid (const PDBM pdbm, cindex_t dim)
	Returns true if the DBM is valid.
void	pdbm_freeClock (PDBM &pdbm, cindex_t dim, cindex_t clock)
	Frees a clock of a priced DBM.
void	pdbm_getOffset (const PDBM pdbm, cindex_t dim, int32_t *valuation)
	Computes the offset point of a priced DBM.
void	pdbm_setRate (PDBM &pdbm, cindex_t dim, cindex_t clock, int32_t rate)
	Sets a coefficient of the hyperplane of a priced DBM.
raw_t *	pdbm_getMutableMatrix (PDBM &pdbm, cindex_t dim)
	Returns the inner matrix of a priced DBM.
const raw_t *	pdbm_getMatrix (const PDBM pdbm, cindex_t dim)
	Returns the inner matrix of a priced DBM.
const int32_t *	pdbm_getRates (const PDBM pdbm, cindex_t dim)
bool	pdbm_constrainToFacet (PDBM &pdbm, cindex_t dim, cindex_t i, cindex_t j)
	Constrain a priced DBM to a facet (i, j).
void	pdbm_print (FILE *f, const PDBM pdbm, cindex_t dim)
	Prints a priced DBM to a stream.
void	pdbm_freeUp (PDBM &pdbm, cindex_t dim, cindex_t index)
	Implementation of the free up operation for priced DBMs.
void	pdbm_freeDown (PDBM &pdbm, cindex_t dim, cindex_t index)
	Implementation of the free down operation for priced DBMs.
void	pdbm_normalise (PDBM pdbm, cindex_t dim)
	Brings a priced DBM into normal form.
bool	pdbm_hasNormalForm (PDBM pdbm, cindex_t dim)
	Checks whether a priced DBM is in normal form.

---

Define Documentation

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

Convenient macro for accessing DBM entries.

#define INVALID   INT_MAX

Constant to mark the cached infimum as void.

#define pdbm_cache (  pdbm   )     ((pdbm)->infimum)

Returns the cache infimum.

#define pdbm_cost (  pdbm   )     ((pdbm)->cost)

Returns the cost at the offset point.

#define pdbm_count (  pdbm   )     ((pdbm)->count)

Returns the reference count.

#define pdbm_matrix (  pdbm   )     ((pdbm)->data + dim)

Returns the matrix.

#define pdbm_rates (  pdbm   )     ((pdbm)->data)

Returns the vectors of coefficients.

---

Function Documentation

static int32_t costAtOtherOffset (  const raw_t *  dbm1, const int32_t *  rates1, uint32_t  cost1, const raw_t *  dbm2, cindex_t  dim )  [static]

Returns the cost of the offset point of dbm2 in dbm1. Parameters: dbm1  is the DBM for which to find the cost. rates1  are the coefficients of the hyperplane of dbm1. cost1  is the cost of the offset point of dbm1 dbm2  is the DBM providing the offset point for which we want to find the cost. dim  is the dimension of dbm1 and dbm2.

static void dbm_findZeroCycles (  const raw_t *  dbm, cindex_t  dim, cindex_t *  next )  [static]

Find the zero cycles of a DBM. The zero cycles are represented by an array which for each clock contains the next element on the zero cycle, or * 0 if the clock is the last element. I.e. next[i] is the index of the next clock on a zero cycle with i. Postcondition: forall i.next[i] == 0 || next[i] > i

static int32_t infOfDiff (  const raw_t *  dbm, uint32_t  dim, int32_t  cost1, const int32_t *  rate1, int32_t  cost2, const int32_t *  rate2 )  [static]

Given a zone and two hyperplanes over that zone, returns the infimum of the difference of the two planes. Parameters: dbm  A DBM. dim  The dimension of the DBM. cost1  The cost at the offset for the first plane. rate1  The rates of the first plane. cost2  The cost at the offset for the second plane. rate2  The rates of the second plane.

static bool isRedundant (  const raw_t *  dbm, cindex_t  dim, cindex_t  i, cindex_t  j, cindex_t *  next )  [static]

static bool leq (  const int32_t *  first, const int32_t *  last, const int32_t *  rate )  [inline, static]

Given two planes, returns true if the slope of the first is less than or equal to the slope of the other. Parameters: first  is a pointer to the first coefficient of the first plane. last  is a pointer to the last coefficient of the first plane. rate  is a pointer to the first coefficient of the second plane.

PDBM pdbm_allocate (  cindex_t  dim  )

Allocates a new priced DBM. The reference count is initialised to 0. No other initialisation is performed. Parameters: dim  is the dimension. Returns: A newly allocated priced DBM of dimension dim. Precondition: dim is larger than 0.

uint32_t pdbm_analyzeForMinDBM (  const PDBM  pdbm, cindex_t  dim, uint32_t *  bitMatrix )

Analyze a priced DBM for its minimal graph representation. Computes the smallest number of constraints needed to represent the same zone. The result is returned as a bit matrix, where each bit indicates whether that entry of the DBM is relevant. I.e. if the bit is set, then the constraint of dbm is needed. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. bitMatrix  is bit matrix of size dim*dim Returns: The number of bits marked one in bitMatrix.

static bool pdbm_areOnZeroCycle (  const PDBM  pdbm, cindex_t  dim, cindex_t  i, cindex_t  j )  [static]

Returns true if two clocks form a zero cycle in a priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. i  is the index of a clock j  is the index of a clock Returns: True if and only if i and j form a zero cycle in pdbm.

void pdbm_close (  PDBM &  pdbm, cindex_t  dim )

Compute the closure of a priced DBM. This function is only relevant if the DBM has been modified with pdbm_setBound(). Parameters: pdbm  is a priced DBM of dimension dim. dim  is the dimension of pdbm. Postcondition: The priced DBM is closed or empty. See also: pdbm_setBound

bool pdbm_constrain1 (  PDBM &  pdbm, cindex_t  dim, cindex_t  i, cindex_t  j, raw_t  constraint )

Constrain a priced DBM. After the call, the DBM will be constrained such that the difference between clock i and clock j is smaller than constraint. See also: dbm_constrain1 Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. i  is a clock index. j  is a clock index. constraint  is a raw_t bound. Precondition: i != j Postcondition: The DBM is empty or closed. Returns: True if and only if the result is not empty.

bool pdbm_constrainN (  PDBM &  pdbm, cindex_t  dim, const constraint_t *  constraints, size_t  n )

Constrain a priced DBM with multiple constraints. See also: dbm_constraint1 Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. constraints  is an array of n constraints. n  is the length of constraints. Precondition: the constraints are valid Postcondition: The DBM is empty or closed. Returns: TRUE if the DBM is non empty + closed non empty DBM + updated consistent rates or FALSE if the DBM is empty + empty DBM + inconsistent rates

bool pdbm_constrainToFacet (  PDBM &  pdbm, cindex_t  dim, cindex_t  i, cindex_t  j )

Constrain a priced DBM to a facet (i, j). Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. i  is a clock index j  is a clock index Postcondition: The DBM is empty or closed. Returns: TRUE if and only if the result is non empty.

bool pdbm_containsDouble (  const PDBM  pdbm, cindex_t  dim, const double *  pt )

Test if a point is included in the priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. pt  is a clock valuation. Returns: TRUE if pt satisfies the constraints of dbm.

bool pdbm_containsInt (  const PDBM  pdbm, cindex_t  dim, const int32_t *  pt )

Test if a point is included in the priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. pt  is a clock valuation. Returns: TRUE if pt satisfies the constraints of dbm.

PDBM pdbm_copy (  PDBM  dst, const PDBM  src, cindex_t  dim )

Copy a priced DBM. This function copies the data of the DBM. Hence, it is only permissible if the reference count of dst is zero. If dst is NULL, a new DBM is allocate with pdbm_allocate(). Parameters: dst  The destination. src  The source. dim  The dimension of dst and src. Precondition: The reference count of dst is zero or dst is NULL. Postcondition: The reference count of the return value is zero. Returns: The destination.

void pdbm_deallocate (  PDBM &  pdbm  )

Deallocates a priced DBM. Precondition: pdbm was allocated with pdbm_allocate(). The reference count of pdbm is zero.

void pdbm_diagonalExtrapolateLUBounds (  PDBM &  pdbm, cindex_t  dim, int32_t *  lower, int32_t *  upper )

Extrapolate a priced zone. The extrapolation is based on a lower and an upper bound for each clock. The output zone simulates the input zone. The implementation is not finished. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. lower  is an array of lower bounds for each clock. upper  is an array of upper bounds for each clock. Precondition: lower[0] = upper[0] = 0 Postcondition: The priced DBM is closed. See also: dbm_diagonalExtrapolateLUBounds

void pdbm_diagonalExtrapolateMaxBounds (  PDBM &  pdbm, cindex_t  dim, int32_t *  max )

Unfinished extrapolation function. See also: dbm_diagonalExtrapolateMaxBounds

void pdbm_extrapolateMaxBounds (  PDBM &  pdbm, cindex_t  dim, int32_t *  max )

Unfinished extrapolation function. See also: dbm_extrapolateMaxBounds

bool pdbm_findNextZeroCycle (  const PDBM  pdbm, cindex_t  dim, cindex_t  x, cindex_t *  out )

Finds a clock that is on a zero cycle with clock. Returns TRUE if and only if such a clock is found. Only clocks with a value equal to or greater than the existing value of output are considered. If multiple clocks are on a zero cycle with clock, then the clock with the smallest index is returned. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. clock  is the index of a clock. out  is where the clock found is written. Returns: TRUE if and only if a clock is found.

bool pdbm_findZeroCycle (  const PDBM  pdbm, cindex_t  dim, cindex_t  clock, cindex_t *  out )

Finds a clock that is on a zero cycle with clock. Returns TRUE if and only if such a clock is found. If multiple clocks are on a zero cycle with clock, then the clock with the smallest index is returned. This function is equivalent to calling pdbm_findNextZeroCyle with output initialised to zero. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. clock  is the index of a clock. out  is where the clock found is written. Returns: TRUE if and only if a clock is found.

void pdbm_freeClock (  PDBM &  pdbm, cindex_t  dim, cindex_t  clock )

Frees a clock of a priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. clock  is the index of the clock to free.

void pdbm_freeDown (  PDBM &  pdbm, cindex_t  dim, cindex_t  index )

Implementation of the free down operation for priced DBMs. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. index  is an index of a clock. * See also: dbm_freeDown

void pdbm_freeUp (  PDBM &  pdbm, cindex_t  dim, cindex_t  index )

Implementation of the free up operation for priced DBMs. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. index  is an index of a clock. See also: dbm_freeUp

uint32_t pdbm_getCostAtOffset (  const PDBM  pdbm, cindex_t  dim )

Returns the cost of the offset point. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm.

int32_t pdbm_getCostOfValuation (  const PDBM  pdbm, cindex_t  dim, const int32_t *  valuation )

Computes the cost of a valuation in a priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. valuation  is a valuation in pdbm. Precondition: pdbm_containsInt(pdbm, dim, valuation) Returns: The cost of valuation in pdbm.

int32_t pdbm_getInfimum (  const PDBM  pdbm, cindex_t  dim )

Computes the infimum cost of the priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim dim  is the dimension of pdbm. Returns: The infimum cost of pdbm.

int32_t pdbm_getInfimumValuation (  const PDBM  pdbm, cindex_t  dim, int32_t *  valuation, const bool *  free )

Generates a valuation which has the infimum cost of the priced DBM. There is no guarantee that the valuation will be contained in the priced DBM, but if it is not it is arbitrarily close to a valuation that is contained in the priced DBM. A false entry in free indicates that the value of this clock has already been set in valuation and that this clock must not be modified. The function will only modify free clocks. Parameters: pdbm  is a closed priced DBM of dimension dim dim  is the dimension of pdbm. valuation  is an array of at least dim elements to which the the valuation will be written. free  is an array of at least dim elements. Returns: The cost of valuation. Exceptions: out_of_range  if no valuation with the given constraints can be found.

uint32_t pdbm_getLowerFacets (  PDBM &  pdbm, cindex_t  dim, cindex_t *  facets )

Computes the lower facets of a priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. facets  is an array of at least dim elements to which the lower facets will be written. Returns: The number of facets written to facets.

uint32_t pdbm_getLowerRelativeFacets (  PDBM &  pdbm, cindex_t  dim, cindex_t  clock, cindex_t *  facets )

Computes the lower facets of a priced DBM relative to clock. As a side-effect, all lower facets relative to clock are converted to weak facets. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. clock  is the clock for which to return the lower facets facets  is an array of at least dim elements to which the lower facets will be written. Returns: The number of facets written to facets.

const raw_t* pdbm_getMatrix (  const PDBM  pdbm, cindex_t  dim )

Returns the inner matrix of a priced DBM. The matrix is read-only. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm.

raw_t* pdbm_getMutableMatrix (  PDBM &  pdbm, cindex_t  dim )

Returns the inner matrix of a priced DBM. The matrix can be modified as long as pdbm_close() is called before any other operations are performed on the priced DBM. Parameters: pdbm  is a priced DBM of dimension dim. dim  is the dimension of pdbm.

void pdbm_getOffset (  const PDBM  pdbm, cindex_t  dim, int32_t *  valuation )

Computes the offset point of a priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. valuation  is an array of at least dim elements to which the offset point is written.

int32_t pdbm_getRate (  const PDBM  pdbm, cindex_t  dim, cindex_t  clock )

Returns the rate (coefficient of the hyperplane) of clock. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. clock  is the clock for which to return the coefficient. Returns: the rate of clock.

const int32_t* pdbm_getRates (  const PDBM  pdbm, cindex_t  dim )

int32_t pdbm_getSlopeOfDelayTrajectory (  const PDBM  pdbm, cindex_t  dim )

Returns the slope of the cost plane along the delay trajectory. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm.

uint32_t pdbm_getUpperFacets (  PDBM &  pdbm, cindex_t  dim, cindex_t *  facets )

Computes the upper facets of a priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. facets  is an array of at least dim elements to which the upper facets will be written. Returns: The number of facets written to facets.

uint32_t pdbm_getUpperRelativeFacets (  PDBM &  pdbm, cindex_t  dim, cindex_t  clock, cindex_t *  facets )

Computes the upper facets of a priced DBM relative to clock. As a side-effect, all upper facets relative to clock are converted to weak facets. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. clock  is the clock for which to return the upper facets facets  is an array of at least dim elements to which the upper facets will be written. Returns: The number of facets written to facets.

uint32_t pdbm_hash (  const PDBM  pdbm, cindex_t  dim, uint32_t  seed )

Compute a hash value for a priced DBM. ISSUE: canonical form needed. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. seed  is a seed for the hash function. Returns: hash value.

bool pdbm_hasNormalForm (  PDBM  pdbm, cindex_t  dim )

Checks whether a priced DBM is in normal form. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm.

void pdbm_incrementCost (  PDBM &  pdbm, cindex_t  dim, int32_t  value )

Increments the cost of each point in a priced DBM by value. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. value  is the amount with which to increase the cost. Postcondition: The priced DBM is closed. Precondition: value >= 0

void pdbm_init (  PDBM &  pdbm, cindex_t  dim )

Initialises a priced DBM to the DBM containing all valuations. The cost of all valuations will be zero. If pdbm is NULL, a new DBM is allocated with pdbm_allocate(). Parameters: pdbm  is the priced DBM to initialize. dim  is the dimension of pdbm.

bool pdbm_isEmpty (  const PDBM  pdbm, cindex_t  dim )

Returns true if the priced DBM is empty. Parameters: pdbm  is a closed or empty priced DBM of dimension dim. dim  is the dimension of pdbm. Returns: TRUE if and only if the priced dbm is empty.

bool pdbm_isUnbounded (  const PDBM  pdbm, cindex_t  dim )

Check if at least one point can delay infinitely. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. Returns: TRUE if unbounded, FALSE otherwise.

bool pdbm_isValid (  const PDBM  pdbm, cindex_t  dim )

Returns true if the DBM is valid. Useful for debugging. Parameters: pdbm  is a priced DBM of dimension dim. dim  is the dimension of pdbm.

void pdbm_normalise (  PDBM  pdbm, cindex_t  dim )

Brings a priced DBM into normal form. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm.

static void pdbm_prepare (  PDBM &  pdbm, cindex_t  dim )  [static]

Prepares a priced DBM for modification. If it is shared, a copy will be created.

void pdbm_print (  FILE *  f, const PDBM  pdbm, cindex_t  dim )

Prints a priced DBM to a stream. Parameters: f  is the stream to print to. pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. See also: dbm_print

void pdbm_readFromMinDBM (  PDBM &  dst, cindex_t  dim, mingraph_t  src )

Uncompresses a compressed priced DBM. The compressed priced DBM src is written to dst. The destination does not need to initialised beforehand. The dimension dim must match the dimension of the compressed priced DBM. Parameters: dst  is a memory area of size pdbm_size(dim). dim  is the dimension of the priced DBM. src  is the compressed priced DBM. Postcondition: dst is a closed priced DBM.

relation_t pdbm_relation (  const PDBM  pdbm1, const PDBM  pdbm2, cindex_t  dim )

Relation between two priced DBMs. See also: relation_t Parameters: pdbm1  is a closed priced DBMs of dimension dim. pdbm2  is a closed priced DBMs of dimension dim. dim  is the dimension of pdbm1 and pdbm2. Returns: The relation between pdbm1 and pdbm2

relation_t pdbm_relationWithMinDBM (  const PDBM  pdbm, cindex_t  dim, const mingraph_t  minDBM, raw_t *  buffer )

Relation between 2 priced dbms where one is in compressed. Notice that in constract to dbm_relationWithMinDBM, buffer may not be NULL. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. minDBM  is the compressed priced dbm. buffer  is a buffer of size dim*dim. Returns: The relation between pdbm1 and pdbm2 See also: dbm_relationWithMinDBM relation_t

void pdbm_relax (  PDBM &  pdbm, cindex_t  dim )

Makes all strong constraints of a priced DBM weak. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. Postcondition: The priced DBM is closed.

PDBM pdbm_reserve (  cindex_t  dim, void *  p )

Reserves a memory area for use as a priced DBM. The priced DBM will be unitialised, hence further initialised with e.g. pdbm_init() or pdbm_zero() is required. Parameters: dim  is the dimension of the priced DBM to reserve. p  is a memory area of size pdbm_size(dim). Returns: An unitialised priced DBM of dimension dim.

bool pdbm_satisfies (  const PDBM  pdbm, cindex_t  dim, cindex_t  i, cindex_t  j, raw_t  constraint )

Check if a priced DBM satisfies a given constraint. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. i,j  are theindices of clocks for the clock constraint. constraint  is the raw_t bound. Returns: TRUE if the DBM satisfies the constraint.

void pdbm_setCostAtOffset (  PDBM &  pdbm, cindex_t  dim, uint32_t  value )

Sets the cost at the offset point. Notice that the value must be large enough such that the infimum cost of the priced DBM is not negative. Temporary inconsistencies are allowed as long as no operations are performed on the priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. value  is the new cost of the offset point.

void pdbm_setRate (  PDBM &  pdbm, cindex_t  dim, cindex_t  clock, int32_t  rate )

Sets a coefficient of the hyperplane of a priced DBM. Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. clock  is the index of a clock for which to set the coefficient. rate  is the coefficient.

size_t pdbm_size (  cindex_t  dim  )

Computes the size in number of bytes of a priced dbm of the given dimension. Parameters: dim  is a dimension. Precondition: dim > 0 Returns: Amount of memory in bytes.

void pdbm_up (  PDBM &  pdbm, cindex_t  dim )

Delay with the current delay rate. Parameters: pdbm  is a closed priced dbm of dimension dim. dim  is the dimension of pdbm. See also: pdbm_delayRate() Postcondition: The priced DBM is closed.

void pdbm_updateValue (  PDBM &  pdbm, cindex_t  dim, cindex_t  clock, uint32_t  value )

Updates clock to value. This is only legitimate if the current rate of clock is zero. Parameters: pdbm  is a closed priced dbm of dimension dim. dim  is the dimension of pdbm. clock  is the index of the clock to reset. value  is the value to which to set clock. Precondition: pdbm_getRate(pdbm, dim, clock) == 0 Postcondition: The priced DBM is closed.

void pdbm_updateValueZero (  PDBM &  pdbm, cindex_t  dim, cindex_t  clock, uint32_t  value, cindex_t  zero )

Updates clock to value. This is only legitimate if the clock forms a zero cycle with another clock (possibly the reference clock). Parameters: pdbm  is a closed priced dbm of dimension dim. dim  is the dimension of pdbm. clock  is the index of the clock to reset. value  is the value to which to set clock. zero  is a clock (possibly zero) forming a zero cycle with clock. Postcondition: The priced DBM is closed. pdbm_getRate(pdbm, dim, clock) == 0

void pdbm_upZero (  PDBM &  pdbm, cindex_t  dim, uint32_t  rate, cindex_t  zero )

Delay with delay rate rate. There must be at least one clock forming a zero cycle with the reference clock. Parameters: pdbm  is a closed priced dbm of dimension dim. dim  is the dimension of pdbm. rate  is the cost of delaying. zero  is the index of a clock forming a zero cycle with the reference clock. Postcondition: The priced DBM is closed.

int32_t* pdbm_writeToMinDBMWithOffset (  const PDBM  pdbm, cindex_t  dim, bool  minimizeGraph, bool  tryConstraints16, allocator_t  c_alloc, uint32_t  offset )

Convert the DBM to a more compact 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 offset+data_size is 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]; Parameters: pdbm  is a closed priced DBM of dimension dim. dim  is the dimension of pdbm. minimizeGraph  when true, try to use minimal constraint form. tryConstraints16  when true, try to save constraints on 16 bits. c_alloc  is a C allocator wrapper. offset  is the offset for allocation. Returns: The converted priced DBM. The first offset integers are unused. Precondition: allocFunction allocates memory in integer units

void pdbm_zero (  PDBM &  pdbm, cindex_t  dim )

Initialize a priced DBM to only contain the origin with a cost of 0. If pdbm is NULL, a new DBM is allocated with pdbm_allocate(). Parameters: pdbm  is the priced DBM to initialise. dim  is the dimension of pdbm.

---