stormvogel.teaching.parametric¶

Parameter space partitioning for parametric Markov models.

Classes¶

FeasibilityProblem

Structured encoding of the parametric reachability feasibility problem.

Functions¶

`parameter_space_partitioning`(...)	Partition the parameter space into annotated regions.
`_state_vars_readable`(→ dict[stormvogel.model.State, ...)	Create teaching-friendly sympy symbols `p_{name}` for each state.
`feasibility_problem`(→ FeasibilityProblem)	Build the feasibility encoding for parametric reachability in a pMC.
`_check_markov_chain`(→ None)
`_t_reachable_nontargets`(→ list[stormvogel.model.State])	Return non-target states from which some target is reachable, in elimination order.
`eliminate_selfloop`(→ None)	Rescale s's outgoing distribution by `1/(1 − P(s,s))` and zero the loop.
`eliminate_transition`(→ None)	Add shortcuts from s_in to every successor of s; zero `P(s_in, s)`.
`eliminate_state`(→ None)	Eliminate all incoming edges to s (must be loop-free).
`solve_reachability`(→ sympy.Expr)	Return the reachability solution function at the initial state via state elimination.

Module Contents¶

stormvogel.teaching.parametric.parameter_space_partitioning(model: parameter_space_partitioning.model, prop: str, threshold: stormvogel.parametric._backend.Number, initial_region: stormvogel.parametric.region.RectangularRegion | None = None, max_iterations: int = 100) → list[stormvogel.parametric.region.AnnotatedRegion]¶

Partition the parameter space into annotated regions.

Starting from initial_region (defaulting to [0.01, 0.99]^n), the algorithm repeatedly annotates the front region in the queue and classifies it against threshold via classify():

safe / unsafe: added to the result; not split further.
unknown / neither: split along the widest dimension and both halves re-queued, as long as the split count is below max_iterations. Once the budget is exhausted the queue is drained — each remaining region is annotated and collected without further splitting.

Parameters:

model – An affine parametric stormvogel model.
prop – A Storm property string, e.g. 'P=? [F "target"]'.
threshold – Classification threshold passed to classify().
initial_region – Starting region. Defaults to [0.01, 0.99]^n where n is the number of declared parameters.
max_iterations – Maximum number of splits before the queue is drained without further splitting.

Returns:

Flat list of AnnotatedRegion.

Raises:

ValueError – If the initial region is not graph-preserving.
ImportError – If stormpy is not installed.

stormvogel.teaching.parametric._state_vars_readable(pmc: stormvogel.model.Model) → dict[stormvogel.model.State, sympy.Symbol]¶: Create teaching-friendly sympy symbols p_{name} for each state.

class stormvogel.teaching.parametric.FeasibilityProblem¶

Structured encoding of the parametric reachability feasibility problem.

Mirrors the existential encoding:

∃ x̄  ∃ p_{s_0}…p_{s_n}
  ∧  lo_x ≤ x ≤ hi_x          for each parameter  (parameter_bounds)
  ∧  p_s = 0                   for s ∈ S_zero       (zero_equations)
  ∧  p_s = 1                   for s ∈ T            (target_equations)
  ∧  p_s = Σ δ(s,s') p_{s'}   for interior s       (interior_equations)
  ∧  p_{s_init} ≥ λ                                 (threshold)

Constraints are stored as sympy relational objects (sp.Eq, sp.Ge).

Parameters:

parameter_bounds – Mapping from parameter symbol to (lower, upper).
zero_equations – sp.Eq(p_s, 0) for each s ∈ S_zero.
target_equations – sp.Eq(p_s, 1) for each s ∈ T.
interior_equations – sp.Eq(p_s, Σ δ·p_{s'}) for interior s.
threshold – sp.Ge(p_{s_init}, λ).
state_variables – Mapping from state to its sympy symbol.

parameter_bounds: dict[sympy.Symbol, tuple[sympy.Expr, sympy.Expr]]¶

zero_equations: list[sympy.Basic]¶

target_equations: list[sympy.Basic]¶

interior_equations: list[sympy.Basic]¶

threshold: sympy.Basic¶

state_variables: dict[stormvogel.model.State, sympy.Symbol]¶

_repr_latex_() → str¶

stormvogel.teaching.parametric.feasibility_problem(pmc: stormvogel.model.Model, target_label: str, threshold: sympy.Expr | float, region: stormvogel.parametric.region.RectangularRegion, zero_states: Iterable[model.State] | None = None) → FeasibilityProblem¶

Build the feasibility encoding for parametric reachability in a pMC.

Constructs a FeasibilityProblem whose constraints are equivalent to: does there exist a parameter valuation inside region such that the reachability probability of states labelled target_label at the initial state is at least threshold?

Parameters:

pmc – A stormvogel DTMC (plain or parametric).
target_label – Label identifying target states (reachability = 1).
threshold – Lower bound λ on the initial-state reachability.
region – Rectangular parameter region providing bounds per parameter.
zero_states – States with known reachability 0, or None to auto-detect from the graph structure.

Returns:

A FeasibilityProblem with all constraint groups filled.

Raises:

ValueError – If pmc is not a DTMC.
KeyError – If target_label is not present in pmc.

stormvogel.teaching.parametric._check_markov_chain(pmc: stormvogel.model.Model) → None¶

stormvogel.teaching.parametric._t_reachable_nontargets(pmc: stormvogel.model.Model, target_states: list[stormvogel.model.State], order: list[stormvogel.model.State] | None) → list[stormvogel.model.State]¶: Return non-target states from which some target is reachable, in elimination order.

stormvogel.teaching.parametric.eliminate_selfloop(pmc: stormvogel.model.Model, s: stormvogel.model.State) → None¶

Rescale s’s outgoing distribution by 1/(1 − P(s,s)) and zero the loop.

Precondition: P(s, s) ≠ 1. No-op when P(s, s) = 0.

stormvogel.teaching.parametric.eliminate_transition(pmc: stormvogel.model.Model, s_in: stormvogel.model.State, s: stormvogel.model.State) → None¶

Add shortcuts from s_in to every successor of s; zero P(s_in, s).

Precondition: P(s, s) = 0 — call eliminate_selfloop() first.

stormvogel.teaching.parametric.eliminate_state(pmc: stormvogel.model.Model, s: stormvogel.model.State, remove: bool = False) → None¶

Eliminate all incoming edges to s (must be loop-free).

Calls eliminate_transition() for every predecessor of s.

Parameters:: remove – If True, remove s from the model after elimination.

stormvogel.teaching.parametric.solve_reachability(pmc: stormvogel.model.Model, target_states: Iterable[stormvogel.model.State], order: list[stormvogel.model.State] | None = None) → sympy.Expr¶

Return the reachability solution function at the initial state via state elimination.

Implements Algorithm 2: eliminates all non-target T-reachable states, collapses the initial state’s self-loop, then sums its outgoing edges to T. Creates a copy of pmc internally; the original is not modified.

Parameters:

pmc – A parametric DTMC.
target_states – Target states (matched by UUID, may come from the original model before copying).
order – Explicit elimination order. Defaults to lexicographic by friendly name. Affects expression size but not correctness.

Returns:

A sympy.Expr rational function in the parameters.