sp
/
tempestpy
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

binder badge

refactoring
hannah 4 years ago
committed by Matthias Volk
parent
9bc48bbf3a
commit
06c08e42ef
No known key found for this signature in database GPG Key ID: 83A57678F739FCD3
10 changed files with 11 additions and 1687 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 11
      doc/source/conf.py
  2. 196
      doc/source/doc/.ipynb_checkpoints/analysis-checkpoint.ipynb
  3. 138
      doc/source/doc/.ipynb_checkpoints/building_models-checkpoint.ipynb
  4. 132
      doc/source/doc/.ipynb_checkpoints/dfts-checkpoint.ipynb
  5. 285
      doc/source/doc/.ipynb_checkpoints/exploration-checkpoint.ipynb
  6. 260
      doc/source/doc/.ipynb_checkpoints/gspns-checkpoint.ipynb
  7. 174
      doc/source/doc/.ipynb_checkpoints/parametric_models-checkpoint.ipynb
  8. 133
      doc/source/doc/.ipynb_checkpoints/reward_models-checkpoint.ipynb
  9. 202
      doc/source/doc/.ipynb_checkpoints/schedulers-checkpoint.ipynb
  10. 167
      doc/source/doc/.ipynb_checkpoints/shortest_paths-checkpoint.ipynb

11
doc/source/conf.py
View File

@ -241,3 +241,14 @@ texinfo_documents = [
# Example configuration for intersphinx: refer to the Python standard library.
intersphinx_mapping = {'https://docs.python.org/': None}
nbsphinx_prolog = """
{% set docname = env.doc2path(env.docname, base=None) %}
.. raw:: html
<div class="admonition note">
Interactive online version:
<span style="white-space: nowrap;"><a href="https://mybinder.org/v2/gh/m-hannah/stormpy/master?filepath=notebooks/{{ docname }}"><img alt="Binder badge" src="https://mybinder.org/badge_logo.svg" style="vertical-align:text-bottom"></a>.</span>
</div>
"""

196
doc/source/doc/.ipynb_checkpoints/analysis-checkpoint.ipynb
View File

@ -1,196 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Analysis"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Background\n",
"\n",
"Storm supports various model checking approaches that we consider in this section on analysis.\n",
"\n",
"As always:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> import stormpy\n",
">>> import stormpy.examples\n",
">>> import stormpy.examples.files\n",
">>> path = stormpy.examples.files.prism_dtmc_die\n",
">>> prism_program = stormpy.parse_prism_program(path)\n",
">>> formula_str = \"P=? [F s=7 & d=2]\"\n",
">>> properties = stormpy.parse_properties(formula_str, prism_program)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Qualitative Analysis"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Adapting the model checking engine\n",
"\n",
"[02-analysis.py](https://github.com/moves-rwth/stormpy/blob/master/examples/analysis/02-analysis.py)\n",
"\n",
"Instead of using the sparse representation, models can also be built symbolically:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> model = stormpy.build_symbolic_model(prism_program, properties)\n",
">>> result = stormpy.model_checking(model, properties[0])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"To access the result, the result has to be filtered:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> filter = stormpy.create_filter_initial_states_symbolic(model)\n",
">>> result.filter(filter)\n",
">>> assert result.min == result.max"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Then, result.min (or result.max) contains the result. Notice that if there are multiple initial states, result.min will not be equal to result.max.\n",
"\n",
"Besides this analysis on the DD, there are approaches that combine both representation.\n",
"Stormpy does support them, but we have not yet documented them."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Adapting model checking algorithms\n",
"\n",
"[03-analysis.py](https://github.com/moves-rwth/stormpy/blob/master/examples/analysis/03-analysis.py)\n",
"\n",
"Reconsider the model checking example from the getting started guide:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> model = stormpy.build_model(prism_program, properties)\n",
">>> result = stormpy.model_checking(model, properties[0])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can also vary the model checking algorithm:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> env = stormpy.Environment()\n",
">>> env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)\n",
">>> env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration\n",
">>> result = stormpy.model_checking(model, properties[0], environment=env)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Finally, we allow to change some parameters of the algorithms. E.g., in iterative approaches,\n",
"we allow to change the number of iterations:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> env.solver_environment.native_solver_environment.maximum_iterations = 3\n",
">>> result = stormpy.model_checking(model, properties[0])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Notice that by setting such parameters, the result may be off from the actual model checking algorithm.\n",
"\n",
"Environments can be used likewise for symbolic model checking. See the example for more information."
]
}
],
"metadata": {
"date": 1598178167.1206837,
"filename": "analysis.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": "Analysis"
},
"nbformat": 4,
"nbformat_minor": 4
}

