pyudbm.binding.udbm

Legacy-style high-level UDBM API.

This module exposes the main Python modeling layer of pyudbm. It keeps the historical Context / Clock / Federation programming model while delegating the actual Difference Bound Matrix (DBM) algorithms to the native UDBM library.

Conceptually, the binding mirrors the standard timed-automata representation used by UDBM:

a DBM represents one convex zone, that is, one conjunction of constraints of the form x_i - x_j <= c;
a federation is a finite union of DBMs, used for non-convex symbolic states;
clock 0 is the implicit reference clock x0 = 0 used by UDBM, while user-visible clocks start at DBM index 1;
the Python DSL turns natural expressions such as c.x < 5 or c.x - c.y <= 2 into native UDBM constraints.

The Python layer intentionally stays thin: methods like Federation.up(), Federation.down(), Federation.predt(), and Federation.extrapolate_max_bounds() are direct high-level wrappers around the corresponding UDBM operations. The documentation below therefore explains both the Python API and the underlying DBM semantics.

Example:

>>> from pyudbm import Context, IntValuation
>>> context = Context(["x", "y"], name="c")
>>> zone = (context.x < 10) & (context.x - context.y > 1)
>>> relaxed = zone.up()
>>> valuation = IntValuation(context)
>>> valuation["x"] = 5
>>> valuation["y"] = 3
>>> zone.contains(valuation)
True
>>> relaxed >= zone
True

all

pyudbm.binding.udbm.__all__ = ['DBM', 'Clock', 'Constraint', 'Context', 'Federation', 'FloatValuation', 'IntValuation', 'Valuation', 'VariableDifference']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

LOGGER

pyudbm.binding.udbm.LOGGER = <Logger pyudbm (WARNING)>: Instances of the Logger class represent a single logging channel. A “logging channel” indicates an area of an application. Exactly how an “area” is defined is up to the application developer. Since an application can have any number of areas, logging channels are identified by a unique string. Application areas can be nested (e.g. an area of “input processing” might include sub-areas “read CSV files”, “read XLS files” and “read Gnumeric files”). To cater for this natural nesting, channel names are organized into a namespace hierarchy where levels are separated by periods, much like the Java or Python package namespace. So in the instance given above, channel names might be “input” for the upper level, and “input.csv”, “input.xls” and “input.gnu” for the sub-levels. There is no arbitrary limit to the depth of nesting.

DBM

class pyudbm.binding.udbm.DBM(context: Context, native: _NativeDBM)[source]

Immutable read-only DBM snapshot.

A DBM represents one convex zone extracted from a federation. It provides DBM-level rendering, direct matrix-cell inspection, matrix export, and minimal-graph export while staying detached from future mutations of the source federation.

In UDBM terms, this object is one closed DBM over the clocks of a single Context. The first matrix row and column always correspond to the implicit reference clock 0. User clocks therefore start at matrix index 1 even though they are exposed by name at the Python level.

Parameters:

context (Context) – Context whose clock names apply to this DBM.
native (_NativeDBM) – Native DBM snapshot.

Variables:

context – Context whose clock names label the DBM matrix.

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"], name="c")
>>> federation = (context.x <= 10) & (context.y <= 7) & (context.x - context.y < 3)
>>> dbm = federation.to_dbm_list()[0]
>>> dbm.dimension
3
>>> dbm.clock_names
('0', 'c.x', 'c.y')
>>> str(dbm)
'(c.x-c.y<3 & c.y<=7)'

__init__(context: Context, native: _NativeDBM)[source]

Initialize one read-only DBM snapshot.

Instances are normally created internally by Federation.to_dbm_list() rather than directly by user code.

Parameters:

context (Context) – Context whose clock names apply to this DBM.
native (_NativeDBM) – Native DBM snapshot.

Returns:

None.

Return type:

None

__repr__() → str[source]

Return a debugging representation including the DBM clock names.

Returns:: Debugging representation.
Return type:: str

Example:

>>> from pyudbm import Context
>>> dbm = (Context(["x"], name="c").x <= 1).to_dbm_list()[0]
>>> repr(dbm)
"DBM(clock_names=('0', 'c.x'))"

__str__() → str[source]

Return the default minimal textual rendering of the DBM.

Returns:: Minimal DBM expression.
Return type:: str

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"], name="c")
>>> dbm = ((context.x <= 10) & (context.y <= 7) & (context.x - context.y < 3)).to_dbm_list()[0]
>>> str(dbm)
'(c.x-c.y<3 & c.y<=7)'

bound(i: int | str, j: int | str) → int[source]

Return the decoded integer bound at (i, j).

This is the integer part of UDBM’s raw_t encoding. For finite cells it matches the bound printed by to_string() and format_matrix().

