tempestpy/doc/source/doc/schedulers.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Working with Schedulers\n",
    "\n",
    "In non-deterministic models the notion of a scheduler (or policy) is important.\n",
    "The scheduler determines which action to take at each state.\n",
    "\n",
    "For a given reachability property, Storm can return the scheduler realizing the resulting probability."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Examining Schedulers for MDPs\n",
    "\n",
    "[01-schedulers.py](https://github.com/moves-rwth/stormpy/blob/master/examples/schedulers/01-schedulers.py)\n",
    "\n",
    "As in [Getting Started](../getting_started.ipynb), we import some required modules and build a model from the example files:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "hide-output": false
   },
   "outputs": [],
   "source": [
    ">>> import stormpy\n",
    ">>> import stormpy.core\n",
    ">>> import stormpy.examples\n",
    ">>> import stormpy.examples.files\n",
    "\n",
    ">>> path = stormpy.examples.files.prism_mdp_coin_2_2\n",
    ">>> formula_str = \"Pmin=? [F \\\"finished\\\" & \\\"all_coins_equal_1\\\"]\"\n",
    ">>> program = stormpy.parse_prism_program(path)\n",
    ">>> formulas = stormpy.parse_properties(formula_str, program)\n",
    ">>> model = stormpy.build_model(program, formulas)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next we check the model and make sure to extract the scheduler:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "hide-output": false
   },
   "outputs": [],
   "source": [
    ">>> result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The result then contains the scheduler we want:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "hide-output": false
   },
   "outputs": [],
   "source": [
    ">>> assert result.has_scheduler\n",
    ">>> scheduler = result.scheduler\n",
    ">>> assert scheduler.memoryless\n",
    ">>> assert scheduler.deterministic\n",
    ">>> print(scheduler)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To get the information which action the scheduler chooses in which state, we can simply iterate over the states:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "hide-output": false
   },
   "outputs": [],
   "source": [
    ">>> for state in model.states:\n",
    "...     choice = scheduler.get_choice(state)\n",
    "...     action = choice.get_deterministic_choice()\n",
    "...     print(\"In state {} choose action {}\".format(state, action))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Examining Schedulers for Markov automata\n",
    "\n",
    "[02-schedulers.py](https://github.com/moves-rwth/stormpy/blob/master/examples/schedulers/02-schedulers.py)\n",
    "\n",
    "Currently there is no support yet for scheduler extraction on MAs.\n",
    "However, if the timing information is not relevant for the property, we can circumvent this lack by first transforming the MA to an MDP.\n",
    "\n",
    "We build the model as before:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "hide-output": false
   },
   "outputs": [],
   "source": [
    ">>> path = stormpy.examples.files.prism_ma_simple\n",
    ">>> formula_str = \"Tmin=? [ F s=4 ]\"\n",
    "\n",
    ">>> program = stormpy.parse_prism_program(path, False, True)\n",
    ">>> formulas = stormpy.parse_properties_for_prism_program(formula_str, program)\n",
    ">>> ma = stormpy.build_model(program, formulas)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next we transform the continuous-time model into a discrete-time model.\n",
    "Note that all timing information is lost at this point:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "hide-output": false
   },
   "outputs": [],
   "source": [
    ">>> mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas)\n",
    ">>> assert mdp.model_type == stormpy.ModelType.MDP"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "After the transformation we have obtained an MDP where we can extract the scheduler as shown before:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "hide-output": false
   },
   "outputs": [],
   "source": [
    ">>> result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True)\n",
    ">>> scheduler = result.scheduler\n",
    ">>> print(scheduler)\n"
   ]
  }
 ],
 "metadata": {
  "date": 1598178167.268541,
  "filename": "schedulers.rst",
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.2"
  },
  "title": "Working with Schedulers"
 },
 "nbformat": 4,
 "nbformat_minor": 4
}