138
doc/source/doc/.ipynb_checkpoints/building_models-checkpoint.ipynb
View File

@ -1,138 +0,0 @@
{
"cells": [
{
"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)"
]
},
{
"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": 1598188121.587518,
"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
}

132
doc/source/doc/.ipynb_checkpoints/dfts-checkpoint.ipynb
View File

@ -1,132 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Dynamic Fault Trees"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Building DFTs\n",
"\n",
"[01-dfts.py](https://github.com/moves-rwth/stormpy/blob/master/examples/dfts/01-dfts.py)\n",
"\n",
"Dynamic fault trees can be loaded from either the Galileo format or from a custom JSON form.\n",
"A file containing the DFT in the Galileo format can be loaded via `load_dft_galileo_file(path)`.\n",
"The custom JSON format can be loaded from a file via `load_dft_json_file(path)` or directly from a string via `load_dft_json_string(path)`.\n",
"We start by loading a simple DFT containing an AND gate from JSON:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> import stormpy\n",
">>> import stormpy.dft\n",
">>> import stormpy.examples\n",
">>> import stormpy.examples.files\n",
">>> path_json = stormpy.examples.files.dft_json_and\n",
">>> dft_small = stormpy.dft.load_dft_json_file(path_json)\n",
">>> print(dft_small)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Next we load a more complex DFT from the Galileo format:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> path_galileo = stormpy.examples.files.dft_galileo_hecs\n",
">>> dft = stormpy.dft.load_dft_galileo_file(path_galileo)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"After loading the DFT, we can display some common statistics about the model:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> print(\"DFT with {} elements.\".format(dft.nr_elements()))\n",
">>> print(\"DFT has {} BEs and {} dynamic elements.\".format(dft.nr_be(), dft.nr_dynamic()))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Analyzing DFTs\n",
"\n",
"[01-dfts.py](https://github.com/moves-rwth/stormpy/blob/master/examples/dfts/01-dfts.py)\n",
"\n",
"The next step is to analyze the DFT via `analyze_dft(dft, formula)`.\n",
"Here we can use all standard properties as described in [Building properties](../getting_started.ipynb#getting-started-building-properties).\n",
"In our example we compute the Mean-time-to-failure (MTTF):"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> formula_str = \"T=? [ F \\\"failed\\\" ]\"\n",
">>> formulas = stormpy.parse_properties(formula_str)\n",
">>> results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula])\n",
">>> result = results[0]\n",
">>> print(\"MTTF: {:.2f}\".format(result))"
]
}
],
"metadata": {
"date": 1598178167.1422036,
"filename": "dfts.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": "Dynamic Fault Trees"
},
"nbformat": 4,
"nbformat_minor": 4
}

285
doc/source/doc/.ipynb_checkpoints/exploration-checkpoint.ipynb
View File

