stormvogel.parametric.region¶

Rectangular parameter regions and the induced interval MDP transformation.

Attributes¶

`_DEFAULT_REGION_COLORS`
`_EXTRA_COLORS`

Classes¶

`AnnotatedRegion`	A rectangular region with interval bounds on its minimum and maximum property value.
`RectangularRegion`	A rectangular parameter region: a Cartesian product of closed intervals.

Functions¶

`_unique_transition_values`(→ set)
`_unique_reward_values`(→ set)
`_to_number`(→ stormvogel.parametric._backend.Number)
`_affine_image`(...)	Return `(min, max)` of an affine sympy expression over region.
`to_interval_mdp`(→ stormvogel.model.Model)	Return the interval MDP induced by pmdp and a rectangular region.
`_draw_solution_isoline`(→ list)	Draw the isoline `solution_fn == threshold` on ax.
`plot_regions`(→ matplotlib.axes.Axes)	Plot a 2D partition of rectangular regions as colored patches.
`plot_annotated_regions`(→ matplotlib.axes.Axes)
`plot_annotated_regions_1d`(→ matplotlib.axes.Axes)	Plot 1-parameter annotated regions as value bands on a 2D axis.

Module Contents¶

class stormvogel.parametric.region.AnnotatedRegion¶

A rectangular region with interval bounds on its minimum and maximum property value.

Parameters:

region – The underlying rectangular parameter region.
min_value – (lo, hi) interval for the minimum property value over region.
max_value – (lo, hi) interval for the maximum property value over region.

region: RectangularRegion¶

min_value: tuple[stormvogel.parametric._backend.Number, stormvogel.parametric._backend.Number]¶

max_value: tuple[stormvogel.parametric._backend.Number, stormvogel.parametric._backend.Number]¶

__post_init__() → None¶

classify(threshold: stormvogel.parametric._backend.Number) → str¶

Return "safe", "unsafe", "neither", or "unknown" relative to threshold.

"safe": min_value[0] >= threshold — every instantiation is ≥ threshold.
"unsafe": max_value[1] < threshold — every instantiation is < threshold.
"neither": max_value[0] >= threshold and min_value[1] < threshold — the region certifiably straddles the threshold (some instantiations above, some below).
"unknown": otherwise — not enough information to classify.

class stormvogel.parametric.region.RectangularRegion¶

A rectangular parameter region: a Cartesian product of closed intervals.

Parameters:: bounds – Mapping from parameter name to (lower, upper) bound. Bounds can be any Number.

bounds: dict[str, tuple[stormvogel.parametric._backend.Number, stormvogel.parametric._backend.Number]]¶

__post_init__() → None¶

contains(valuation: dict[str, stormvogel.parametric._backend.Number]) → bool¶: Return True iff valuation lies inside every interval.

vertices() → list[dict[str, stormvogel.parametric._backend.Number]]¶: Return all 2^n corner points of the region.

split(param: str | None = None) → tuple[RectangularRegion, RectangularRegion]¶

Split the region into two equal halves at the midpoint of param.

If param is None the dimension with the largest range is chosen.

Parameters:: param – Parameter name to split along.
Returns:: Pair (lower_half, upper_half) whose union is this region.
Raises:: ValueError – If param is not present in this region.

is_well_defined(model: RectangularRegion.is_well_defined.model) → bool¶

Return True iff the region is well-defined for model.

A region is well-defined if every transition probability lies in [0, 1], every reward is non-negative for all instantiations within the region, and the probabilities of every choice sum to exactly 1 as a formal identity. Requires an affine parametric model.

For non-parametric models, the check basically asks whether the model is stochastic.

is_graph_preserving(model: RectangularRegion.is_graph_preserving.model) → bool¶

Return True iff the region is graph-preserving for model.

A well-defined region is graph-preserving if no transition probability evaluates to 0 for any instantiation within the region. Regions that are not-welldefined are not graph-preserving. Requires an affine parametric model.

__repr__() → str¶

stormvogel.parametric.region._unique_transition_values(model: _unique_transition_values.model) → set¶

stormvogel.parametric.region._unique_reward_values(model: _unique_reward_values.model) → set¶

stormvogel.parametric.region._to_number(x: sympy.Expr) → stormvogel.parametric._backend.Number¶

stormvogel.parametric.region._affine_image(expr: sympy.Expr, region: RectangularRegion) → tuple[stormvogel.parametric._backend.Number, stormvogel.parametric._backend.Number]¶

Return (min, max) of an affine sympy expression over region.

For each parameter x with coefficient c, the minimum uses the lower bound when c ≥ 0 and the upper bound when c < 0 (and vice-versa for the maximum).

Raises:: ValueError – If expr has total degree > 1, or a free symbol is absent from region.

stormvogel.parametric.region.to_interval_mdp(pmdp: stormvogel.model.Model, region: RectangularRegion) → stormvogel.model.Model¶

Return the interval MDP induced by pmdp and a rectangular region.

Each parametric transition probability (which must be affine in the parameters) is replaced by the interval [min, max] of its image over region. Non-parametric probabilities become point intervals [p, p].

Uses copy() to preserve state UUIDs, so the returned model can be cross-referenced with the original via get_state_by_id.

Parameters:

pmdp – A parametric stormvogel model.
region – A rectangular region covering all parameters in pmdp.

Returns:

A new stormvogel model with Interval transition probabilities.

Raises:

ValueError – If any transition probability is not affine, or if a parameter is absent from region.