Parameters:

i (int or str) – Row index or clock name.
j (int or str) – Column index or clock name.

Returns:

Decoded integer bound.

Return type:

int

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"], name="c")
>>> dbm = (context.x - context.y <= 1).to_dbm_list()[0]
>>> dbm.bound("c.x", "y")
1

property clock_names: tuple

Return the matrix headers including the reference clock 0.

Returns:: Tuple of matrix row and column names.
Return type:: tuple

Example:

>>> from pyudbm import Context
>>> dbm = (Context(["x"], name="c").x <= 1).to_dbm_list()[0]
>>> dbm.clock_names
('0', 'c.x')

property dimension: int

Return the DBM dimension including the reference clock.

For a context with n user clocks, the DBM dimension is n + 1 because index 0 is reserved for the reference clock.

Returns:: Matrix dimension.
Return type:: int

Example:

>>> from pyudbm import Context
>>> dbm = (Context(["x", "y"]).x <= 1).to_dbm_list()[0]
>>> dbm.dimension
3

format_matrix() → str[source]

Return a human-readable table view of the DBM matrix.

The formatted view includes row and column headers, including the reference clock 0.

Returns:: Pretty-printed matrix with row and column headers.
Return type:: str

Example:

>>> from pyudbm import Context
>>> dbm = (Context(["x"]).x <= 1).to_dbm_list()[0]
>>> print(dbm.format_matrix())
     0   x
  0 <=0 <=0
  x <=1 <=0

is_infinity(i: int | str, j: int | str) → bool[source]

Return whether the DBM cell at (i, j) equals < inf.

Parameters:

i (int or str) – Row index or clock name.
j (int or str) – Column index or clock name.

Returns:

True if the matrix cell is the infinity sentinel.

Return type:

bool

Example:

>>> from pyudbm import Context
>>> dbm = (Context(["x", "y"], name="c").x <= 1).to_dbm_list()[0]
>>> dbm.is_infinity("c.y", "x")
True

is_strict(i: int | str, j: int | str) → bool[source]

Return whether the DBM cell at (i, j) is strict.

Parameters:

i (int or str) – Row index or clock name.
j (int or str) – Column index or clock name.

Returns:

True when the encoded inequality is strict.

Return type:

bool

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"], name="c")
>>> dbm = (context.x - context.y < 3).to_dbm_list()[0]
>>> dbm.is_strict("x", "c.y")
True

plot(ax: Any = None, **kwargs: Any) → Any[source]

Plot this DBM through pyudbm.binding.visual.

The import is intentionally lazy so matplotlib stays optional unless plotting is actually requested. For the full parameter list and the exact plotting semantics, see pyudbm.binding.visual.plot_dbm().

Parameters:

ax (Any) – Optional matplotlib axes.
kwargs (Any) – Forwarded plotting keyword arguments.

Returns:

Plot result wrapper from pyudbm.binding.visual.plot_dbm().

Return type:

Any

Clock

class pyudbm.binding.udbm.Clock(context: Context, name: str, index: int)[source]

Symbolic clock inside a Context.

A Clock is the Python name-bearing handle for one user-visible UDBM clock. The underlying DBM still works with integer indices and keeps index 0 reserved for the reference clock x0 = 0. The public attribute dbm_index therefore starts at 1.

Clock instances are the entry point to the DSL. Comparing a clock with an integer does not produce a boolean; instead it builds a Federation containing the corresponding zone:

clock <= n means clock - x0 <= n
clock >= n means x0 - clock <= -n
clock == n is the intersection of both bounds
clock1 - clock2 produces a VariableDifference

The binding intentionally accepts only plain integers for symbolic bounds. This matches the native DBM interface used here and avoids the accidental acceptance of bool values.

Parameters:

context (Context) – Owning clock context.
name (str) – Clock name inside the context.
index (int) – Zero-based clock index inside the context.

Variables:

context – The owning context.
index – Zero-based user index inside Context.clocks.
name – User-visible clock name.
dbm_index – Native DBM index, shifted by one because UDBM keeps index 0 for the reference clock.

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"], name="c")
>>> context.x.get_full_name()
'c.x'
>>> str(context.x < 10)
'(c.x<10)'
>>> (context.x == 3) <= (context.x <= 3)
True
>>> (context.x - context.y <= 2) == (context.y - context.x >= -2)
True

__eq__(bound: Any) → Any[source]

Build equality to a constant, or compare clock identity otherwise.

With an integer operand this returns the zone clock == bound. With any non-integer operand it falls back to normal Python object identity.

Parameters:: bound (Any) – Integer bound or arbitrary object.
Returns:: Constraint federation or boolean identity result.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> str(context.x == 2)
'(x==2)'
>>> context.x == context["x"]
True