@ -1,285 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Exploring Models"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Background\n",
"\n",
"Often, stormpy is used as a testbed for new algorithms.\n",
"An essential step is to transfer the (low-level) descriptions of an MDP or other state-based model into\n",
"an own algorithm. In this section, we discuss some of the functionality."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Reading MDPs\n",
"\n",
"[01-exploration.py](https://github.com/moves-rwth/stormpy/blob/master/examples/exploration/01-exploration.py)\n",
"\n",
"In [Getting Started](../getting_started.ipynb), we briefly iterated over a DTMC. In this section, we explore an MDP:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {
"hide-output": false,
"scrolled": true
},
"outputs": [],
"source": [
">>> import doctest\n",
">>> doctest.ELLIPSIS_MARKER = '-etc-' \n",
">>> import stormpy\n",
">>> import stormpy.examples\n",
">>> import stormpy.examples.files\n",
">>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_mdp_maze)\n",
">>> prop = \"R=? [F \\\"goal\\\"]\"\n",
"\n",
">>> properties = stormpy.parse_properties_for_prism_program(prop, program, None)\n",
">>> model = stormpy.build_model(program, properties)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The iteration over the model is as before, but now, for every action, we can have several transitions:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {
"hide-output": false,
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"State 0 is initial\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 1\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 2\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 3\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 4\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 5\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 6\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 7\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 8\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 9\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 10\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 11\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 12\n",
"From state 0 by action 0, with probability 0.07692307692307693, go to state 13\n",
"From state 1 by action 0, with probability 1.0, go to state 2\n",
"From state 1 by action 1, with probability 1.0, go to state 1\n",
"From state 1 by action 2, with probability 1.0, go to state 1\n",
"From state 1 by action 3, with probability 1.0, go to state 6\n",
"From state 2 by action 0, with probability 1.0, go to state 3\n",
"From state 2 by action 1, with probability 1.0, go to state 1\n",
"From state 2 by action 2, with probability 1.0, go to state 2\n",
"From state 2 by action 3, with probability 1.0, go to state 2\n",
"From state 3 by action 0, with probability 1.0, go to state 4\n",
"From state 3 by action 1, with probability 1.0, go to state 2\n",
"From state 3 by action 2, with probability 1.0, go to state 3\n",
"From state 3 by action 3, with probability 1.0, go to state 7\n",
"From state 4 by action 0, with probability 1.0, go to state 5\n",
"From state 4 by action 1, with probability 1.0, go to state 3\n",
"From state 4 by action 2, with probability 1.0, go to state 4\n",
"From state 4 by action 3, with probability 1.0, go to state 4\n",
"From state 5 by action 0, with probability 1.0, go to state 5\n",
"From state 5 by action 1, with probability 1.0, go to state 4\n",
"From state 5 by action 2, with probability 1.0, go to state 5\n",
"From state 5 by action 3, with probability 1.0, go to state 8\n",
"From state 6 by action 0, with probability 1.0, go to state 6\n",
"From state 6 by action 1, with probability 1.0, go to state 6\n",
"From state 6 by action 2, with probability 1.0, go to state 1\n",
"From state 6 by action 3, with probability 1.0, go to state 9\n",
"From state 7 by action 0, with probability 1.0, go to state 7\n",
"From state 7 by action 1, with probability 1.0, go to state 7\n",
"From state 7 by action 2, with probability 1.0, go to state 3\n",
"From state 7 by action 3, with probability 1.0, go to state 10\n",
"From state 8 by action 0, with probability 1.0, go to state 8\n",
"From state 8 by action 1, with probability 1.0, go to state 8\n",
"From state 8 by action 2, with probability 1.0, go to state 5\n",
"From state 8 by action 3, with probability 1.0, go to state 11\n",
"From state 9 by action 0, with probability 1.0, go to state 9\n",
"From state 9 by action 1, with probability 1.0, go to state 9\n",
"From state 9 by action 2, with probability 1.0, go to state 6\n",
"From state 9 by action 3, with probability 1.0, go to state 12\n",
"From state 10 by action 0, with probability 1.0, go to state 10\n",
"From state 10 by action 1, with probability 1.0, go to state 10\n",
"From state 10 by action 2, with probability 1.0, go to state 7\n",
"From state 10 by action 3, with probability 1.0, go to state 14\n",
"From state 11 by action 0, with probability 1.0, go to state 10\n",
"From state 11 by action 1, with probability 1.0, go to state 10\n",
"From state 11 by action 2, with probability 1.0, go to state 8\n",
"From state 11 by action 3, with probability 1.0, go to state 13\n",
"From state 12 by action 0, with probability 1.0, go to state 12\n",
"From state 12 by action 1, with probability 1.0, go to state 12\n",
"From state 12 by action 2, with probability 1.0, go to state 9\n",
"From state 12 by action 3, with probability 1.0, go to state 12\n",
"From state 13 by action 0, with probability 1.0, go to state 13\n",
"From state 13 by action 1, with probability 1.0, go to state 13\n",
"From state 13 by action 2, with probability 1.0, go to state 11\n",
"From state 13 by action 3, with probability 1.0, go to state 13\n",
"From state 14 by action 0, with probability 1.0, go to state 14\n"
]
}
],
"source": [
">>> for state in model.states:\n",
"... if state.id in model.initial_states:\n",
"... print(\"State {} is initial\".format(state.id))\n",
"... for action in state.actions:\n",
"... for transition in action.transitions:\n",
"... print(\"From state {} by action {}, with probability {}, go to state {}\".format(state, action, transition.value(), transition.column))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Internally, storm can hold hints to the origin of the actions, which may be helpful to give meaning and for debugging.\n",
"As the availability and the encoding of this data depends on the input model, we discuss these features in highlevel_models.\n",
"\n",
"Storm currently supports deterministic rewards on states or actions. More information can be found in [Reward Models](reward_models.ipynb)."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Reading POMDPs\n",
"\n",
"[02-exploration.py](https://github.com/moves-rwth/stormpy/blob/master/examples/exploration/02-exploration.py)\n",
"\n",
"Internally, POMDPs extend MDPs. Thus, iterating over the MDP is done as before.\n",
"\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"scrolled": true
},
"outputs": [],
"source": [
">>> import stormpy\n",
">>> import stormpy.examples\n",
">>> import stormpy.examples.files\n",
">>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze)\n",
">>> prop = \"R=? [F \\\"goal\\\"]\"\n",
">>> properties = stormpy.parse_properties_for_prism_program(prop, program, None)\n",
">>> model = stormpy.build_model(program, properties)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Indeed, all that changed in the code above is the example we use.\n",
"And, that the model type now is a POMDP:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {
"hide-output": false,
"scrolled": true
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"ModelType.MDP\n"
]
}
],
"source": [
">>> print(model.model_type)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Additionally, POMDPs have a set of observations, which are internally just numbered by an integer from 0 to the number of observations -1"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false,
"scrolled": true
},
"outputs": [],
"source": [
">>> print(model.nr_observations)\n",
">>> for state in model.states:\n",
"... print(\"State {} has observation id {}\".format(state.id, model.observations[state.id]))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Sorting states\n",
"\n",
"[03-exploration.py](https://github.com/moves-rwth/stormpy/blob/master/examples/exploration/03-exploration.py)\n",
"\n",
"Often, one may sort the states according to the graph structure.\n",
"Storm supports some of these sorting algorithms, e.g., topological sort."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Reading MAs\n",
"\n",
"To be continued…"
]
}
],
"metadata": {
"date": 1598178167.1595793,
"filename": "exploration.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": "Exploring Models"
},
"nbformat": 4,
"nbformat_minor": 4
}

