diff --git a/doc/source/doc/models/building_ctmcs.rst b/doc/source/doc/models/building_ctmcs.rst index 0ddf6dd..46c8f8e 100644 --- a/doc/source/doc/models/building_ctmcs.rst +++ b/doc/source/doc/models/building_ctmcs.rst @@ -30,7 +30,7 @@ In this example, we build the transition matrix using a numpy array:: The following function call returns a sparse matrix with default row groups:: >>> transition_matrix = stormpy.build_sparse_matrix(transitions) - >>> print(transition_matrix) + >>> print(transition_matrix) # doctest: +SKIP 0 1 2 3 ---- group 0/3 ---- 0 ( 0 1.5 0 0 ) 0 @@ -67,13 +67,13 @@ Building the Model Now, we can collect all components, including the choice labeling and the exit rates. To let the transition values be interpreted as rates we set `rate_transitions` to `True`:: - components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True) - components.exit_rates = exit_rates + >>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True) + >>> components.exit_rates = exit_rates And finally, we can build the model:: >>> ctmc = stormpy.storage.SparseCtmc(components) - >>> print(ctmc) + >>> print(ctmc) # doctest: +SKIP -------------------------------------------------------------- Model type: CTMC (sparse) States: 4 diff --git a/doc/source/doc/models/building_dtmcs.rst b/doc/source/doc/models/building_dtmcs.rst index 8a9de44..aa984b3 100644 --- a/doc/source/doc/models/building_dtmcs.rst +++ b/doc/source/doc/models/building_dtmcs.rst @@ -82,7 +82,7 @@ Labels can be asociated with states. As an example, we label the state 0 with "i >>> state_labeling.add_label_to_state('init', 0) >>> print(state_labeling.get_states('init')) - bit vector(1/13) [0] + bit vector(1/13) [0 ] Next, we set the associations between the remaining labels and states.:: @@ -96,7 +96,7 @@ Next, we set the associations between the remaining labels and states.:: 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])) - >>> print(state_labeling) + >>> print(state_labeling) # doctest: +SKIP 9 labels * one -> 1 item(s) * four -> 1 item(s) @@ -131,7 +131,7 @@ Next, we collect all components:: And finally, we can build the DTMC:: >>> dtmc = stormpy.storage.SparseDtmc(components) - >>> print(dtmc) + >>> print(dtmc) # doctest: +SKIP -------------------------------------------------------------- Model type: DTMC (sparse) States: 13 diff --git a/doc/source/doc/models/building_mas.rst b/doc/source/doc/models/building_mas.rst index 852b00b..a840746 100644 --- a/doc/source/doc/models/building_mas.rst +++ b/doc/source/doc/models/building_mas.rst @@ -39,7 +39,7 @@ In the beginning, we create a numpy array that will be used to build the transit 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:: >>> transition_matrix = stormpy.build_sparse_matrix(transitions, [0, 2, 3, 4, 5]) - >>> print(transition_matrix) + >>> print(transition_matrix) # doctest: +SKIP 0 1 2 3 4 ---- group 0/4 ---- @@ -65,17 +65,33 @@ we build a BitVector that contains the respective Markovian states:: Building the Model ==================== + +.. testsetup:: + # Not displayed in documentation but needed for doctests + + >>> state_labeling = stormpy.storage.StateLabeling(5) + >>> state_labels = {'init', 'deadlock'} + >>> for label in state_labels: + ... state_labeling.add_label(label) + >>> state_labeling.add_label_to_state('init', 0) + >>> choice_labeling = stormpy.storage.ChoiceLabeling(6) + >>> choice_labels = {'alpha', 'beta'} + >>> for label in choice_labels: + ... choice_labeling.add_label(label) + >>> choice_labeling.add_label_to_choice('alpha', 0) + >>> choice_labeling.add_label_to_choice('beta', 1) + >>> exit_rates = [0.0, 10.0, 12.0, 1.0, 1.0] + Now, we can collect all components:: - >>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, - markovian_states=markovian_states) + >>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, markovian_states=markovian_states) >>> components.choice_labeling = choice_labeling >>> components.exit_rates = exit_rates Finally, we can build the model:: >>> ma = stormpy.storage.SparseMA(components) - >>> print(ma) + >>> print(ma) # doctest: +SKIP -------------------------------------------------------------- Model type: Markov Automaton (sparse) States: 5 diff --git a/doc/source/doc/models/building_mdps.rst b/doc/source/doc/models/building_mdps.rst index a588df3..2b94a5e 100644 --- a/doc/source/doc/models/building_mdps.rst +++ b/doc/source/doc/models/building_mdps.rst @@ -82,7 +82,7 @@ Recall that those actions where defined in row one and two of the transition mat >>> choice_labeling.add_label_to_choice('a', 0) >>> choice_labeling.add_label_to_choice('b', 1) - >>> print(choice_labeling) + >>> print(choice_labeling) # doctest: +SKIP Choice 2 labels * a -> 1 item(s) * b -> 1 item(s) @@ -99,6 +99,23 @@ In this reward model the length of the action rewards coincides with the number Building the Model ==================== + +.. testsetup:: + + # Not displayed in documentation but needed for doctests + >>> 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) + >>> 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) + >>> state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12])) + We collect the components:: >>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions=False) @@ -107,7 +124,7 @@ We collect the components:: We build the model:: >>> mdp = stormpy.storage.SparseMdp(components) - >>> print(mdp) + >>> print(mdp) # doctest: +SKIP Model type: MDP (sparse) States: 13 Transitions: 22