Module dbm Documentation

4.1.0 ()

raw_t is the encoded clock constraint

See also:

constraints.h.

IMPORTANT NOTE: in the system, you will typically have clocks x1,x2...,xn. The dbm will have x0 as the reference clock, hence dimension = n + 1 => ASSUME dimension > 0

Format of a dbm of dimension dim: dbm[i,j] = dbm[i*dim+j] where dbm[i,j] = constraint xi-xj < or <= c_ij The constraint encoding is described in constraints.h

The API does not support indirection table for clocks. Dynamic mappings must be resolved before calling these functions. Be careful when dealing with operation that involve arrays of constraints (e.g. kExtrapolate). As a common assumption for all operations on DBM: dim > 0, which means at least the reference clock is in the DBM. DBM non empty means the represented zone is non empty, which is, for a closed dbm the diagonal elements are =0.

Common pre-condition: DBMs are always of dimension >= 1.

---