From 3c29f467aac42a91f8b0afb519ed9e60e4698264 Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Sat, 27 Jun 2020 16:03:26 +0200
Subject: [PATCH] doc dtmcs
---
doc/source/advanced_topics.rst | 1 +
doc/source/doc/building_dtmcs.rst | 132 +++++++++++++++++++
examples/building_dtmcs/01-building-dtmcs.py | 67 ++++++++++
3 files changed, 200 insertions(+)
create mode 100644 doc/source/doc/building_dtmcs.rst
create mode 100644 examples/building_dtmcs/01-building-dtmcs.py
diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst
index 9d2d225..3572bea 100644
--- a/doc/source/advanced_topics.rst
+++ b/doc/source/advanced_topics.rst
@@ -10,6 +10,7 @@ This guide is a collection of examples meant to bridge the gap between the getti
doc/analysis
doc/building_models
+ doc/building_dtmcs
doc/engines
doc/exploration
doc/reward_models
diff --git a/doc/source/doc/building_dtmcs.rst b/doc/source/doc/building_dtmcs.rst
new file mode 100644
index 0000000..66dda3a
--- /dev/null
+++ b/doc/source/doc/building_dtmcs.rst
@@ -0,0 +1,132 @@
+**********************************
+Discrete-time Markov chains (DTMCs)
+**********************************
+
+
+Background
+=====================
+As described in :doc:`../getting_started`,
+Storm can be used to translate a model description e.g. in form of a prism file into a Markov chain.
+
+Here, we use Stormpy to create the single components, to build a DTMC without parsing a model description.
+We consider the previous example of the die.
+
+.. seealso:: `01-building-dtmcs.py <todo/02-gspns.py/examples/building_dtmcs/01-building-dtmcs.py>`
+
+In the following we create transition matrix, the state labeling and the reward models of a DTMC.
+First, we import stormpy::
+
+>>> import stormpy
+
+Transition Matrix
+=====================
+We begin by creating the matrix representing the transitions in the model in terms of probabilities.
+For constructing the transition matrix, we use the SparseMatrixBuilder::
+
+>>> builder = stormpy.SparseMatrixBuilder(rows = 0, columns = 0, entries = 0, force_dimensions = False, has_custom_row_grouping = False)
+
+Here, we start with an empty matrix to later insert more entries.
+If the number of rows, columns and entries is known, the matrix can be constructed using these values.
+
+For DTMCs each state has at most one outgoing probability distribution.
+Thus, we create matrix with trivial row grouping where each group contains one row representing the state action.
+
+We specify the transitions of the model, by adding values to the matrix where the column represents the target state.
+All transitions are equipped with a probability defined by the value::
+
+ >>> builder.add_next_value(row = 0, column = 1, value = 0.5)
+ >>> builder.add_next_value(0, 2, 0.5)
+ >>> builder.add_next_value(1, 3, 0.5)
+ >>> builder.add_next_value(1, 4, 0.5)
+ >>> builder.add_next_value(2, 5, 0.5)
+ >>> builder.add_next_value(2, 6, 0.5)
+ >>> builder.add_next_value(3, 7, 0.5)
+ >>> builder.add_next_value(3, 1, 0.5)
+ >>> builder.add_next_value(4, 8, 0.5)
+ >>> builder.add_next_value(4, 9, 0.5)
+ >>> builder.add_next_value(5, 10, 0.5)
+ >>> builder.add_next_value(5, 11, 0.5)
+ >>> builder.add_next_value(6, 2, 0.5)
+ >>> builder.add_next_value(6, 12, 0.5)
+
+Lastly, we add a self-loop with probability one to the final states::
+
+ >>> for s in range(7,13):
+ >>> builder.add_next_value(s, s, 1)
+
+
+Finally, we can build the matrix with updated row and columns count that both coincide with the number of states::
+
+ >>> transition_matrix = builder.build(13, 13)
+
+It should be noted that entries can only be inserted in ascending order, i.e. row by row and column by column.
+Stormpy provides the possibility to build a sparse matrix using the numpy library <https://numpy.org/>
+Instead of using the SparseMatrixBuilder, a sparse matrix can be build from a numpy array via the method stormpy.build_sparse_matrix.
+
+Labeling
+====================
+
+States can be labelled with sets of propositions, for example state 0 can be labelled with 'init'.
+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::
+
+ >>> state_labeling = stormpy.storage.StateLabeling(13)
+
+ >>> labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}
+ >>> for label in labels:
+ >>> state_labeling.add_label(label)
+
+Next, we set teh associations between the labels and the respective states.::
+
+ >>> state_labeling.add_label_to_state('init', 0)
+ >>> state_labeling.add_label_to_state('one', 7)
+ >>> state_labeling.add_label_to_state('two', 8)
+ >>> state_labeling.add_label_to_state('three', 9)
+ >>> state_labeling.add_label_to_state('four', 10)
+ >>> state_labeling.add_label_to_state('five', 11)
+ >>> state_labeling.add_label_to_state('six', 12)
+
+To set the same label for multiple states, we can use a BitVector representation for the set of states::
+
+ >>> state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))
+
+In addition, it is possible to define a choice labeling, which is described in :doc:`building_ctmcs`.
+
+Reward Models
+====================
+Stormpy supports multiple reward models such as state rewards, state-action rewards and as transition rewards.
+In this example, the actions of states which satisfy s<7 acquire a reward of 1.0.
+
+The state-action rewards are represented by a vector, which is associated to a reward model named 'coin_flips'::
+
+ >>> reward_models = {}
+ >>> 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]
+ >>> reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector = action_reward)
+
+Building the Model
+====================
+
+Next, we collect all components::
+
+ >>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models)
+
+And finally, we can build the DTMC::
+
+ >>> dtmc = stormpy.storage.SparseDtmc(components)
+ >>> print(dtmc)
+ --------------------------------------------------------------
+ Model type: DTMC (sparse)
+ States: 13
+ Transitions: 20
+ Reward Models: coin_flips
+ State Labels: 9 labels
+ * three -> 1 item(s)
+ * six -> 1 item(s)
+ * done -> 6 item(s)
+ * four -> 1 item(s)
+ * five -> 1 item(s)
+ * deadlock -> 0 item(s)
+ * init -> 1 item(s)
+ * two -> 1 item(s)
+ * one -> 1 item(s)
+ Choice Labels: none
+ --------------------------------------------------------------
diff --git a/examples/building_dtmcs/01-building-dtmcs.py b/examples/building_dtmcs/01-building-dtmcs.py
new file mode 100644
index 0000000..18cdafb
--- /dev/null
+++ b/examples/building_dtmcs/01-building-dtmcs.py
@@ -0,0 +1,67 @@
+import stormpy
+import numpy as np
+
+
+def example_building_dtmcs_01():
+
+
+ # Use the SparseMatrixBuilder for constructing the transition matrix
+ builder = stormpy.SparseMatrixBuilder(rows = 0, columns = 0, entries = 0, force_dimensions = False, has_custom_row_grouping = False)
+
+ # New Transition from state 0 to target state 1 with probability 0.5
+ builder.add_next_value(row = 0, column = 1, value = 0.5)
+ builder.add_next_value(0, 2, 0.5)
+ builder.add_next_value(1, 3, 0.5)
+ builder.add_next_value(1, 4, 0.5)
+ builder.add_next_value(2, 5, 0.5)
+ builder.add_next_value(2, 6, 0.5)
+ builder.add_next_value(3, 7, 0.5)
+ builder.add_next_value(3, 1, 0.5)
+ builder.add_next_value(4, 8, 0.5)
+ builder.add_next_value(4, 9, 0.5)
+ builder.add_next_value(5, 10, 0.5)
+ builder.add_next_value(5, 11, 0.5)
+ builder.add_next_value(6, 2, 0.5)
+ builder.add_next_value(6, 12, 0.5)
+
+ # Add transitions for the final states
+ for s in range(7,13):
+ builder.add_next_value(s, s, 1)
+
+ # Build matrix
+ transition_matrix = builder.build(13, 13)
+
+ # State labeling
+ state_labeling = stormpy.storage.StateLabeling(13)
+
+ # Add labels
+ labels = {'init','one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'}
+ for label in labels:
+ state_labeling.add_label(label)
+
+ # Add label to state
+ state_labeling.add_label_to_state('init', 0)
+ state_labeling.add_label_to_state('one', 7)
+ state_labeling.add_label_to_state('two', 8)
+ state_labeling.add_label_to_state('three', 9)
+ state_labeling.add_label_to_state('four', 10)
+ state_labeling.add_label_to_state('five', 11)
+ state_labeling.add_label_to_state('six', 12)
+
+ # Add label 'done' to multiple states
+ state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))
+
+ # Reward models:
+ reward_models = {}
+ # Create a vector representing the state-action rewards
+ 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]
+ reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector = action_reward)
+
+ components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models)
+
+ dtmc = stormpy.storage.SparseDtmc(components)
+
+ print(dtmc)
+
+if __name__ == '__main__':
+ example_building_dtmcs_01()
\ No newline at end of file