tempestpy/doc/source/doc/engines.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Engines"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Background\n",
    "\n",
    "Storm supports different engines for building and checking a model. A detailed comparison of the different engines provided in Storm can be found on the [Storm website](http://www.stormchecker.org/documentation/usage/engines.html)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Sparse engine\n",
    "\n",
    "In all of the examples so far we used the default sparse engine:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> import stormpy.examples\n",
    ">>> import stormpy.examples.files\n",
    ">>> prism_program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)\n",
    ">>> properties = stormpy.parse_properties('P=? [F \"one\"]', prism_program)\n",
    ">>> sparse_model = stormpy.build_sparse_model(prism_program, properties)\n",
    ">>> print(type(sparse_model))\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> print(\"Number of states: {}\".format(sparse_model.nr_states))\n",
    "\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> print(\"Number of transitions: {}\".format(sparse_model.nr_transitions))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> sparse_result = stormpy.check_model_sparse(sparse_model, properties[0])\n",
    ">>> initial_state = sparse_model.initial_states[0]\n",
    ">>> print(sparse_result.at(initial_state))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Symbolic engine\n",
    "\n",
    "Instead of using the sparse engine, one can also use a symbolic representation in terms of binary decision diagrams (BDDs).\n",
    "To use the symbolic (dd) engine, we use the symbolic versions for the building and model checking:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> symbolic_model = stormpy.build_symbolic_model(prism_program, properties)\n",
    ">>> print(type(symbolic_model))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> print(\"Number of states: {}\".format(symbolic_model.nr_states))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> print(\"Number of transitions: {}\".format(symbolic_model.nr_transitions))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> symbolic_result = stormpy.check_model_dd(symbolic_model, properties[0])\n",
    ">>> print(symbolic_result)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can also filter the computed results and only consider the initial states:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)\n",
    ">>> symbolic_result.filter(filter)\n",
    ">>> print(symbolic_result.min)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "It is also possible to first build the model symbolically and then transform it into a sparse model:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> print(type(symbolic_model))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> transformed_model = stormpy.transform_to_sparse_model(symbolic_model)\n",
    ">>> print(type(transformed_model))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Hybrid engine\n",
    "\n",
    "A third possibility is to use the hybrid engine, a combination of sparse and dd engines.\n",
    "It first builds the model symbolically.\n",
    "The actual model checking is then performed with the engine which is deemed most suitable for the given task.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> print(type(symbolic_model))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    ">>> hybrid_result = stormpy.check_model_hybrid(symbolic_model, properties[0])\n",
    ">>> filter = stormpy.create_filter_initial_states_symbolic(symbolic_model)\n",
    ">>> hybrid_result.filter(filter)\n",
    ">>> print(hybrid_result)"
   ]
  }
 ],
 "metadata": {
  "date": 1598178167.148,
  "filename": "engines.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": "Engines"
 },
 "nbformat": 4,
 "nbformat_minor": 4
}