__ge__(bound: Any) → Any[source]

Build the non-strict lower-bound constraint clock >= bound.

Parameters:: bound (Any) – Integer lower bound.
Returns:: Federation representing the constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> str(context.x >= 2)
'(2<=x)'

__gt__(bound: Any) → Any[source]

Build the strict lower-bound constraint clock > bound.

Parameters:: bound (Any) – Integer lower bound.
Returns:: Federation representing the strict constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> str(context.x > 2)
'(2<x)'

__hash__() → int[source]

Return the hash derived from the fully-qualified clock name.

Returns:: Hash value.
Return type:: int

Example:

>>> from pyudbm import Context
>>> context = Context(["x"], name="c")
>>> hash(context.x) == hash(context.x.get_full_name())
True

__init__(context: Context, name: str, index: int)[source]

Initialize one clock object inside a context.

The constructor is normally called by Context while it creates the declared clock set. index is the user-clock position, while the derived dbm_index is shifted by one because UDBM reserves DBM index 0 for the reference clock.

Parameters:

context (Context) – Owning context.
name (str) – User-visible clock name.
index (int) – Zero-based user-clock index.

Returns:

None.

Return type:

None

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> context.x.index
0
>>> context.x.dbm_index
1

__le__(bound: Any) → Any[source]

Build the non-strict upper-bound constraint clock <= bound.

Parameters:: bound (Any) – Integer upper bound.
Returns:: Federation representing the constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> str(context.x <= 2)
'(x<=2)'

__lt__(bound: Any) → Any[source]

Build the strict upper-bound constraint clock < bound.

Parameters:: bound (Any) – Integer upper bound.
Returns:: Federation representing the strict constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> str(context.x < 2)
'(x<2)'

__ne__(bound: Any) → Any[source]

Build disequality to a constant, or compare identity otherwise.

With an integer operand the result is the union clock < bound or clock > bound. With non-integer operands this is the negation of __eq__().

Parameters:: bound (Any) – Integer bound or arbitrary object.
Returns:: Constraint federation or boolean identity result.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> str(context.x != 2)
'(2<x) | (x<2)'
>>> context.x != context["x"]
False

__repr__() → str[source]

Return a debugging representation of the clock.

Returns:: Representation containing the fully-qualified name.
Return type:: str

Example:

>>> from pyudbm import Context
>>> context = Context(["x"], name="c")
>>> repr(context.x)
'<Clock c.x>'

__sub__(other: Any) → VariableDifference[source]

Build a symbolic difference between two clocks.

The result is a VariableDifference, not a numeric value. Both clocks must belong to the same context because UDBM diagonal constraints are context-local.

Parameters:: other (Any) – Right-hand clock.
Returns:: Symbolic clock difference.
Return type:: VariableDifference
Raises:: ValueError – If the clocks come from different contexts.

Example:

>>> from pyudbm import Context, VariableDifference
>>> context = Context(["x", "y"])
>>> isinstance(context.x - context.y, VariableDifference)
True

get_full_name() → str[source]

Return the fully-qualified clock name.

If the parent context has a display name, the result uses the context.clock form that UDBM string rendering expects. Otherwise the raw clock name is returned unchanged.

Returns:: Context-qualified clock name when a context name is present.
Return type:: str

Example:

>>> from pyudbm import Context
>>> named = Context(["x"], name="sys")
>>> anonymous = Context(["x"])
>>> named.x.get_full_name()
'sys.x'
>>> anonymous.x.get_full_name()
'x'

Valuation

class pyudbm.binding.udbm.Valuation(context: Context)[source]

Clock valuation base class.

UDBM membership tests are performed against concrete valuations. This class stores such valuations as a mapping from Clock objects to concrete numeric values, while also accepting clock names on assignment for convenience.

The base class only normalizes keys and tracks context consistency; it does not restrict the value type. For membership checks through Federation.contains(), use IntValuation or FloatValuation, which match the two native containment entry points.

Parameters:: context (Context) – Owning clock context.
Variables:: context – The context that defines the allowed clock keys.

Example:

>>> from pyudbm import Context, Valuation
>>> context = Context(["x", "y"])
>>> valuation = Valuation(context)
>>> valuation["x"] = 1
>>> valuation[context.y] = 2
>>> valuation[context.x]
1
>>> valuation[context.y]
2

__init__(context: Context)[source]

Initialize an empty valuation for one context.

Parameters:: context (Context) – Owning context.
Returns:: None.
Return type:: None

Example:

>>> from pyudbm import Context, Valuation
>>> valuation = Valuation(Context(["x"]))
>>> len(valuation)
0

