stormvogel.stormpy_utils.parametric_analysis
============================================

.. py:module:: stormvogel.stormpy_utils.parametric_analysis

.. autoapi-nested-parse::

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

.. autoapisummary::

   stormvogel.stormpy_utils.parametric_analysis.stormpy


Classes
-------

.. autoapisummary::

   stormvogel.stormpy_utils.parametric_analysis.AnalyseParametric


Functions
---------

.. autoapisummary::

   stormvogel.stormpy_utils.parametric_analysis.rectangular_region_to_stormpy


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

.. py:data:: stormpy
   :value: None


.. py:function:: rectangular_region_to_stormpy(name_to_var: dict[str, object], region: stormvogel.parametric.region.RectangularRegion) -> stormpy.pars.ParameterRegion

   Convert a :class:`~stormvogel.parametric.region.RectangularRegion` to a stormpy ``ParameterRegion``.

   :param name_to_var: Mapping from parameter name to the corresponding
       ``pycarl.Variable`` object (as returned by
       :meth:`AnalyseParametric.name_to_var`).
   :param 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*.


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

   :param model: A parametric stormvogel model.
   :param prop: A Storm property string, e.g. ``'P=? [F "target"]'``.
   :param env: A stormpy ``Environment`` to use; a fresh default environment
       is created when ``None``.
   :raises ImportError: If stormpy is not installed.
   :raises ValueError: If *model* is not parametric.


   .. py:attribute:: model


   .. py:attribute:: _sp_model


   .. py:attribute:: env
      :type:  stormpy.Environment


   .. py:attribute:: _formula


   .. py:attribute:: _name_to_var
      :type:  dict[str, object]


   .. py:attribute:: _instantiation_checker


   .. py:attribute:: _region_checker


   .. py:property:: name_to_var
      :type: dict[str, object]


      Mapping from parameter name to pycarl ``Variable``.

      Pass this to :func:`rectangular_region_to_stormpy` when you need to
      convert regions outside of this class.



   .. py:method:: evaluate_at_point(valuation: collections.abc.Mapping[str, stormvogel.parametric._backend.Number]) -> float

      Evaluate the property at a single parameter instantiation.

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



   .. py:method:: 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 :class:`~fractions.Fraction` derived
      from the rational number produced by stormpy's region checker.

      :param region: A rectangular parameter region.  Must be graph-preserving
          for *model*.
      :param maximize: ``True`` to get an upper bound (Pmax), ``False`` for
          a lower bound (Pmin).
      :param assume_graph_preserving: Skip the graph-preserving check.  Set
          this only when the caller has already verified the region.
      :returns: The bound as a :class:`~fractions.Fraction`.
      :raises ValueError: If *region* is not graph-preserving for the model.



   .. py:method:: 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 :meth:`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)``

      :param region: The rectangular parameter region to annotate.
      :param sample: Whether to evaluate at vertices and the center.
      :param assume_graph_preserving: Skip the graph-preserving check inside
          :meth:`get_region_bound`.  Set this only when the caller has already
          verified that *region* is graph-preserving for the model.
      :returns: An :class:`~stormvogel.parametric.region.AnnotatedRegion`.