stormvogel.parametric.region._DEFAULT_REGION_COLORS: dict[str, str]¶

stormvogel.parametric.region._EXTRA_COLORS = ['#5b9bd5', '#ed7d31', '#a9d18e', '#ffc000']¶

stormvogel.parametric.region._draw_solution_isoline(ax: matplotlib.axes.Axes, solution_fn, threshold: stormvogel.parametric._backend.Number, x_param: str, y_param: str, x_lim: tuple[float, float], y_lim: tuple[float, float], resolution: int, shade_safe: bool = False) → list¶

Draw the isoline solution_fn == threshold on ax.

solution_fn may be a sympy expression with free symbols matching x_param and y_param, or any callable (x_val, y_val) -> float that accepts the x and y values as positional arguments.

When shade_safe is True, the region where solution_fn >= threshold is filled with a semi-transparent green overlay.

Returns a list of legend proxy artists that the caller should pass to ax.legend().

stormvogel.parametric.region.plot_regions(regions: list[tuple[RectangularRegion, str] | AnnotatedRegion], ax: Axes | None = None, figsize: tuple[float, float] | None = None, colors: dict[str, str] | None = None, param_order: tuple[str, str] | None = None, solution_fn=None, threshold: Number | None = None, resolution: int = 200, shade_safe: bool = False, x_lim: tuple[float, float] | None = None, y_lim: tuple[float, float] | None = None) → matplotlib.axes.Axes¶

Plot a 2D partition of rectangular regions as colored patches.

Each (region, label) pair is rendered as a filled rectangle, similar to the region plots produced by prophesy. The default color mapping is "safe" → green, "unsafe" → red, "unknown" → gray; override or extend via colors.

An optional solution-function isoline can be overlaid by supplying both solution_fn and threshold: the curve where solution_fn == threshold is drawn as a dashed black line. Set shade_safe to True to also fill the region where solution_fn >= threshold with a semi-transparent green overlay.

regions may be empty; in that case param_order is required and the axis limits default to (0, 1) unless x_lim / y_lim are given explicitly.

Parameters:

regions – List of (region, label) pairs or AnnotatedRegion objects to plot. When AnnotatedRegion objects are given, threshold is required for classification.
ax – Target axes; creates a new figure if None.
figsize – Figure size in inches as (width, height). Ignored when ax is provided.
colors – Mapping from label to matplotlib color string, merged with the defaults.
param_order – (x_param, y_param) to control axis assignment. Defaults to the insertion order of the first region’s bounds. Required when regions is empty.
solution_fn – A sympy expression or callable (x, y) -> float representing the solution function. Requires threshold when given.
threshold – The threshold value to draw the isoline at. Required when solution_fn is provided.
resolution – Number of grid points per axis for isoline evaluation.
shade_safe – When True, fill the region where solution_fn >= threshold with a semi-transparent green overlay. Requires solution_fn and threshold.
x_lim – Override the x-axis range as (lo, hi). Defaults to the range spanned by regions, or (0, 1) when regions is empty.
y_lim – Override the y-axis range as (lo, hi). Same default logic as x_lim.

Raises:

ValueError – If any region does not have exactly 2 parameters, a param_order name is absent from the region bounds, param_order is omitted when regions is empty, or solution_fn is given without threshold.

stormvogel.parametric.region.plot_annotated_regions(regions: list[AnnotatedRegion], threshold: stormvogel.parametric._backend.Number, ax: Axes | None = None, figsize: tuple[float, float] | None = None, colors: dict[str, str] | None = None, param_order: tuple[str, str] | None = None, solution_fn=None, resolution: int = 200, shade_safe: bool = False, x_lim: tuple[float, float] | None = None, y_lim: tuple[float, float] | None = None) → matplotlib.axes.Axes¶: Deprecated since version Use: plot_regions() with AnnotatedRegion objects instead.

stormvogel.parametric.region.plot_annotated_regions_1d(regions: list[AnnotatedRegion], threshold: stormvogel.parametric._backend.Number, ax: Axes | None = None, figsize: tuple[float, float] | None = None, colors: dict[str, str] | None = None, solution_fn=None, resolution: int = 500) → matplotlib.axes.Axes¶

Plot 1-parameter annotated regions as value bands on a 2D axis.

The x-axis is the single parameter; the y-axis is the property value. Each annotated region [x_lo, x_hi] is drawn as two nested shaded rectangles:

outer band [lo_min, hi_max] (alpha 0.25): the full uncertainty range — the property value is guaranteed to lie here for all instantiations in the region.
inner band [hi_min, lo_max] (alpha 0.55): the tighter verified range, drawn only when hi_min ≤ lo_max.

Both bands are colored by the region’s classification relative to threshold (green/red/orange/gray for safe/unsafe/neither/unknown). A horizontal dashed line marks threshold on the value axis.

If solution_fn is provided — a sympy expression in the single parameter symbol, or a callable (x_val) -> float — its graph is overlaid as a solid black curve.

Parameters:

regions – Annotated regions with exactly 1 parameter each.
threshold – Classification threshold, also drawn as a horizontal line.
ax – Target axes; creates a new figure if None.
figsize – Figure size in inches as (width, height). Ignored when ax is provided.
colors – Mapping from classification label to matplotlib color string, merged with the defaults.
solution_fn – A sympy expression or callable (x) -> float.
resolution – Number of x-points for evaluating solution_fn.

Raises:

ValueError – If regions is empty or any region has ≠ 1 parameter.