__setitem__(key: str | Clock, value: Any) → None[source]

Store a value using either a clock name or a Clock key.

Parameters:

key (str or Clock) – Clock name or clock object.
value (Any) – Concrete clock value.

Returns:

None.

Return type:

None

Example:

>>> from pyudbm import Context, Valuation
>>> context = Context(["x", "y"])
>>> valuation = Valuation(context)
>>> valuation["x"] = 1
>>> valuation[context.y] = 2
>>> valuation[context.x], valuation[context.y]
(1, 2)

check() → None[source]

Check whether all clocks of the context have assigned values.

The method does not raise. For historical compatibility, missing entries are reported through the pyudbm logger instead. This is primarily useful before calling Federation.contains(), where a partial valuation would otherwise fail later when translated into a native point vector.

Returns:: None.
Return type:: None

Example:

>>> from pyudbm import Context, Valuation
>>> context = Context(["x", "y"])
>>> valuation = Valuation(context)
>>> valuation["x"] = 1
>>> valuation["y"] = 2
>>> valuation.check() is None
True

IntValuation

class pyudbm.binding.udbm.IntValuation(context: Context)[source]

Integer clock valuation.

This specialization matches UDBM’s integer containment check. It accepts only plain int values and rejects bool for the same reason as the symbolic constraint layer.

Parameters:: context (Context) – Owning clock context.

Example:

>>> from pyudbm import Context, IntValuation
>>> context = Context(["x", "y"])
>>> valuation = IntValuation(context)
>>> valuation["x"] = 3
>>> valuation["y"] = 1
>>> ((context.x == 3) & (context.y == 1)).contains(valuation)
True

__setitem__(key: str | Clock, value: Any) → None[source]

Store one integer-valued clock assignment.

Parameters:

key (str or Clock) – Clock name or clock object.
value (Any) – Integer value to assign.

Returns:

None.

Return type:

None

Raises:

TypeError – If value is not a plain integer.

Example:

>>> from pyudbm import Context, IntValuation
>>> valuation = IntValuation(Context(["x"]))
>>> valuation["x"] = 3
>>> valuation[valuation.context.x]
3

FloatValuation

class pyudbm.binding.udbm.FloatValuation(context: Context)[source]

Floating-point clock valuation.

This specialization targets UDBM’s real-valued point inclusion test. It accepts both integers and floating-point numbers and is the right choice when strict inequalities make the difference between integer and real membership observable.

Parameters:: context (Context) – Owning clock context.

Example:

>>> from pyudbm import Context, FloatValuation
>>> context = Context(["x"])
>>> valuation = FloatValuation(context)
>>> valuation["x"] = 1.5
>>> (context.x > 1).contains(valuation)
True
>>> (context.x == 1).contains(valuation)
False

__setitem__(key: str | Clock, value: Any) → None[source]

Store one real-valued clock assignment.

Parameters:

key (str or Clock) – Clock name or clock object.
value (Any) – Integer or floating-point value.

Returns:

None.

Return type:

None

Raises:

TypeError – If value is neither int nor float.

Example:

>>> from pyudbm import Context, FloatValuation
>>> valuation = FloatValuation(Context(["x"]))
>>> valuation["x"] = 1.5
>>> valuation[valuation.context.x]
1.5

VariableDifference

class pyudbm.binding.udbm.VariableDifference(variables: List[Clock])[source]

Symbolic difference between two clocks.

This lightweight helper represents the symbolic expression x - y for two clocks in the same context. Comparing the difference with an integer creates a Federation whose DBM contains the corresponding diagonal constraint x - y <= c or its strict / reversed variants.

In timed-automata terms, this is how diagonal constraints are expressed in the Python DSL.

Parameters:

variables (list[Clock]) – Two clocks from the same context.

Variables:

vars – The two clocks in [left, right] order.
context – Shared context of both clocks.

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> diagonal = context.x - context.y
>>> (diagonal <= 3) == (context.y - context.x >= -3)
True
>>> str(diagonal == 1)
'(1<=x & x-y==1)'
>>> (diagonal == 1) == ((context.x - context.y) == 1)
True

__eq__(bound: Any) → Any[source]

Build the equality zone left - right == bound.

Parameters:: bound (Any) – Integer difference value.
Returns:: Federation representing the equality, or False for non-integer operands.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> str(context.x - context.y == 2)
'(2<=x & x-y==2)'

__ge__(bound: Any) → Any[source]

Build the diagonal constraint left - right >= bound.

Parameters:: bound (Any) – Integer lower bound.
Returns:: Federation representing the diagonal constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> str(context.x - context.y >= 2)
'(y-x<=-2)'

__gt__(bound: Any) → Any[source]

