simplified examples

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

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

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

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

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;