Merge branch '6-make-a-mapping-between-simple-representations-and-spa…

…rsematrix' into main

examples/die.py

@@ -1,14 +1,20 @@
 import stormvogel.model
 
-# Create a new model with the name "Die"
-dtmc = stormvogel.model.new_dtmc("Die")
 
-init = dtmc.get_initial_state()
+def create_die_dtmc():
+    # Create a new model with the name "Die"
+    dtmc = stormvogel.model.new_dtmc("Die")
 
-# From the initial state, add the transition to 6 new states with probability 1/6th.
-init.set_transitions(
-    [(1 / 6, dtmc.new_state(f"rolled{i}", {"rolled": i})) for i in range(6)]
-)
+    init = dtmc.get_initial_state()
 
-# Print the resulting model in dot format.
-print(dtmc.to_dot())
+    # From the initial state, add the transition to 6 new states with probability 1/6th.
+    init.set_transitions(
+        [(1 / 6, dtmc.new_state(f"rolled{i}", {"rolled": i})) for i in range(6)]
+    )
+    return dtmc
+
+
+if __name__ == "__main__":
+    # Print the resulting model in dot format.
+
+    print(create_die_dtmc().to_dot())

examples/monty_hall.py

@@ -1,64 +1,71 @@
 import stormvogel.model
 
-mdp = stormvogel.model.new_mdp("Monty Hall")
 
-init = mdp.get_initial_state()
+def create_monty_hall_mdp():
+    mdp = stormvogel.model.new_mdp("Monty Hall")
 
-# first choose car position
-init.set_transitions(
-    [(1 / 3, mdp.new_state("carchosen", {"car_pos": i})) for i in range(3)]
-)
+    init = mdp.get_initial_state()
 
