refine_plan.algorithms.semi_mdp_solver
======================================

.. py:module:: refine_plan.algorithms.semi_mdp_solver

.. autoapi-nested-parse::

   Functions which solve a semi-MDP into storm and retrieve the policy.

   Author: Charlie Street
   Owner: Charlie Street



Functions
---------

.. autoapisummary::

   refine_plan.algorithms.semi_mdp_solver.synthesise_policy


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

.. py:function:: synthesise_policy(semi_mdp, prism_prop='Rmax=?[F "goal"]')

   Solve a semi-MDP and return the policy.

   Note that stormpy can only handle reachability properties.

   :param semi_mdp: The semiMDP
   :param prism_prop: The property to solve for (must be reachability-based)

   :returns: A policy with the value function included

   :raises solution_exception: Raised if issue arises with model checking result