doc dtmcs

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

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
+    --------------------------------------------------------------

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()