BoundedValue

class BoundedValue(value: Any, lower: Any = None, upper: Any = None)

Bases: object

Value of a single state in a model checking result, together with sound lower and upper bounds on the actual value.

The bounds are given if the solution method could establish them, e.g., for sound methods. An unknown bound is None. An infinite bound means the method tried but could not establish a finite bound.

The object behaves like its value in comparisons with numbers and when converting to float. Addition, subtraction, multiplication and division (with other values and plain numbers, which are exact) keep sound bounds on the result. Division only yields bounds if the bounds of the divisor exclude 0. Infinite values follow the convention 0 * infinity = 0. A bound which is undefined (infinity minus infinity) becomes unknown.

Create a value with bounds.

Parameters:

  • value – The (approximate) value.

  • lower – Sound lower bound on the actual value (None if not known).

  • upper – Sound upper bound on the actual value (None if not known).

property has_lower: bool

Whether a lower bound is known.

property has_upper: bool

Whether an upper bound is known.

property lower: Any

Sound lower bound on the actual value (None if not known).

property upper: Any

Sound upper bound on the actual value (None if not known).

property value: Any

The (approximate) value.