Build the strict diagonal constraint left - right > bound.

Parameters:: bound (Any) – Integer lower bound.
Returns:: Federation representing the diagonal constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> str(context.x - context.y > 2)
'(y-x<-2)'

__init__(variables: List[Clock])[source]

Initialize a symbolic difference left - right.

Parameters:: variables (List[Clock]) – Exactly two clocks from the same context.
Returns:: None.
Return type:: None
Raises:: ValueError – If the input does not contain exactly two compatible clocks.

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> difference = context.x - context.y
>>> [clock.name for clock in difference.vars]
['x', 'y']

__le__(bound: Any) → Any[source]

Build the diagonal constraint left - right <= bound.

Parameters:: bound (Any) – Integer upper bound.
Returns:: Federation representing the diagonal constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> str(context.x - context.y <= 2)
'(x-y<=2)'

__lt__(bound: Any) → Any[source]

Build the strict diagonal constraint left - right < bound.

Parameters:: bound (Any) – Integer upper bound.
Returns:: Federation representing the diagonal constraint.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> str(context.x - context.y < 2)
'(x-y<2)'

__ne__(bound: Any) → Any[source]

Build the disequality zone left - right != bound.

Parameters:: bound (Any) – Integer difference value.
Returns:: Federation representing the disequality, or True for non-integer operands.
Return type:: Any

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> str(context.x - context.y != 2)
'(y-x<-2) | (x-y<2)'

Constraint

class pyudbm.binding.udbm.Constraint(arg1: Clock | None, arg2: Clock | None, val: int, is_strict: bool)[source]

Internal symbolic constraint wrapper.

This class is the immediate bridge between the Python DSL and the native UDBM constraint_t representation. It stores one encoded difference constraint of the form arg1 - arg2 <= val together with strictness.

End users usually create Constraint objects implicitly through Clock and VariableDifference expressions, but the class remains public because it is part of the historical high-level surface and is used directly by Federation.

Parameters:

arg1 (Clock or None) – Left clock operand, or None for the reference clock.
arg2 (Clock or None) – Right clock operand, or None for the reference clock.
val (int) – Integer bound.
is_strict (bool) – Whether the bound is strict.

Variables:

arg1 – Left clock operand, or None for the reference clock.
arg2 – Right clock operand, or None for the reference clock.
context – Context owning the participating clocks.

Example:

>>> from pyudbm import Constraint, Context, Federation
>>> context = Context(["x", "y"])
>>> constraint = Constraint(context.x, context.y, 3, False)
>>> zone = Federation(constraint)
>>> zone == (context.x - context.y <= 3)
True

__init__(arg1: Clock | None, arg2: Clock | None, val: int, is_strict: bool)[source]

Initialize one symbolic DBM constraint wrapper.

Parameters:

arg1 (Clock or None) – Left clock operand, or None for the reference clock.
arg2 (Clock or None) – Right clock operand, or None for the reference clock.
val (int) – Integer bound.
is_strict (bool) – Whether the bound is strict.

Returns:

None.

Return type:

None

Raises:

TypeError – If operands or the bound have invalid types.
ValueError – If no operand is given or the clocks belong to different contexts.

Example:

>>> from pyudbm import Constraint, Context
>>> context = Context(["x", "y"])
>>> constraint = Constraint(context.x, context.y, 3, False)
>>> constraint.context is context
True

Federation

class pyudbm.binding.udbm.Federation(arg: Context | Constraint)[source]

Union of DBMs within a single Context.

A federation is the core symbolic set object of UDBM. Each element of the union is one DBM, that is, one convex zone over the clocks of the context. Federations are therefore the natural representation for non-convex timed states.

This Python wrapper keeps the algebra close to the underlying library:

& is exact intersection;
| is set union;
+ is convex union, meaning pairwise DBM hull construction rather than plain set union;
- is set subtraction;
comparisons implement set inclusion semantics.

Mutability follows the historical binding rather than a pure in-place API:

reduce(), set_zero(), set_init(), and intern() mutate the object and return self (or None for intern);
methods such as up(), down(), free_clock(), convex_hull(), predt(), update_value(), reset_value(), and extrapolate_max_bounds() return a modified copy and leave the original federation untouched.

The constructor mirrors the historical binding: creating from a Context yields the zero federation, while creating from a Constraint yields the initial federation constrained by that symbolic expression.

Parameters:: arg (Context or Constraint) – Context or symbolic constraint source.
Variables:: context – Context shared by every DBM in the federation.

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"], name="c")
>>> d1 = (context.x >= 1) & (context.x <= 2)
>>> d2 = (context.y >= 3) & (context.y <= 4)
>>> union = d1 | d2
>>> hull = d1 + d2
>>> union.get_size()
2
>>> hull >= d1
True
>>> hull >= d2
True

