stormvogel.teaching.pareto
==========================

.. py:module:: stormvogel.teaching.pareto

.. autoapi-nested-parse::

   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
----------

.. autoapisummary::

   stormvogel.teaching.pareto.EPS
   stormvogel.teaching.pareto._BIG


Classes
-------

.. autoapisummary::

   stormvogel.teaching.pareto.ParetoQuery


Functions
---------

.. autoapisummary::

   stormvogel.teaching.pareto._feasible_polygon
   stormvogel.teaching.pareto._infeasible_patch
   stormvogel.teaching.pareto._add_hyperplane
   stormvogel.teaching.pareto._prepare_ax
   stormvogel.teaching.pareto._finalize_ax
   stormvogel.teaching.pareto.plot_pareto
   stormvogel.teaching.pareto.explore_pareto


Module Contents
---------------

.. py:data:: EPS
   :type:  float
   :value: 1e-09


.. py:data:: _BIG
   :type:  float
   :value: 1000000.0


.. py:class:: ParetoQuery

   A single direction-vector query result.

   :param 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.
   :param p: Achievable point returned by the model checker for direction w.


   .. py:attribute:: w
      :type:  tuple[float, float] | None


   .. py:attribute:: p
      :type:  tuple[float, float]


.. py:function:: _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).


.. py:function:: _infeasible_patch(q: ParetoQuery) -> matplotlib.patches.Polygon

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


.. py:function:: _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.


.. py:function:: _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.


.. py:function:: _finalize_ax(ax: matplotlib.axes.Axes, x_hi: float, y_hi: float, xlabel: str, ylabel: str, legend: str | bool = 'inside') -> None

.. py:function:: 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

   :param queries: Direction-vector query results.
   :param ax: Target axes; creates a new figure if None.
   :param bbox_pad: Fractional padding added around achievable points for axis limits.
   :param labels: Pair of target label strings used for the axis labels.
       Defaults to ``("T_1", "T_2")``.
   :param figsize: Figure size in inches as ``(width, height)``. Ignored when
       *ax* is provided by the caller.
   :param legend: Legend placement. ``"inside"`` (default) places it inside
       the axes; ``"outside"`` places it to the right; ``False`` suppresses it.
   :returns: The populated axes.


.. py:function:: 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 :func:`~stormvogel.teaching.multiobjective.compute_weighted_reachability_policy`.
   2. Induce the DTMC from that policy and evaluate individual reachability
      probabilities via
      :func:`~stormvogel.teaching.multiobjective.evaluate_policy_reachability`.
   3. Record the result as a :class:`ParetoQuery` with ``p = (P(T_1), P(T_2))``.

   All collected queries are then passed to :func:`plot_pareto`.

   :param mdp: The input MDP.
   :param target_labels: Exactly two target labels (2-objective setting).
   :param weight_vectors: Sequence of 2D weight vectors to query.
   :param ax: Target axes; a new figure is created if *None*.
   :param bbox_pad: Fractional padding around achievable points for axis limits.
   :param figsize: Figure size in inches as ``(width, height)``. Ignored when
       *ax* is provided by the caller.
   :param legend: Legend placement; forwarded to :func:`plot_pareto`.
   :returns: The collected queries. The plot is rendered as a side effect; use
       :func:`plot_pareto` directly if you need access to the axes.
   :raises ValueError: If *target_labels* does not have exactly two entries.
   :raises ImportError: If stormpy is not installed.

   #TODO this method currently fails to handle MECs.