260
doc/source/doc/.ipynb_checkpoints/gspns-checkpoint.ipynb
View File

@ -1,260 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Generalized Stochastic Petri Nets"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Loading GSPNs\n",
"\n",
"[01-gspns.py](https://github.com/moves-rwth/stormpy/blob/master/examples/gspns/01-gspns.py)\n",
"\n",
"Generalized stochastic Petri nets can be given either in the PNPRO format or in the PNML format.\n",
"We start by loading a GSPN stored in the PNML format:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> import stormpy\n",
">>> import stormpy.gspn\n",
">>> import stormpy.examples\n",
">>> import stormpy.examples.files\n",
"\n",
">>> import_path = stormpy.examples.files.gspn_pnml_simple\n",
">>> gspn_parser = stormpy.gspn.GSPNParser()\n",
">>> gspn = gspn_parser.parse(import_path)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"After loading, we can display some properties of the GSPN:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> print(\"Name of GSPN: {}.\".format(gspn.get_name()))"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
">>> print(\"Number of places: {}.\".format(gspn.get_number_of_places()))"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
">>> print(\"Number of immediate transitions: {}.\".format(gspn.get_number_of_immediate_transitions()))"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
">>> print(\"Number of timed transitions: {}.\".format(gspn.get_number_of_timed_transitions()))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Building GSPNs\n",
"\n",
"[02-gspns.py](https://github.com/moves-rwth/stormpy/blob/master/examples/gspns/02-gspns.py)\n",
"\n",
"In the following, we describe how to construct GSPNs via the `GSPNBuilder`.\n",
"First, we create an instance of the `GSPNBuilder` and set the name of the GSPN:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> builder = stormpy.gspn.GSPNBuilder()\n",
">>> builder.set_name(\"my_gspn\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In the next step, we add an immediate transition to the GSPN.\n",
"Additionally, we define the position of the transition by setting its layout information:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> it_1 = builder.add_immediate_transition(1, 0.0, \"it_1\")\n",
">>> it_layout = stormpy.gspn.LayoutInfo(1.5, 2.0)\n",
">>> builder.set_transition_layout_info(it_1, it_layout)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We add a timed transition and set its layout information:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> tt_1 = builder.add_timed_transition(0, 0.4, \"tt_1\")\n",
">>> tt_layout = stormpy.gspn.LayoutInfo(12.5, 2.0)\n",
">>> builder.set_transition_layout_info(tt_1, tt_layout)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Next, we add two places to the GSPN and set their layouts:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> place_1 = builder.add_place(1, 1, \"place_1\")\n",
">>> p1_layout = stormpy.gspn.LayoutInfo(6.5, 2.0)\n",
">>> builder.set_place_layout_info(place_1, p1_layout)\n",
"\n",
">>> place_2 = builder.add_place(1, 0, \"place_2\")\n",
">>> p2_layout = stormpy.gspn.LayoutInfo(18.5, 2.0)\n",
">>> builder.set_place_layout_info(place_2, p2_layout)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Places and transitions can be linked by input, output and inhibition arcs.\n",
"We add the arcs of our GSPN as follows:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> builder.add_output_arc(it_1, place_1)\n",
">>> builder.add_inhibition_arc(place_1, it_1)\n",
">>> builder.add_input_arc(place_1, tt_1)\n",
">>> builder.add_output_arc(tt_1, place_2)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We can now build the GSPN:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> gspn = builder.build_gspn()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"After building, we export the GSPN.\n",
"GSPNs can be saved in the PNPRO format via `export_gspn_pnpro_file(path)` and in the PNML format via `export_gspn_pnml_file(path)`.\n",
"We export the GSPN into the PNPRO format:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> export_path = stormpy.examples.files.gspn_pnpro_simple\n",
">>> gspn.export_gspn_pnpro_file(export_path)"
]
}
],
"metadata": {
"date": 1598178167.1731207,
"filename": "gspns.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": "Generalized Stochastic Petri Nets"
},
"nbformat": 4,
"nbformat_minor": 4
}

