You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
285 lines
11 KiB
285 lines
11 KiB
{
|
|
"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
|
|
}
|