-# we choose a door in each case
-for s in mdp.get_states_with("carchosen"):
-    s.set_transitions(
-        [
-            (
-                mdp.action(f"open{i}"),
-                mdp.new_state("open", s.features | {"chosen_pos": i}),
-            )
-            for i in range(3)
-        ]
+    # first choose car position
+    init.set_transitions(
+        [(1 / 3, mdp.new_state("carchosen", {"car_pos": i})) for i in range(3)]
     )
 
-# the other goat is revealed
-for s in mdp.get_states_with("open"):
-    car_pos = s.features["car_pos"]
-    chosen_pos = s.features["chosen_pos"]
-    other_pos = {0, 1, 2} - {car_pos, chosen_pos}
-    s.set_transitions(
-        [
-            (
-                1 / len(other_pos),
-                mdp.new_state("goatrevealed", s.features | {"reveal_pos": i}),
-            )
-            for i in other_pos
-        ]
-    )
+    # we choose a door in each case
+    for s in mdp.get_states_with("carchosen"):
+        s.set_transitions(
+            [
+                (
+                    mdp.action(f"open{i}"),
+                    mdp.new_state("open", s.features | {"chosen_pos": i}),
+                )
+                for i in range(3)
+            ]
+        )
+
+    # the other goat is revealed
+    for s in mdp.get_states_with("open"):
+        car_pos = s.features["car_pos"]
+        chosen_pos = s.features["chosen_pos"]
+        other_pos = {0, 1, 2} - {car_pos, chosen_pos}
+        s.set_transitions(
+            [
+                (
+                    1 / len(other_pos),
+                    mdp.new_state("goatrevealed", s.features | {"reveal_pos": i}),
+                )
+                for i in other_pos
+            ]
+        )
 
-# we must choose whether we want to switch
-for s in mdp.get_states_with("goatrevealed"):
-    car_pos = s.features["car_pos"]
-    chosen_pos = s.features["chosen_pos"]
-    reveal_pos = s.features["reveal_pos"]
-    other_pos = list({0, 1, 2} - {reveal_pos, chosen_pos})[0]
-    s.set_transitions(
-        [
-            (
-                mdp.action("stay"),
-                mdp.new_state(
-                    ["done"] + (["target"] if chosen_pos == car_pos else []),
-                    s.features | {"chosen_pos": chosen_pos},
+    # we must choose whether we want to switch
+    for s in mdp.get_states_with("goatrevealed"):
+        car_pos = s.features["car_pos"]
+        chosen_pos = s.features["chosen_pos"]
+        reveal_pos = s.features["reveal_pos"]
+        other_pos = list({0, 1, 2} - {reveal_pos, chosen_pos})[0]
+        s.set_transitions(
+            [
+                (
+                    mdp.action("stay"),
+                    mdp.new_state(
+                        ["done"] + (["target"] if chosen_pos == car_pos else []),
+                        s.features | {"chosen_pos": chosen_pos},
+                    ),
                 ),
-            ),
-            (
-                mdp.action("switch"),
-                mdp.new_state(
-                    ["done"] + (["target"] if other_pos == car_pos else []),
-                    s.features | {"chosen_pos": other_pos},
+                (
+                    mdp.action("switch"),
+                    mdp.new_state(
+                        ["done"] + (["target"] if other_pos == car_pos else []),
+                        s.features | {"chosen_pos": other_pos},
+                    ),
                 ),
-            ),
-        ]
-    )
+            ]
+        )
+
+    return mdp
+
 
-print(mdp.to_dot())
+if __name__ == "__main__":
+    # Print the resulting model in dot format.
+    print(create_monty_hall_mdp().to_dot())

examples/stormpy_mdp.py

@@ -0,0 +1,128 @@
+import stormpy
+
+
+# Knuth's model of a fair die using only fair coins
+def example_building_mdps_01():
+    nr_states = 13
+    nr_choices = 14
+
+    # Transition matrix with custom row grouping: nondeterministic choice over the actions available in states
+    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)
+    # State 1
+    builder.new_row_group(2)
+    builder.add_next_value(2, 3, 0.5)
+    builder.add_next_value(2, 4, 0.5)
+    # State 2
+    builder.new_row_group(3)
+    builder.add_next_value(3, 5, 0.5)
+    builder.add_next_value(3, 6, 0.5)
+    # State 3
+    builder.new_row_group(4)
+    builder.add_next_value(4, 7, 0.5)
+    builder.add_next_value(4, 1, 0.5)
+    # State 4
+    builder.new_row_group(5)
+    builder.add_next_value(5, 8, 0.5)
+    builder.add_next_value(5, 9, 0.5)
+    # State 5
+    builder.new_row_group(6)
+    builder.add_next_value(6, 10, 0.5)
+    builder.add_next_value(6, 11, 0.5)
+    # State 6
+    builder.new_row_group(7)
+    builder.add_next_value(7, 2, 0.5)
+    builder.add_next_value(7, 12, 0.5)
+
+    # Add transitions for the final states
+    for s in range(8, 14):
+        builder.new_row_group(s)
+        builder.add_next_value(s, s - 1, 1)
+
+    transition_matrix = builder.build()
+
+    # 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 labeling of 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 labels
+    choice_labeling.add_label_to_choice("a", 0)
+    choice_labeling.add_label_to_choice("b", 1)
+    print(choice_labeling)
+
+    # 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)
+    return mdp
+
+
+if __name__ == "__main__":
+    example_building_mdps_01()

examples/stormpy_to_stormvogel.py

@@ -33,7 +33,7 @@ def example_building_dtmcs_01():
 
     # Build matrix
     transition_matrix = builder.build()
-    print(transition_matrix)
+    # print(transition_matrix)
 
     # State labeling
     state_labeling = stormpy.storage.StateLabeling(13)
@@ -45,7 +45,7 @@ def example_building_dtmcs_01():
 
     # Set label of state 0
     state_labeling.add_label_to_state("init", 0)
-    print(state_labeling.get_states("init"))
+    # print(state_labeling.get_states("init"))
 
     # Set remaining labels
     state_labeling.add_label_to_state("one", 7)
@@ -57,7 +57,7 @@ def example_building_dtmcs_01():
 
     # Set label 'done' for multiple states
     state_labeling.set_states("done", stormpy.BitVector(13, [7, 8, 9, 10, 11, 12]))
-    print(state_labeling)
+    # print(state_labeling)
 
     # Reward models:
     reward_models = {}
@@ -75,8 +75,8 @@ def example_building_dtmcs_01():
 
     dtmc = stormpy.storage.SparseDtmc(components)
 
-    print(dtmc)
+    return dtmc
 
 
 if __name__ == "__main__":
-    example_building_dtmcs_01()
+    print(example_building_dtmcs_01())