documentation tests

doc/Dockerfile

@@ -0,0 +1,43 @@
+FROM movesrwth/stormpy:1.6.0
+MAINTAINER Matthias Volk <matthias.volk@cs.rwth-aachen.de>
+
+
+##########
+# Create user
+##########
+
+ARG NB_USER=jovyan
+ARG NB_UID=1000
+ENV USER ${NB_USER}
+ENV NB_UID ${NB_UID}
+ENV HOME /home/${NB_USER}
+
+RUN adduser --disabled-password \
+    --gecos "Default user" \
+    --uid ${NB_UID} \
+    ${NB_USER}
+
+# Change the owner of the virtual environment
+WORKDIR /opt
+USER root
+RUN chown -R ${NB_UID} venv
+USER ${NB_USER}
+
+WORKDIR ${HOME}
+# Add missing path
+ENV PATH="$HOME/.local/bin:$PATH"
+
+
+##########
+# Install dependencies
+##########
+
+RUN pip install --no-cache-dir notebook==5.7.9
+
+##########
+# Copy files for notebooks
+##########
+
+RUN mkdir notebooks
+COPY source/*.ipynb notebooks/
+COPY source/doc/*.ipynb notebooks/

doc/source/conf.py

@@ -42,7 +42,8 @@ extensions = [
     #'sphinx.ext.intersphinx',
     'sphinx.ext.coverage',
     'sphinx.ext.githubpages',
-    'sphinx.ext.autosectionlabel'
+    'sphinx.ext.autosectionlabel',
+    'nbsphinx'
 ]
 autosectionlabel_prefix_document = True
 #autosectionlabel_maxdepth = 10

doc/source/doc/building_models.ipynb

@@ -0,0 +1,136 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Building Models"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Background\n",
+    "\n",
+    "Storm supports a wide range of formalisms. Stormpy can be used to build models from some of these formalisms.\n",
+    "Moreover, during construction, various options can be set. This document yields information about the most important options."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Building different formalisms\n",
+    "\n",
+    "We use some standard examples:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "hide-output": false
+   },
+   "outputs": [],
+   "source": [
+    ">>> import stormpy.examples\n",
+    ">>> import stormpy.examples.files"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Storm supports the explicit DRN format.\n",
+    "From this, models can be built directly:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "hide-output": false
+   },
+   "outputs": [],
+   "source": [
+    ">>> path = stormpy.examples.files.drn_ctmc_dft\n",
+    ">>> model = stormpy.build_model_from_drn(path)\n",
+    ">>> print(model.model_type)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "And the same for parametric models:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "hide-output": false
+   },
+   "outputs": [],
+   "source": [
+    ">>> path = stormpy.examples.files.drn_pdtmc_die\n",
+    ">>> model = stormpy.build_parametric_model_from_drn(path)\n",
+    ">>> print(model.model_type)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Another option are JANI descriptions. These are another high-level description format.\n",
+    "Building models from JANI is done in two steps. First the Jani-description is parsed, and then the model is built from this description:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "hide-output": false
+   },
+   "outputs": [],
+   "source": [
+    ">>> path = stormpy.examples.files.jani_dtmc_die\n",
+    ">>> jani_program, properties = stormpy.parse_jani_model(path)\n",
+    ">>> model = stormpy.build_model(jani_program)\n",
+    ">>> print(model.model_type)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Notice that parsing JANI files also returns properties. In JANI, properties can be embedded in the model file."
+   ]
+  }
+ ],
+ "metadata": {
+  "date": 1596309564.4717214,
+  "filename": "building_models.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": "Building Models"
+ },
+ "nbformat": 4,
+ "nbformat_minor": 4
+}

doc/source/doc/building_models.rst

@@ -1,44 +0,0 @@
-***************
-Building Models
-***************
-
-Background
-=====================
-
-Storm supports a wide range of formalisms. Stormpy can be used to build models from some of these formalisms.
-Moreover, during construction, various options can be set. This document yields information about the most important options.
-
-
-Building different formalisms
-===============================
-
-We use some standard examples::
-
-    >>> import stormpy.examples
-    >>> import stormpy.examples.files
-
-Storm supports the explicit DRN format.
-From this, models can be built directly::
-
-    >>> path = stormpy.examples.files.drn_ctmc_dft
-    >>> model = stormpy.build_model_from_drn(path)
-    >>> print(model.model_type)
-    ModelType.CTMC
-
-And the same for parametric models::
-
-    >>> path = stormpy.examples.files.drn_pdtmc_die
-    >>> model = stormpy.build_parametric_model_from_drn(path)
-    >>> print(model.model_type)
-    ModelType.DTMC
-
-Another option are JANI descriptions. These are another high-level description format.
-Building models from JANI is done in two steps. First the Jani-description is parsed, and then the model is built from this description::
-
-    >>> path = stormpy.examples.files.jani_dtmc_die
-    >>> jani_program, properties = stormpy.parse_jani_model(path)
-    >>> model = stormpy.build_model(jani_program)
-    >>> print(model.model_type)
-    ModelType.DTMC
-
-Notice that parsing JANI files also returns properties. In JANI, properties can be embedded in the model file.