174
doc/source/doc/.ipynb_checkpoints/parametric_models-checkpoint.ipynb
View File

@ -1,174 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Parametric Models"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Instantiating parametric models\n",
"\n",
"[01-parametric-models.py](https://github.com/moves-rwth/stormpy/blob/master/examples//parametric_models/01-parametric-models.py)\n",
"\n",
"Input formats such as prism allow to specify programs with open constants. We refer to these open constants as parameters.\n",
"If the constants only influence the probabilities or rates, but not the topology of the underlying model, we can build these models as parametric models:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> import stormpy\n",
">>> import stormpy.examples\n",
">>> import stormpy.examples.files\n",
">>> path = stormpy.examples.files.prism_dtmc_die\n",
">>> prism_program = stormpy.parse_prism_program(path)\n",
">>> formula_str = \"P=? [F s=7 & d=2]\"\n",
">>> properties = stormpy.parse_properties(formula_str, prism_program)\n",
">>> model = stormpy.build_parametric_model(prism_program, properties)\n",
">>> parameters = model.collect_probability_parameters()\n",
">>> for x in parameters:\n",
"... print(x)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In order to obtain a standard DTMC, MDP or other Markov model, we need to instantiate these models by means of a model instantiator:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> import stormpy.pars\n",
">>> instantiator = stormpy.pars.PDtmcInstantiator(model)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Before we obtain an instantiated model, we need to map parameters to values: We build such a dictionary as follows:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> point = dict()\n",
">>> for x in parameters:\n",
"... print(x.name)\n",
"... point[x] = 0.4\n",
">>> instantiated_model = instantiator.instantiate(point)\n",
">>> result = stormpy.model_checking(instantiated_model, properties[0])"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Initial states and labels are set as for the parameter-free case."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Checking parametric models\n",
"\n",
"[02-parametric-models.py](https://github.com/moves-rwth/stormpy/blob/master/examples//parametric_models/02-parametric-models.py)\n",
"\n",
"It is also possible to check the parametric model directly, similar as before in [Checking properties](../getting_started.ipynb#getting-started-checking-properties):"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> result = stormpy.model_checking(model, properties[0])\n",
">>> initial_state = model.initial_states[0]\n",
">>> func = result.at(initial_state)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We collect the constraints ensuring that underlying model is well-formed and the graph structure does not change:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> collector = stormpy.ConstraintCollector(model)\n",
">>> for formula in collector.wellformed_constraints:\n",
"... print(formula)\n",
">>> for formula in collector.graph_preserving_constraints:\n",
"... print(formula)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Collecting information about the parametric models\n",
"\n",
"[03-parametric-models.py](https://github.com/moves-rwth/stormpy/blob/master/examples//parametric_models/03-parametric-models.py)\n",
"\n",
"This example shows three implementations to obtain the number of transitions with probability one in a parametric model."
]
}
],
"metadata": {
"date": 1598178167.2485256,
"filename": "parametric_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": "Parametric Models"
},
"nbformat": 4,
"nbformat_minor": 4
}

