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