__add__(other: Federation) → Federation[source]

Return the convex union of two federations.

Unlike __or__(), this computes UDBM’s convex-hull style addition and may introduce new valuations between the operands.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: Convex union result.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> hull = (context.x == 0) + (context.x == 2)
>>> hull == ((context.x >= 0) & (context.x <= 2))
True

__and__(other: Federation) → Federation[source]

Return the exact intersection of two federations.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: Intersection result.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> left = context.x >= 1
>>> right = context.x <= 3
>>> (left & right) == ((context.x >= 1) & (context.x <= 3))
True

__eq__(other: Any) → bool[source]

Return whether two federations denote the same symbolic set.

Parameters:: other (Any) – Object to compare with.
Returns:: True if both federations are equal.
Return type:: bool

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> (context.x == 1) == ((context.x <= 1) & (context.x >= 1))
True

__ge__(other: Federation) → bool[source]

Return whether self is a superset of other.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: True if reverse inclusion holds.
Return type:: bool

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> (context.x <= 1) >= (context.x == 1)
True

__gt__(other: Federation) → bool[source]

Return whether self is a strict superset of other.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: True if strict reverse inclusion holds.
Return type:: bool

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> (context.x <= 1) > (context.x == 1)
True

__hash__() → int[source]

Return the native order-insensitive federation hash.

Returns:: Hash value.
Return type:: int

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> left = (context.x == 1) | (context.y == 1)
>>> right = (context.y == 1) | (context.x == 1)
>>> hash(left) == hash(right)
True

__iadd__(other: Federation) → Federation[source]

Replace this federation by its convex union with another one.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: self after convex union.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> zone = context.x == 0
>>> zone += (context.x == 2)
>>> zone == ((context.x >= 0) & (context.x <= 2))
True

__iand__(other: Federation) → Federation[source]

Intersect this federation with another one in place.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: self after intersection.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> zone = context.x >= 1
>>> zone &= (context.x <= 3)
>>> zone == ((context.x >= 1) & (context.x <= 3))
True

__init__(arg: Context | Constraint)[source]

Initialize a federation from a context or one constraint.

Passing a Context creates that context’s zero federation. Passing a Constraint creates a one-DBM federation containing the corresponding symbolic zone.

Parameters:: arg (Context or Constraint) – Context or constraint source.
Returns:: None.
Return type:: None
Raises:: TypeError – If arg is neither a context nor a constraint.

Example:

>>> from pyudbm import Constraint, Context, Federation
>>> context = Context(["x"])
>>> Federation(context).is_zero()
True
>>> Federation(Constraint(context.x, None, 2, False)) == (context.x <= 2)
True

__ior__(other: Federation) → Federation[source]

Union this federation with another one in place.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: self after union.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> zone = context.x == 0
>>> zone |= (context.x == 1)
>>> zone.get_size()
2

__isub__(other: Federation) → Federation[source]

Subtract another federation from this one in place.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: self after subtraction.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> zone = (context.x >= 0) & (context.x <= 2)
>>> zone -= (context.x == 1)
>>> zone == (((context.x >= 0) & (context.x < 1)) | ((context.x > 1) & (context.x <= 2)))
True

__le__(other: Federation) → bool[source]

Return whether self is a subset of other.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: True if inclusion holds.
Return type:: bool

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> (context.x == 1) <= (context.x <= 1)
True

__lt__(other: Federation) → bool[source]

Return whether self is a strict subset of other.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: True if strict inclusion holds.
Return type:: bool

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> (context.x == 1) < (context.x <= 1)
True

__ne__(other: Any) → bool[source]

Return whether two federations denote different symbolic sets.

Parameters:: other (Any) – Object to compare with.
Returns:: True if the federations differ.
Return type:: bool

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> (context.x == 1) != (context.x == 2)
True

__or__(other: Federation) → Federation[source]

Return the set-theoretic union of two federations.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: Union result.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> union = (context.x == 0) | (context.x == 1)
>>> union.get_size()
2

__str__() → str[source]

Return UDBM-style textual rendering of the federation.

Returns:: Human-readable symbolic zone expression.
Return type:: str

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> str(context.x < 2)
'(x<2)'

__sub__(other: Federation) → Federation[source]

Return the set difference self \ other.

Parameters:: other (Federation) – Other federation in the same context.
Returns:: Difference result.
Return type:: Federation

Example:

>>> from pyudbm import Context, IntValuation
>>> context = Context(["x"])
>>> zone = ((context.x >= 0) & (context.x <= 2)) - (context.x == 1)
>>> kept = IntValuation(context)
>>> kept["x"] = 0
>>> removed = IntValuation(context)
>>> removed["x"] = 1
>>> zone.contains(kept), zone.contains(removed)
(True, False)