133
doc/source/doc/.ipynb_checkpoints/reward_models-checkpoint.ipynb
View File

@ -1,133 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Reward Models\n",
"\n",
"In [Getting Started](../getting_started.ipynb), we mainly looked at probabilities in the Markov models and properties that refer to these probabilities.\n",
"In this section, we discuss reward models."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Exploring reward models\n",
"\n",
"[01-reward-models.py](https://github.com/moves-rwth/stormpy/blob/master/examples/reward_models/01-reward-models.py)\n",
"\n",
"We consider the die again, but with another property which talks about the expected reward:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> import stormpy\n",
">>> import stormpy.examples\n",
">>> import stormpy.examples.files\n",
">>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)\n",
">>> prop = \"R=? [F \\\"done\\\"]\"\n",
"\n",
">>> properties = stormpy.parse_properties(prop, program, None)\n",
">>> model = stormpy.build_model(program, properties)\n",
">>> assert len(model.reward_models) == 1"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The model now has a reward model, as the property talks about rewards.\n",
"When [Building Models](building_models.ipynb) from explicit sources, the reward model is always included if it is defined in the source.\n",
"We can do model checking analogous to probabilities:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> initial_state = model.initial_states[0]\n",
">>> result = stormpy.model_checking(model, properties[0])\n",
">>> print(\"Result: {}\".format(round(result.at(initial_state), 6)))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The reward model has a name which we can obtain as follows:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> reward_model_name = list(model.reward_models.keys())[0]\n",
">>> print(reward_model_name)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We discuss later how to work with multiple reward models.\n",
"Rewards come in multiple fashions, as state rewards, state-action rewards and as transition rewards.\n",
"In this example, we only have state-action rewards. These rewards are a vector, over which we can trivially iterate:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> assert not model.reward_models[reward_model_name].has_state_rewards\n",
">>> assert model.reward_models[reward_model_name].has_state_action_rewards\n",
">>> assert not model.reward_models[reward_model_name].has_transition_rewards\n",
">>> for reward in model.reward_models[reward_model_name].state_action_rewards:\n",
"... print(reward)"
]
}
],
"metadata": {
"date": 1598188121.7157953,
"filename": "reward_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": "Reward Models"
},
"nbformat": 4,
"nbformat_minor": 4
}

