diff --git a/doc/Dockerfile b/doc/Dockerfile new file mode 100644 index 0000000..d2d0d33 --- /dev/null +++ b/doc/Dockerfile @@ -0,0 +1,43 @@ +FROM movesrwth/stormpy:1.6.0 +MAINTAINER Matthias Volk + + +########## +# 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/ diff --git a/doc/source/conf.py b/doc/source/conf.py index fec21e1..fe063d1 100644 --- a/doc/source/conf.py +++ b/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 diff --git a/doc/source/doc/building_models.ipynb b/doc/source/doc/building_models.ipynb new file mode 100644 index 0000000..0901a47 --- /dev/null +++ b/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 +} diff --git a/doc/source/doc/building_models.rst b/doc/source/doc/building_models.rst deleted file mode 100644 index 9a8c052..0000000 --- a/doc/source/doc/building_models.rst +++ /dev/null @@ -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.