diff --git a/doc/source/doc/models/.ipynb_checkpoints/building_ctmcs-checkpoint.ipynb b/doc/source/doc/models/.ipynb_checkpoints/building_ctmcs-checkpoint.ipynb deleted file mode 100644 index ff32229..0000000 --- a/doc/source/doc/models/.ipynb_checkpoints/building_ctmcs-checkpoint.ipynb +++ /dev/null @@ -1,189 +0,0 @@ -{ - "cells": [ - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "# Continuous-time Markov chains (CTMCs)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Background\n", - "\n", - "In this section, we explain how Stormpy can be used to build a simple CTMC.\n", - "Building CTMCs works similar to building DTMCs as in [Discrete-time Markov chains (DTMCs)](building_dtmcs.ipynb), but additionally every state is equipped with an exit rate.\n", - "\n", - "[01-building-ctmcs.py](https://github.com/moves-rwth/stormpy/blob/master/examples/building_ctmcs/01-building-ctmcs.py)\n", - "\n", - "First, we import Stormpy:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> import stormpy" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Transition Matrix\n", - "\n", - "In this example, we build the transition matrix using a numpy array" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": {}, - "outputs": [], - "source": [ - ">>> import numpy as np\n", - ">>> transitions = np.array([\n", - "... [0, 1.5, 0, 0],\n", - "... [3, 0, 1.5, 0],\n", - "... [0, 3, 0, 1.5],\n", - "... [0, 0, 3, 0], ], dtype='float64')" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "The following function call returns a sparse matrix with default row groups:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> transition_matrix = stormpy.build_sparse_matrix(transitions)\n", - ">>> print(transition_matrix) " - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Labeling\n", - "\n", - "The state labeling is created analogously to the previous example in [building DTMCs](building_dtmcs.ipynb#labeling):" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> state_labeling = stormpy.storage.StateLabeling(4)\n", - ">>> state_labels = {'empty', 'init', 'deadlock', 'full'}\n", - ">>> for label in state_labels:\n", - "... state_labeling.add_label(label)\n", - ">>> state_labeling.add_label_to_state('init', 0)\n", - ">>> state_labeling.add_label_to_state('empty', 0)\n", - ">>> state_labeling.add_label_to_state('full', 3)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Exit Rates\n", - "\n", - "Lastly, we initialize a list to equip every state with an exit rate:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> exit_rates = [1.5, 4.5, 4.5, 3.0]" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Building the Model\n", - "\n", - "Now, we can collect all components, including the choice labeling and the exit rates.\n", - "To let the transition values be interpreted as rates we set rate_transitions to True:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True)\n", - ">>> components.exit_rates = exit_rates" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "And finally, we can build the model:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> ctmc = stormpy.storage.SparseCtmc(components)\n", - ">>> print(ctmc) " - ] - } - ], - "metadata": { - "date": 1598178167.1853151, - "filename": "building_ctmcs.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": "Continuous-time Markov chains (CTMCs)" - }, - "nbformat": 4, - "nbformat_minor": 4 -} diff --git a/doc/source/doc/models/.ipynb_checkpoints/building_dtmcs-checkpoint.ipynb b/doc/source/doc/models/.ipynb_checkpoints/building_dtmcs-checkpoint.ipynb deleted file mode 100644 index aa4f95e..0000000 --- a/doc/source/doc/models/.ipynb_checkpoints/building_dtmcs-checkpoint.ipynb +++ /dev/null @@ -1,328 +0,0 @@ -{ - "cells": [ - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "# Discrete-time Markov chains (DTMCs)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Background\n", - "\n", - "As described in [Getting Started](../../getting_started.ipynb),\n", - "Storm can be used to translate a model description e.g. in form of a prism file into a Markov chain.\n", - "\n", - "Here, we use Stormpy to create the components for a model and build a DTMC directly from these components without parsing a model description.\n", - "We consider the previous example of the Knuth-Yao die.\n", - "\n", - "[01-building-dtmcs.py](https://github.com/moves-rwth/stormpy/blob/master/examples/building_dtmcs/01-building-dtmcs.py)\n", - "\n", - "In the following we create the transition matrix, the state labeling and the reward models of a DTMC.\n", - "First, we import stormpy:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> import stormpy" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Transition Matrix\n", - "\n", - "We begin by creating the matrix representing the transitions in the model in terms of probabilities.\n", - "For constructing the transition matrix, we use the SparseMatrixBuilder:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> builder = stormpy.SparseMatrixBuilder(rows = 0, columns = 0, entries = 0, force_dimensions = False, has_custom_row_grouping = False)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Here, we start with an empty matrix to later insert more entries.\n", - "If the number of rows, columns and entries is known, the matrix can be constructed using these values.\n", - "\n", - "For DTMCs each state has at most one outgoing probability distribution.\n", - "Thus, we create a matrix with trivial row grouping where each group contains one row representing the state action.\n", - "In [Markov decision processes (MDPs)](building_mdps.ipynb) we will revisit the example of the die, but extend the model with nondeterministic choice.\n", - "\n", - "We specify the transitions of the model by adding values to the matrix where the column represents the target state.\n", - "All transitions are equipped with a probability defined by the value:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> builder.add_next_value(row = 0, column = 1, value = 0.5)\n", - ">>> builder.add_next_value(0, 2, 0.5)\n", - ">>> builder.add_next_value(1, 3, 0.5)\n", - ">>> builder.add_next_value(1, 4, 0.5)\n", - ">>> builder.add_next_value(2, 5, 0.5)\n", - ">>> builder.add_next_value(2, 6, 0.5)\n", - ">>> builder.add_next_value(3, 7, 0.5)\n", - ">>> builder.add_next_value(3, 1, 0.5)\n", - ">>> builder.add_next_value(4, 8, 0.5)\n", - ">>> builder.add_next_value(4, 9, 0.5)\n", - ">>> builder.add_next_value(5, 10, 0.5)\n", - ">>> builder.add_next_value(5, 11, 0.5)\n", - ">>> builder.add_next_value(6, 2, 0.5)\n", - ">>> builder.add_next_value(6, 12, 0.5)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Lastly, we add a self-loop with probability one to the final states:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> for s in range(7,13):\n", - "... builder.add_next_value(s, s, 1)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Finally, we can build the matrix:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> transition_matrix = builder.build()" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "It should be noted that entries can only be inserted in ascending order, i.e. row by row and column by column.\n", - "Stormpy provides the possibility to build a sparse matrix using the numpy library ([https://numpy.org/](https://numpy.org/) )\n", - "Instead of using the SparseMatrixBuilder, a sparse matrix can be build from a numpy array via the method stormpy.build_sparse_matrix.\n", - "An example is given in [building CTMCs](building_ctmcs.ipynb#transition-matrix)." - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Labeling\n", - "\n", - "States can be labeled with sets of propositions, for example state 0 can be labeled with “init”.\n", - "In order to specify the state labeling we create an empty labeling for the given number of states and add the labels to the labeling:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> state_labeling = stormpy.storage.StateLabeling(13)\n", - "\n", - ">>> labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}\n", - ">>> for label in labels:\n", - "... state_labeling.add_label(label)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Labels can be asociated with states. As an example, we label the state 0 with “init”:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> state_labeling.add_label_to_state('init', 0)\n", - ">>> print(state_labeling.get_states('init'))" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Next, we set the associations between the remaining labels and states.:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> state_labeling.add_label_to_state('one', 7)\n", - ">>> state_labeling.add_label_to_state('two', 8)\n", - ">>> state_labeling.add_label_to_state('three', 9)\n", - ">>> state_labeling.add_label_to_state('four', 10)\n", - ">>> state_labeling.add_label_to_state('five', 11)\n", - ">>> state_labeling.add_label_to_state('six', 12)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "To set the same label for multiple states, we can use a BitVector representation for the set of states:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))\n", - ">>> print(state_labeling) " - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Defining a choice labeling is possible in a similar way." - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Reward Models\n", - "\n", - "Stormpy supports multiple reward models such as state rewards, state-action rewards and as transition rewards.\n", - "In this example, the actions of states which satisfy s<7 acquire a reward of 1.0.\n", - "\n", - "The state-action rewards are represented by a vector, which is associated to a reward model named “coin_flips”:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> reward_models = {}\n", - ">>> action_reward = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]\n", - ">>> reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector = action_reward)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Building the Model\n", - "\n", - "Next, we collect all components:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "And finally, we can build the DTMC:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> dtmc = stormpy.storage.SparseDtmc(components)\n", - ">>> print(dtmc) " - ] - } - ], - "metadata": { - "date": 1598178167.203723, - "filename": "building_dtmcs.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": "Discrete-time Markov chains (DTMCs)" - }, - "nbformat": 4, - "nbformat_minor": 4 -} diff --git a/doc/source/doc/models/.ipynb_checkpoints/building_mas-checkpoint.ipynb b/doc/source/doc/models/.ipynb_checkpoints/building_mas-checkpoint.ipynb deleted file mode 100644 index b4f177f..0000000 --- a/doc/source/doc/models/.ipynb_checkpoints/building_mas-checkpoint.ipynb +++ /dev/null @@ -1,211 +0,0 @@ -{ - "cells": [ - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "# Markov automata (MAs)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Background\n", - "\n", - "We already saw the process of building [CTMCs](building_ctmcs.ipynb) and [MDPs](building_mdps.ipynb) via Stormpy.\n", - "\n", - "Markov automata use states that are probabilistic, i.e. like the states of an MDP, or Markovian, i.e. like the states of a CTMC.\n", - "\n", - "In this section, we build a small MA with five states from which the first four are Markovian.\n", - "Since we covered labeling and exit rates already in the previous examples we omit the description of these components.\n", - "The full example can be found here:\n", - "\n", - "[01-building-mas.py](https://github.com/moves-rwth/stormpy/blob/master/examples/building_mas/01-building-mas.py)\n", - "\n", - "First, we import Stormpy:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> import stormpy" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Transition Matrix\n", - "\n", - "For [building MDPS](building_mdps.ipynb#transition-matrix), we used the SparseMatrixBuilder to create a matrix with a custom row grouping.\n", - "In this example, we use the numpy library.\n", - "\n", - "In the beginning, we create a numpy array that will be used to build the transition matrix of our model.:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> import numpy as np\n", - ">>> transitions = np.array([\n", - "... [0, 1, 0, 0, 0],\n", - "... [0.8, 0, 0.2, 0, 0],\n", - "... [0.9, 0, 0, 0.1, 0],\n", - "... [0, 0, 0, 0, 1],\n", - "... [0, 0, 0, 1, 0],\n", - "... [0, 0, 0, 0, 1]], dtype='float64')" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "When building the matrix we define a custom row grouping by passing a list containing the starting row of each row group in ascending order:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> transition_matrix = stormpy.build_sparse_matrix(transitions, [0, 2, 3, 4, 5])\n", - ">>> print(transition_matrix) " - ] - }, - { - "cell_type": "markdown", - "metadata": { - "nbsphinx": "hidden" - }, - "source": [ - "## Labeling and Exit Rates" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "nbsphinx": "hidden" - }, - "outputs": [], - "source": [ - "\n", - ">>> state_labeling = stormpy.storage.StateLabeling(5)\n", - ">>> state_labels = {'init', 'deadlock'}\n", - ">>> for label in state_labels:\n", - "... state_labeling.add_label(label)\n", - ">>> state_labeling.add_label_to_state('init', 0)\n", - "\n", - ">>> choice_labeling = stormpy.storage.ChoiceLabeling(6)\n", - ">>> choice_labels = {'alpha', 'beta'}\n", - ">>> for label in choice_labels:\n", - "... choice_labeling.add_label(label)\n", - ">>> choice_labeling.add_label_to_choice('alpha', 0)\n", - ">>> choice_labeling.add_label_to_choice('beta', 1)\n", - "\n", - ">>> exit_rates = [0.0, 10.0, 12.0, 1.0, 1.0]" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Markovian States\n", - "\n", - "In order to define which states have only one probability distribution over the successor states,\n", - "we build a BitVector that contains the respective Markovian states:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> markovian_states = stormpy.BitVector(5, [1, 2, 3, 4])" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Building the Model\n", - "\n", - "Now, we can collect all components:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, markovian_states=markovian_states)\n", - ">>> components.choice_labeling = choice_labeling\n", - ">>> components.exit_rates = exit_rates" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Finally, we can build the model:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> ma = stormpy.storage.SparseMA(components)\n", - ">>> print(ma) " - ] - } - ], - "metadata": { - "celltoolbar": "Edit Metadata", - "date": 1598178167.2185411, - "filename": "building_mas.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": "Markov automata (MAs)" - }, - "nbformat": 4, - "nbformat_minor": 4 -} diff --git a/doc/source/doc/models/.ipynb_checkpoints/building_mdps-checkpoint.ipynb b/doc/source/doc/models/.ipynb_checkpoints/building_mdps-checkpoint.ipynb deleted file mode 100644 index 5ebf2e1..0000000 --- a/doc/source/doc/models/.ipynb_checkpoints/building_mdps-checkpoint.ipynb +++ /dev/null @@ -1,309 +0,0 @@ -{ - "cells": [ - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "# Markov decision processes (MDPs)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Background\n", - "\n", - "In [Discrete-time Markov chains (DTMCs)](building_dtmcs.ipynb) we modelled Knuth-Yao’s model of a fair die by the means of a DTMC.\n", - "In the following we extend this model with nondeterministic choice by building a Markov decision process.\n", - "\n", - "[01-building-mdps.py](https://github.com/moves-rwth/stormpy/blob/master/examples/building_mdps/01-building-mdps.py)\n", - "\n", - "First, we import Stormpy:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> import stormpy" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Transition Matrix\n", - "\n", - "Since we want to build a nondeterminstic model, we create a transition matrix with a custom row group for each state:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=True, row_groups=0)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "We need more than one row for the transitions starting in state 0 because a nondeterministic choice over the actions is available.\n", - "Therefore, we start a new group that will contain the rows representing actions of state 0.\n", - "Note that the row group needs to be added before any entries are added to the group:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> builder.new_row_group(0)\n", - ">>> builder.add_next_value(0, 1, 0.5)\n", - ">>> builder.add_next_value(0, 2, 0.5)\n", - ">>> builder.add_next_value(1, 1, 0.2)\n", - ">>> builder.add_next_value(1, 2, 0.8)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "In this example, we have two nondeterministic choices in state 0.\n", - "With choice 0 we have probability 0.5 to got to state 1 and probability 0.5 to got to state 2.\n", - "With choice 1 we got to state 1 with probability 0.2 and go to state 2 with probability 0.8.\n", - "\n", - "For the remaining states, we need to specify the starting rows of each row group:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> builder.new_row_group(2)\n", - ">>> builder.add_next_value(2, 3, 0.5)\n", - ">>> builder.add_next_value(2, 4, 0.5)\n", - ">>> builder.new_row_group(3)\n", - ">>> builder.add_next_value(3, 5, 0.5)\n", - ">>> builder.add_next_value(3, 6, 0.5)\n", - ">>> builder.new_row_group(4)\n", - ">>> builder.add_next_value(4, 7, 0.5)\n", - ">>> builder.add_next_value(4, 1, 0.5)\n", - ">>> builder.new_row_group(5)\n", - ">>> builder.add_next_value(5, 8, 0.5)\n", - ">>> builder.add_next_value(5, 9, 0.5)\n", - ">>> builder.new_row_group(6)\n", - ">>> builder.add_next_value(6, 10, 0.5)\n", - ">>> builder.add_next_value(6, 11, 0.5)\n", - ">>> builder.new_row_group(7)\n", - ">>> builder.add_next_value(7, 2, 0.5)\n", - ">>> builder.add_next_value(7, 12, 0.5)\n", - "\n", - ">>> for s in range(8, 14):\n", - "... builder.new_row_group(s)\n", - "... builder.add_next_value(s, s - 1, 1)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Finally, we build the transition matrix:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> transition_matrix = builder.build()" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Labeling\n", - "\n", - "We have seen the construction of a state labeling in previous examples. Therefore we omit the description here\n", - "Instead, we focus on the choices.\n", - "Since in state 0 a nondeterministic choice over two actions is available, the number of choices is 14.\n", - "To distinguish those we can define a choice labeling:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "nbsphinx": "hidden" - }, - "outputs": [], - "source": [ - ">>> state_labeling = stormpy.storage.StateLabeling(13)\n", - ">>> labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}\n", - ">>> for label in labels:\n", - "... state_labeling.add_label(label)\n", - "\n", - ">>> state_labeling.add_label_to_state('init', 0)\n", - ">>> state_labeling.add_label_to_state('one', 7)\n", - ">>> state_labeling.add_label_to_state('two', 8)\n", - ">>> state_labeling.add_label_to_state('three', 9)\n", - ">>> state_labeling.add_label_to_state('four', 10)\n", - ">>> state_labeling.add_label_to_state('five', 11)\n", - ">>> state_labeling.add_label_to_state('six', 12)\n", - ">>> state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> choice_labeling = stormpy.storage.ChoiceLabeling(14)\n", - ">>> choice_labels = {'a', 'b'}\n", - "\n", - ">>> for label in choice_labels:\n", - "... choice_labeling.add_label(label)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "We assign the label ‘a’ to the first action of state 0 and ‘b’ to the second.\n", - "Recall that those actions where defined in row one and two of the transition matrix respectively:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> choice_labeling.add_label_to_choice('a', 0)\n", - ">>> choice_labeling.add_label_to_choice('b', 1)\n", - ">>> print(choice_labeling) " - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Reward models\n", - "\n", - "In this reward model the length of the action rewards coincides with the number of choices:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> reward_models = {}\n", - ">>> action_reward = [0.0, 0.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]\n", - ">>> reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward)" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Building the Model\n", - "\n", - "We collect the components:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False)\n", - ">>> components.choice_labeling = choice_labeling" - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "We build the model:" - ] - }, - { - "cell_type": "code", - "execution_count": null, - "metadata": { - "hide-output": false - }, - "outputs": [], - "source": [ - ">>> mdp = stormpy.storage.SparseMdp(components)\n", - ">>> print(mdp) " - ] - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "## Partially observable Markov decision process (POMDPs)\n", - "\n", - "To build a partially observable Markov decision process (POMDP),\n", - "components.observations can be set to a list of numbers that defines the status of the observables in each state." - ] - } - ], - "metadata": { - "celltoolbar": "Edit Metadata", - "date": 1598178167.234528, - "filename": "building_mdps.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": "Markov decision processes (MDPs)" - }, - "nbformat": 4, - "nbformat_minor": 4 -}