stormvogel.stormpy_utils.parametric_analysis¶

Thin stormpy wrappers for parametric model analysis.

Provides a class that fixes a stormvogel model and a property formula once, then reuses the stormpy model and checkers across repeated queries.

Attributes¶

stormpy

Classes¶

AnalyseParametric

Reusable analysis context for a fixed parametric model and property.

Functions¶

rectangular_region_to_stormpy(...)

Convert a RectangularRegion to a stormpy ParameterRegion.

Module Contents¶

stormvogel.stormpy_utils.parametric_analysis.stormpy = None¶

stormvogel.stormpy_utils.parametric_analysis.rectangular_region_to_stormpy(name_to_var: dict[str, object], region: stormvogel.parametric.region.RectangularRegion) → stormpy.pars.ParameterRegion¶

Convert a RectangularRegion to a stormpy ParameterRegion.

Parameters:

name_to_var – Mapping from parameter name to the corresponding pycarl.Variable object (as returned by AnalyseParametric.name_to_var()).
region – The rectangular region to convert.

Returns:

A stormpy ParameterRegion with the same bounds.

Raises:

KeyError – If a parameter name in region is absent from name_to_var.

class stormvogel.stormpy_utils.parametric_analysis.AnalyseParametric(model: stormvogel.model.Model, prop: str, env: stormpy.Environment | None = None)¶

Reusable analysis context for a fixed parametric model and property.

The stormvogel→stormpy conversion, formula parsing, instantiation checker, and region checker are all created once in the constructor and reused across every query call.

Parameters:

model – A parametric stormvogel model.
prop – A Storm property string, e.g. 'P=? [F "target"]'.
env – A stormpy Environment to use; a fresh default environment is created when None.

Raises:

ImportError – If stormpy is not installed.
ValueError – If model is not parametric.

model¶

_sp_model¶

env: stormpy.Environment¶

_formula¶

_name_to_var: dict[str, object]¶

_instantiation_checker¶

_region_checker¶

property name_to_var: dict[str, object]¶

Mapping from parameter name to pycarl Variable.

Pass this to rectangular_region_to_stormpy() when you need to convert regions outside of this class.

evaluate_at_point(valuation: collections.abc.Mapping[str, stormvogel.parametric._backend.Number]) → float¶

Evaluate the property at a single parameter instantiation.

Parameters:: valuation – Mapping from parameter name to a concrete value.
Returns:: The property value at the initial state as a float.
Raises:: KeyError – If a name in valuation is not a parameter of the model.

TODO: once the instantiation checker also exposes exact rationals, use exact arithmetic here. See https://github.com/stormchecker/stormpy/discussions/389

get_region_bound(region: stormvogel.parametric.region.RectangularRegion, maximize: bool = True, assume_graph_preserving: bool = False) → stormvogel.parametric._backend.Number¶

Return the optimistic bound on the property value over region.

Calls RegionChecker.get_bound; the result is an upper bound when maximize is True and a lower bound when False.

The bound is returned as an exact Fraction derived from the rational number produced by stormpy’s region checker.

Parameters:

region – A rectangular parameter region. Must be graph-preserving for model.
maximize – True to get an upper bound (Pmax), False for a lower bound (Pmin).
assume_graph_preserving – Skip the graph-preserving check. Set this only when the caller has already verified the region.

Returns:

The bound as a Fraction.

Raises:

ValueError – If region is not graph-preserving for the model.

annotate_region(region: stormvogel.parametric.region.RectangularRegion, sample: bool = True, assume_graph_preserving: bool = False) → stormvogel.parametric.region.AnnotatedRegion¶

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

Always calls get_region_bound() twice to obtain a verified lower bound on the minimum (Pmin) and a verified upper bound on the maximum (Pmax) via the region checker.

When sample is True, the property is also evaluated at every vertex of region and at its center point. The minimum and maximum of those samples tighten the inner bounds:

min_value = (Pmin, min(samples))
max_value = (max(samples), Pmax)

When sample is False, only the verified bounds are used and the inner bounds default to (Pmin, Pmax):

min_value = (Pmin, Pmax)
max_value = (Pmin, Pmax)

Parameters:

region – The rectangular parameter region to annotate.
sample – Whether to evaluate at vertices and the center.
assume_graph_preserving – Skip the graph-preserving check inside get_region_bound(). Set this only when the caller has already verified that region is graph-preserving for the model.

Returns:

An AnnotatedRegion.