contains(valuation: Valuation) → bool[source]

Test whether a concrete valuation belongs to the federation.

The valuation must cover every clock of the context. Integer and floating-point valuations are dispatched to the corresponding native UDBM containment check.

Parameters:: valuation (Valuation) – Concrete clock values.
Returns:: True if the valuation is contained in at least one DBM.
Return type:: bool

Example:

>>> from pyudbm import Context, IntValuation
>>> context = Context(["x", "y"])
>>> zone = (context.x == 2) & (context.y == 1)
>>> valuation = IntValuation(context)
>>> valuation["x"] = 2
>>> valuation["y"] = 1
>>> zone.contains(valuation)
True

convex_hull() → Federation[source]

Return the convex hull of the federation.

UDBM computes the convex union of all DBMs in the federation, yielding one convex over-approximation zone.

Returns:: A convex-hull copy.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> d1 = (context.x >= 1) & (context.x <= 2) & (context.y >= 1) & (context.y <= 2)
>>> d2 = (context.x >= 3) & (context.x <= 4) & (context.y >= 3) & (context.y <= 4)
>>> hull = (context.x - context.y <= 1) & (context.y - context.x <= 1)
>>> hull &= (context.x >= 1) & (context.y >= 1) & (context.x <= 4) & (context.y <= 4)
>>> (d1 | d2).convex_hull() == hull
True

copy() → Federation[source]

Return a copy of the federation.

The copy shares the same Context but owns an independent native federation value.

Returns:: A copy sharing the same context.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> original = (context.x == 1)
>>> copied = original.copy()
>>> copied |= (context.y == 2)
>>> original != copied
True
>>> original == (context.x == 1)
True

down() → Federation[source]

Compute the inverse delay predecessor of the federation.

This is the standard weakest pre-condition for time elapse: lower bounds are relaxed so that delaying can lead into the current zone.

Returns:: A predecessor copy of the federation.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> zone = (context.x >= 1) & (context.x <= 2) & (context.y >= 1) & (context.y <= 2)
>>> expected = (context.x - context.y <= 1) & (context.y - context.x <= 1) & (context.x <= 2) & (context.y <= 2)
>>> zone.down() == expected
True

extrapolate_max_bounds(bounds: Mapping[str | Clock, int]) → Federation[source]

Return a maximal-bound extrapolation of the federation.

This is the classical DBM k-normalization described in UDBM as extrapolateMaxBounds. For each DBM, constraints above the maximal constant of their source clock are dropped to infinity, while very low lower bounds are clamped to the negated maximal constant of the target clock. The operation preserves closure but may over-approximate the original zone.

The Python wrapper accepts a mapping keyed either by Clock objects or by clock names. Bounds must be provided for every clock in the context.

Parameters:: bounds (Mapping[str or Clock, int]) – Maximal constants for every user clock.
Returns:: Extrapolated copy of the federation.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y", "z"])
>>> federation = (context.x - context.y <= 1) & (context.x < 150)
>>> federation &= (context.z < 150) & (context.x - context.z <= 1000)
>>> bounds = {context.x: 100, context.y: 300, context.z: 400}
>>> federation.extrapolate_max_bounds(bounds) == ((context.x - context.y <= 1) & (context.z < 150))
True

free_clock(clock: Clock) → Federation[source]

Return a copy where one clock has been unconstrained.

UDBM’s freeClock removes both upper and lower bounds involving the given clock, while still preserving the ambient positivity convention inherited from the reference clock.

Parameters:: clock (Clock) – Clock to unconstrain.
Returns:: A modified copy with the clock freed.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> zone = (context.x >= 10) & (context.y >= 10)
>>> zone.free_clock(context.x) == (context.y >= 10)
True
>>> zone == ((context.x >= 10) & (context.y >= 10))
True

get_size() → int[source]

Return the number of DBMs currently stored in the federation.

This is the exact native federation size, not the number of visible clock constraints.

Returns:: Number of DBMs.
Return type:: int

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> federation = (context.x == 0) | (context.x == 1)
>>> federation.get_size()
2

has_zero() → bool[source]

Return whether the federation contains the origin.

The origin is the valuation where every user clock is 0. This is a cheap and common query in timed-automata algorithms.

Returns:: True if the origin is included.
Return type:: bool

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> (context.x < 1).has_zero()
True
>>> (context.x > 1).has_zero()
False

hash() → int[source]

Return the Python hash of the federation.

The underlying native hash is designed to be insensitive to DBM order. The Python wrapper exposes it through hash() and this convenience method.

