stormvogel.teaching.pareto

Pareto front geometry visualization for 2-objective MDP model checking.

Each query (w, p) defines:

  • supporting hyperplane w·x = w·p (black dashed)

  • infeasible halfspace w·x ≥ w·p one red region per query

The green region is the downward closure of the convex hull of all achievable points.

Attributes

EPS

_BIG

Classes

ParetoQuery

A single direction-vector query result.

Functions

_feasible_polygon(→ numpy.ndarray | None)

Return ordered (N, 2) vertices of the downward closure of conv({p_i}).

_infeasible_patch(→ matplotlib.patches.Polygon)

Large parallelogram covering {x | w · x ≥ w · p}; matplotlib clips to axes.

_add_hyperplane(→ None)

Draw the supporting hyperplane w · x = w · p as a dashed line on ax.

_prepare_ax(→ tuple[matplotlib.axes.Axes, float, float])

Create axes if needed; return (ax, x_hi, y_hi) with padding applied.

_finalize_ax(→ None)

plot_pareto(→ matplotlib.axes.Axes)

Visualize Pareto front geometry for a set of direction-vector queries.

explore_pareto(→ list[ParetoQuery])

Query an MDP with a set of weight vectors and visualize the Pareto geometry.

Module Contents

stormvogel.teaching.pareto.EPS: float = 1e-09
stormvogel.teaching.pareto._BIG: float = 1000000.0
class stormvogel.teaching.pareto.ParetoQuery

A single direction-vector query result.

Parameters:

  • w – Weight/direction vector; both components must be non-negative. When None, the point is plotted but no infeasible region or supporting hyperplane is drawn for it.

  • p – Achievable point returned by the model checker for direction w.

w: tuple[float, float] | None
p: tuple[float, float]
stormvogel.teaching.pareto._feasible_polygon(queries: list[ParetoQuery], x_lo: float, y_lo: float) → numpy.ndarray | None

Return ordered (N, 2) vertices of the downward closure of conv({p_i}).

Adds three corner points — origin (x_lo, y_lo), (max_x, y_lo), (x_lo, max_y) — and takes the convex hull of all points. This is the standard construction for the downward-closed feasible region of a 2D Pareto front (maximization setting).

stormvogel.teaching.pareto._infeasible_patch(q: ParetoQuery) → matplotlib.patches.Polygon

Large parallelogram covering {x | w · x ≥ w · p}; matplotlib clips to axes.

stormvogel.teaching.pareto._add_hyperplane(q: ParetoQuery, ax: matplotlib.axes.Axes, label: str | None = None) → None

Draw the supporting hyperplane w · x = w · p as a dashed line on ax.

stormvogel.teaching.pareto._prepare_ax(points: list, bbox_pad: float, ax: matplotlib.axes.Axes | None, figsize: tuple[float, float] | None = None) → tuple[matplotlib.axes.Axes, float, float]

Create axes if needed; return (ax, x_hi, y_hi) with padding applied.

stormvogel.teaching.pareto._finalize_ax(ax: matplotlib.axes.Axes, x_hi: float, y_hi: float, xlabel: str, ylabel: str, legend: str | bool = 'inside') → None
stormvogel.teaching.pareto.plot_pareto(queries: list[ParetoQuery], ax: matplotlib.axes.Axes | None = None, bbox_pad: float = 0.2, labels: tuple[str, str] | None = None, figsize: tuple[float, float] | None = None, legend: str | bool = 'inside') → matplotlib.axes.Axes

Visualize Pareto front geometry for a set of direction-vector queries.

Renders (bottom to top): - Red semitransparent halfplanes: infeasible regions, one per query - Green filled polygon: feasible region (downward closure of convex hull) - Black dashed lines: supporting hyperplanes - Black dots: achievable points

Parameters:

  • queries – Direction-vector query results.

  • ax – Target axes; creates a new figure if None.

  • bbox_pad – Fractional padding added around achievable points for axis limits.

  • labels – Pair of target label strings used for the axis labels. Defaults to ("T_1", "T_2").

  • figsize – Figure size in inches as (width, height). Ignored when ax is provided by the caller.

  • legend – Legend placement. "inside" (default) places it inside the axes; "outside" places it to the right; False suppresses it.

Returns:

The populated axes.

stormvogel.teaching.pareto.explore_pareto(mdp: stormvogel.model.Model, target_labels: list[str], weight_vectors: list[tuple[float, float]], ax: matplotlib.axes.Axes | None = None, bbox_pad: float = 0.2, figsize: tuple[float, float] | None = None, legend: str | bool = 'inside') → list[ParetoQuery]

Query an MDP with a set of weight vectors and visualize the Pareto geometry.

For each weight vector w:

  1. Compute the policy that maximises w · (P(reach T_1), P(reach T_2)) via compute_weighted_reachability_policy().

  2. Induce the DTMC from that policy and evaluate individual reachability probabilities via evaluate_policy_reachability().

  3. Record the result as a ParetoQuery with p = (P(T_1), P(T_2)).

All collected queries are then passed to plot_pareto().

Parameters:

  • mdp – The input MDP.

  • target_labels – Exactly two target labels (2-objective setting).

  • weight_vectors – Sequence of 2D weight vectors to query.

  • ax – Target axes; a new figure is created if None.

  • bbox_pad – Fractional padding around achievable points for axis limits.

  • figsize – Figure size in inches as (width, height). Ignored when ax is provided by the caller.

  • legend – Legend placement; forwarded to plot_pareto().

Returns:

The collected queries. The plot is rendered as a side effect; use plot_pareto() directly if you need access to the axes.

Raises:

  • ValueError – If target_labels does not have exactly two entries.

  • ImportError – If stormpy is not installed.

#TODO this method currently fails to handle MECs.