RegionCheckEngine¶

class RegionCheckEngine(*values)¶

Bases: Enum

Region checking engines, controlling the arithmetic and supported regions.

PARAMETER_LIFTING (default): floating-point computations on the lifted model.
EXACT_PARAMETER_LIFTING: exact rational computations on the lifted model.
VALIDATING_PARAMETER_LIFTING: floating-point computations followed by exact validation of the results.
ROBUST_PARAMETER_LIFTING: floating-point computations using robust models. Supports DTMCs only and allows graph-changing and ill-defined regions.

All engines except ROBUST_PARAMETER_LIFTING require a well-defined, graph-preserving region.

EXACT_PARAMETER_LIFTING = 1¶

PARAMETER_LIFTING = 0¶

ROBUST_PARAMETER_LIFTING = 3¶

VALIDATING_PARAMETER_LIFTING = 2¶