Returns:: Hash value.
Return type:: int

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> left = (context.x == 1) | (context.y == 1)
>>> right = (context.y == 1) | (context.x == 1)
>>> left.hash() == right.hash()
True

intern() → None[source]

Intern the native DBMs backing this federation.

UDBM can canonicalize identical DBMs through internal hash tables. Calling intern() is therefore a memory and equality-optimization hint rather than a semantic transformation.

Returns:: None.
Return type:: None

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> federation = context.x - context.y <= 1
>>> before = federation.copy()
>>> federation.intern() is None
True
>>> federation == before
True

is_empty() → bool[source]

Return whether the federation contains no valuations.

Returns:: True if the federation is empty.
Return type:: bool

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> ((context.x == 1) & (context.x != 1)).is_empty()
True
>>> (context.x == 1).is_empty()
False

is_zero() → bool[source]

Return whether the federation is exactly the origin zone.

This is stronger than has_zero(): the whole federation must equal the zero federation of its context.

Returns:: True if the federation equals the origin zone.
Return type:: bool

Example:

>>> from pyudbm import Context, Federation
>>> context = Context(["x"])
>>> Federation(context).is_zero()
True
>>> (context.x == 1).is_zero()
False

plot(ax: Any = None, **kwargs: Any) → Any[source]

Plot this federation through pyudbm.binding.visual.

The import is intentionally lazy so matplotlib stays optional unless plotting is actually requested. For the full parameter list and the exact plotting semantics, see pyudbm.binding.visual.plot_federation().

Parameters:

ax (Any) – Optional matplotlib axes.
kwargs (Any) – Forwarded plotting keyword arguments.

Returns:

Plot result wrapper from pyudbm.binding.visual.plot_federation().

Return type:

Any

Context

class pyudbm.binding.udbm.Context(clock_names: Iterable[str], name: str | None = None)[source]

Named clock context.

A context owns the finite set of clocks manipulated together by UDBM. All Clock, Valuation, VariableDifference, and Federation objects are context-specific, and almost every binary operation requires the same context on both sides.

Each declared clock is available in two ways:

as an attribute, for example context.x;
through name lookup, for example context["x"].

Attribute access is convenient for normal modeling code, while indexed lookup keeps working even when a clock name would shadow an existing attribute.

Parameters:

clock_names (iterable[str]) – Clock names to create.
name (str or None) – Optional context prefix used in string rendering.

Variables:

clocks – List of clocks in declaration order.
name – Optional display prefix used by Clock.get_full_name().

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"], name="c")
>>> context.x is context["x"]
True
>>> context.y.get_full_name()
'c.y'
>>> context.get_zero_federation().is_zero()
True

__getitem__(arg: str) → Clock[source]

Return one clock by its declared name.

Parameters:: arg (str) – Clock name.
Returns:: Matching clock object.
Return type:: Clock
Raises:: KeyError – If no unique clock with that name exists.

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> context["x"] is context.x
True

__init__(clock_names: Iterable[str], name: str | None = None)[source]

Initialize a context and create all declared clocks.

Parameters:

clock_names (Iterable[str]) – Names of clocks to create.
name (str or None) – Optional display prefix.

Returns:

None.

Return type:

None

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"], name="c")
>>> [clock.name for clock in context.clocks]
['x', 'y']
>>> context.name
'c'

get_zero_federation() → Federation[source]

Return the zero federation for this context.

The zero federation contains exactly the origin valuation where all clocks are equal to 0.

Returns:: Zero federation.
Return type:: Federation

Example:

>>> from pyudbm import Context
>>> context = Context(["x", "y"])
>>> zero = context.get_zero_federation()
>>> zero.is_zero()
True
>>> zero.has_zero()
True

set_name(name: str | None) → None[source]

Set the context display name.

The display name affects only string rendering and derived clock full names. It does not change DBM identities or context compatibility.

Parameters:: name (str or None) – New context name.
Returns:: None.
Return type:: None

Example:

>>> from pyudbm import Context
>>> context = Context(["x"])
>>> context.set_name("renamed")
>>> context.x.get_full_name()
'renamed.x'

to_cdd_context(bools: Iterable[str] = (), name: str | None = None) → Any[source]

Build a pyudbm.binding.ucdd.CDDContext from this clock context.

The resulting CDD context preserves the current clock order so that Federation and DBM objects from this context can be converted without remapping.

Parameters:

bools (Iterable[str]) – Optional boolean variable names to add.
name (str or None) – Optional display-name override.

Returns:

Matching CDD context.

Return type:

Any

pyudbm.binding.udbm

__all__

LOGGER

DBM

Clock

Valuation

IntValuation

FloatValuation

VariableDifference

Constraint

Federation

Context

all