diff --git a/doc/source/conf.py b/doc/source/conf.py index 6f5193f..b33d6a3 100644 --- a/doc/source/conf.py +++ b/doc/source/conf.py @@ -248,7 +248,7 @@ nbsphinx_prolog = """ .. raw:: html
- Interactive online version: + Interactive version: Binder badge.
""" \ No newline at end of file diff --git a/doc/source/doc/building_models.ipynb b/doc/source/doc/building_models.ipynb index 4e92d5f..8ce6c11 100644 --- a/doc/source/doc/building_models.ipynb +++ b/doc/source/doc/building_models.ipynb @@ -4,9 +4,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "# Building Models\n", - "\n", - "[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/gh/m-hannah/stormpy/master?filepath=notebooks%2Fbuilding_models.ipynb)" + "# Building Models" ] }, { diff --git a/doc/source/doc/engines.ipynb b/doc/source/doc/engines.ipynb index c0d3569..61ca790 100644 --- a/doc/source/doc/engines.ipynb +++ b/doc/source/doc/engines.ipynb @@ -22,24 +22,51 @@ "source": [ "## Sparse engine\n", "\n", - "In all of the examples so far we used the default 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", + ">>> 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", - "\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", - "Number of states: 13\n", - ">>> print(\"Number of transitions: {}\".format(sparse_model.nr_transitions))\n", - "Number of transitions: 20The model checking was also done in the sparse engine:\n", - "\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))\n", - "0.16666666666666666" + ">>> print(sparse_result.at(initial_state))" ] }, { @@ -49,29 +76,89 @@ "## 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", - "\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))\n", - "\n", - ">>> print(\"Number of states: {}\".format(symbolic_model.nr_states))\n", - "Number of states: 13\n", - ">>> print(\"Number of transitions: {}\".format(symbolic_model.nr_transitions))\n", - "Number of transitions: 20\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)\n", - "[0, 1] (range)We can also filter the computed results and only consider the initial states:\n", - "\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)\n", - "0.16666650772094727It is also possible to first build the model symbolically and then transform it into a sparse model:\n", - "\n", - ">>> print(type(symbolic_model))\n", - "\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))\n", - "" + ">>> print(type(transformed_model))" ] }, { @@ -82,15 +169,28 @@ "\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", - "\n", - ">>> print(type(symbolic_model))\n", - "\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)\n", - "0.166667" + ">>> print(hybrid_result)" ] } ], @@ -98,12 +198,24 @@ "date": 1598178167.148, "filename": "engines.rst", "kernelspec": { - "display_name": "Python", - "language": "python3", + "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 -} \ No newline at end of file +}