From 0ccd7de0e9aa46f4b53519e9982aced7bc53cfef Mon Sep 17 00:00:00 2001 From: hannah Date: Sun, 28 Jun 2020 13:52:21 +0200 Subject: [PATCH] simplified examples --- examples/building_ctmcs/01-building-ctmcs.py | 68 ++++---------- examples/building_dtmcs/01-building-dtmcs.py | 27 +++--- examples/building_mas/01-building-mas.py | 10 ++ examples/building_mdps/01-building-mdps.py | 99 ++++++++++++++++++++ lib/stormpy/examples/files/ctmc/tiny.sm | 11 +++ 5 files changed, 153 insertions(+), 62 deletions(-) create mode 100644 examples/building_mas/01-building-mas.py create mode 100644 examples/building_mdps/01-building-mdps.py create mode 100644 lib/stormpy/examples/files/ctmc/tiny.sm diff --git a/examples/building_ctmcs/01-building-ctmcs.py b/examples/building_ctmcs/01-building-ctmcs.py index 07df0e4..8f4acda 100644 --- a/examples/building_ctmcs/01-building-ctmcs.py +++ b/examples/building_ctmcs/01-building-ctmcs.py @@ -1,71 +1,36 @@ import stormpy import numpy as np -# polling example [IT90] -# gxn/dxp 26/01/00 -def example_building_ctmcs_01(): +def example_building_ctmcs_01(): # Building the transition matrix using numpy transitions = np.array([ - [0, 0.5, 0.5, 200, 0, 0, 0, 0, 0, 0, 0, 0], - [0, 0, 0, 0, 0.5, 200, 0, 0, 0, 0, 0, 0], - [0, 0, 0, 0, 0.5, 0, 200, 0, 0, 0, 0, 0], - [200, 0, 0, 0, 0, 0, 0.5, 0.5, 0, 0, 0, 0], - [0, 0, 0, 0, 0, 0, 0, 0, 200, 0, 0, 0], - [0, 0, 0, 1, 0, 0, 0, 0, 0.5, 0, 0, 0], - [0, 0, 0, 0, 0, 0, 0, 0, 0, 0.5, 200, 0], - [0, 200, 0, 0, 0, 0, 0, 0, 0, 0.5, 0, 0], - [0, 0, 0, 0, 0, 0, 1, 0, 0, 0 ,0, 0], - [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 200], - [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0.5 ], - [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] - ], dtype='float64') + [0, 1.5, 0, 0], + [3, 0, 1.5, 0], + [0, 3, 0, 1.5], + [0, 0, 3, 0], ], dtype='float64') - # Default row groups: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12] + # Default row groups: [0,1,2,3] transition_matrix = stormpy.build_sparse_matrix(transitions) - + print(transition_matrix) # State labeling - state_labeling = stormpy.storage.StateLabeling(12) - state_labels = {'init', 'deadlock', 'target'} + state_labeling = stormpy.storage.StateLabeling(4) + state_labels = {'empty', 'init', 'deadlock', 'full'} for label in state_labels: state_labeling.add_label(label) # Adding label to states state_labeling.add_label_to_state('init', 0) - # Sets the labeling of states given in a BitVector (length: nr_states) - state_labeling.set_states('target', stormpy.BitVector(12, [5, 8])) - - # Choice labeling - nr_choices = 12 - choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices) - choice_labels = {'loop1a', 'loop1b', 'serve1', 'loop2a', 'loop2b', 'serve2'} - for label in choice_labels: - choice_labeling.add_label(label) - # Sets the labeling of states given in a bit vector (length: nr_choices) - choice_labeling.set_choices('loop1a', stormpy.BitVector(nr_choices, [0, 2])) - choice_labeling.set_choices('loop1b', stormpy.BitVector(nr_choices, [1, 4])) - choice_labeling.set_choices('serve1', stormpy.BitVector(nr_choices, [5, 8])) - choice_labeling.set_choices('loop2a', stormpy.BitVector(nr_choices, [3, 7])) - choice_labeling.set_choices('loop2b', stormpy.BitVector(nr_choices, [6, 9])) - choice_labeling.set_choices('serve2', stormpy.BitVector(nr_choices, [10, 11])) - - # Reward models: - reward_models = {} - # Create a vector representing the state-action rewards - action_reward = [0.0, 0.0, 0.0, 0.0, 0.0, 2/3, 0.0, 0.0, 1.0, 0.0, 0.0, 0.0] - reward_models['served'] = stormpy.SparseRewardModel(optional_state_action_reward_vector = action_reward) - - ## Create a vector representing the state rewards - state_reward = [0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 0.0, 1.0, 0.0, 1.0, 0.0, 1.0] - reward_models['waiting'] = stormpy.SparseRewardModel(optional_state_reward_vector = state_reward) + state_labeling.add_label_to_state('empty', 0) + state_labeling.add_label_to_state('full', 3) # Exit rate for each state - exit_rates = [201.0, 200.5, 200.5, 201.0, 200.0, 1.5, 200.5, 200.5, 1.0, 200.0, 1.5, 1.0] + exit_rates = [1.5, 4.5, 4.5, 3.0] - # Collect components, rate_transitions = True, because the transition values are interpreted as rates (CTMC specific) - components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions = True) - components.choice_labeling = choice_labeling + # Collect components + # rate_transitions = True, because the transition values are interpreted as rates + components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True) components.exit_rates = exit_rates # Build the model @@ -73,5 +38,6 @@ def example_building_ctmcs_01(): print(ctmc) + if __name__ == '__main__': - example_building_ctmcs_01() \ No newline at end of file + example_building_ctmcs_01() diff --git a/examples/building_dtmcs/01-building-dtmcs.py b/examples/building_dtmcs/01-building-dtmcs.py index 58e8e94..1548b3d 100644 --- a/examples/building_dtmcs/01-building-dtmcs.py +++ b/examples/building_dtmcs/01-building-dtmcs.py @@ -2,13 +2,12 @@ import stormpy 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) + 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(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) @@ -24,22 +23,25 @@ def example_building_dtmcs_01(): builder.add_next_value(6, 12, 0.5) # Add transitions for the final states - for s in range(7,13): + for s in range(7, 13): builder.add_next_value(s, s, 1) # Build matrix transition_matrix = builder.build(13, 13) + print(transition_matrix) # State labeling state_labeling = stormpy.storage.StateLabeling(13) # Add labels - labels = {'init','one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} + labels = {'init', 'one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} for label in labels: state_labeling.add_label(label) - # Add label to state + # Set label to state state_labeling.add_label_to_state('init', 0) + print(state_labeling.get_states('init')) + state_labeling.add_label_to_state('one', 7) state_labeling.add_label_to_state('two', 8) state_labeling.add_label_to_state('three', 9) @@ -47,20 +49,23 @@ def example_building_dtmcs_01(): state_labeling.add_label_to_state('five', 11) state_labeling.add_label_to_state('six', 12) - # Add label 'done' to multiple states + # Set label 'done' for multiple states state_labeling.set_states('done', stormpy.BitVector(13, [7, 8, 9, 10, 11, 12])) + print(state_labeling) # 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) + 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) + 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 + example_building_dtmcs_01() diff --git a/examples/building_mas/01-building-mas.py b/examples/building_mas/01-building-mas.py new file mode 100644 index 0000000..f543ceb --- /dev/null +++ b/examples/building_mas/01-building-mas.py @@ -0,0 +1,10 @@ +import stormpy + + +# hybrid_states example +def example_building_mas_01(): + print('todo') + + +if __name__ == '__main__': + example_building_mas_01() diff --git a/examples/building_mdps/01-building-mdps.py b/examples/building_mdps/01-building-mdps.py new file mode 100644 index 0000000..9eee6f2 --- /dev/null +++ b/examples/building_mdps/01-building-mdps.py @@ -0,0 +1,99 @@ +import stormpy +import numpy as np + +# Knuth's model of a fair die using only fair coins +def example_building_mdps_01(): + nr_states = 13 + nr_choices = 14 + + # Building the transition matrix using + builder = stormpy.SparseMatrixBuilder(rows = 0, columns = 0, entries = 0, force_dimensions = False, has_custom_row_grouping = True, row_groups = 0) + + # New row group, for actions of state 0 + builder.new_row_group(0) + builder.add_next_value(0, 1, 0.5) + builder.add_next_value(0, 2, 0.5) + builder.add_next_value(1, 1, 0.2) + builder.add_next_value(1, 2, 0.8) + # New row group, for actions of state 1 + builder.new_row_group(2) + builder.add_next_value(2, 3, 0.5) + builder.add_next_value(2, 4, 0.5) + # New row group, for actions of state 2 + builder.new_row_group(3) + builder.add_next_value(3, 5, 0.5) + builder.add_next_value(3, 6, 0.5) + # New row group, for actions of state 3 + builder.new_row_group(4) + builder.add_next_value(4, 7, 0.5) + builder.add_next_value(4, 1, 0.5) + # New row group, for actions of state 4 + builder.new_row_group(5) + builder.add_next_value(5, 8, 0.5) + builder.add_next_value(5, 9, 0.5) + # New row group, for actions of state 5 + builder.new_row_group(6) + builder.add_next_value(6, 10, 0.5) + builder.add_next_value(6, 11, 0.5) + # New row group, for actions of state 6 + builder.new_row_group(7) + builder.add_next_value(7, 2, 0.5) + builder.add_next_value(7, 12, 0.5) + + # final states + for s in range(8,14): + builder.new_row_group(s) + builder.add_next_value(s, s-1, 1) + + # Build transition matrix, set overridden_row_count = nr_states, no row group count since nondet otherwise set overrridenRowGroupCount + transition_matrix = builder.build(nr_choices, nr_states) + + + # State labeling + state_labeling = stormpy.storage.StateLabeling(nr_states) + # Add labels + labels = {'init','one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} + for label in labels: + state_labeling.add_label(label) + + # Set label for single 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) + + # Set label 'done' for multiple states + state_labeling.set_states('done', stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12])) + + # Choice labeling + choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices) + choice_labels = {'a', 'b'} + # Add labels + for label in choice_labels: + choice_labeling.add_label(label) + + # Set label for single choice + choice_labeling.add_label_to_choice('a', 0) + choice_labeling.add_label_to_choice('b', 1) + + # Reward models + reward_models = {} + # Create a vector representing the state-action rewards. + 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] + reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector = action_reward) + + # Collect components + components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models, rate_transitions = False) + components.choice_labeling = choice_labeling + + # Build the model + mdp = stormpy.storage.SparseMdp(components) + print(mdp) + + + +if __name__ == '__main__': + example_building_mdps_01() \ No newline at end of file diff --git a/lib/stormpy/examples/files/ctmc/tiny.sm b/lib/stormpy/examples/files/ctmc/tiny.sm new file mode 100644 index 0000000..df193c8 --- /dev/null +++ b/lib/stormpy/examples/files/ctmc/tiny.sm @@ -0,0 +1,11 @@ +ctmc + +module one + s : [0 .. 3] init 0; + + [] s<3 -> 3/2 : (s'=s+1); + [] s>0 -> 3 : (s'=s-1); +endmodule + +label "empty" = s=0; +label "full" = s=3;