202
doc/source/doc/.ipynb_checkpoints/schedulers-checkpoint.ipynb
View File

@ -1,202 +0,0 @@
{
"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
}

167
doc/source/doc/.ipynb_checkpoints/shortest_paths-checkpoint.ipynb
View File

@ -1,167 +0,0 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Working with Shortest Paths\n",
"\n",
"Storm can enumerate the most probable paths of a model, leading from the initial state to a defined set of target states, which we refer to as shortest paths.\n",
"In particular, the model states visited along those paths are available as sets and can be accumulated, yielding a *sub-model*."
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Background\n",
"\n",
"The underlying implementation uses the *recursive enumeration algorithm* [[JM1999]](#jm1999), substituting distance for probability – which is why we refer to the most probable paths as the *shortest* paths.\n",
"\n",
"This algorithm computes the shortest paths recursively and in order, i.e., to find the 7th shortest path, the 1st through 6th shortest paths are computed as precursors. The next (i.e., 8th shortest) path can then be computed efficiently.\n",
"\n",
"It is crucial to note that *any* path is eligible, including those that (repeatedly) traverse loops (i.e., *non-simple* paths). This is a common case in practice: Often a large number of similar paths that differ only in the order and number of loop traversals occur successively in the sequence of shortest paths. (For applications that are only interested in simple paths, this is rather unfortunate.)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Examining Shortest Paths\n",
"\n",
"[01-shortest-paths.py](https://github.com/moves-rwth/stormpy/blob/master/examples/shortest_paths/01-shortest-paths.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.examples\n",
">>> import stormpy.examples.files\n",
">>> path = stormpy.examples.files.prism_dtmc_die\n",
">>> prism_program = stormpy.parse_prism_program(path)\n",
">>> model = stormpy.build_model(prism_program)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"We also import the `ShortestPathsGenerator`:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> from stormpy.utility import ShortestPathsGenerator"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"and choose a target state (by its ID) to which we want to compute the shortest paths:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> state_id = 8"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"It is also possible to specify a set of target states (as a list, e.g., `[8, 10, 11]`) or a label in the model if applicable (e.g., `\"observe0Greater1\"`).\n",
"For simplicity, we will stick to using a single state for now.\n",
"\n",
"We initialize a `ShortestPathsGenerator` instance:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> spg = ShortestPathsGenerator(model, state_id)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Now we can query the k-shortest path by index. Note that 1-based indices are used, so that the 3rd shortest path indeed corresponds to index `k=3`.\n",
"Let us inspect the first three shortest paths:"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"hide-output": false
},
"outputs": [],
"source": [
">>> for k in range(1, 4):\n",
"... path = spg.get_path_as_list(k)\n",
"... distance = spg.get_distance(k)\n",
"... print(\"{}-shortest path to state #{}: {}, with distance {}\".format(k, state_id, path, distance))"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"As you can see, the distance (i.e., probability of the path) is also available.\n",
"Note that the paths are displayed as a backward-traversal from the target to the initial state.\n",
"\n",
"<a id='jm1999'></a>\n",
"\\[JM1999\\] Víctor M. Jiménez, Andrés Marzal. [Computing the K Shortest Paths: A New Algorithm and an Experimental Comparison](https://scholar.google.com/scholar?q=Computing+the+k+shortest+paths%3A+A+new+algorithm+and+an+experimental+comparison). International Workshop on Algorithm Engineering, 1999"
]
}
],
"metadata": {
"date": 1598178167.2826114,
"filename": "shortest_paths.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 Shortest Paths"
},
"nbformat": 4,
"nbformat_minor": 4
}
Write Preview
Loading…
Cancel
Save