works with schedulers + created first test

stormvogel/model_checking.py

@@ -20,20 +20,15 @@ def model_checking(
         stormpy_model, prop[0], extract_scheduler=scheduler
     )
     assert model is not None
-    stormvogel_result = stormvogel.result.convert_model_checking_result(
-        model, stormpy_result
-    )
 
-    return stormvogel_result
+    # to get the correct action labels, we need to convert the model back to stormvogel instead of
+    # using the initial one for now. (otherwise schedulers won't work)
+    stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(stormpy_model)
 
+    assert stormvogel_model is not None
 
-if __name__ == "__main__":
-    dtmc = stormvogel.model.new_dtmc("Die")
-    init = dtmc.get_initial_state()
-    init.set_transitions(
-        [(1 / 6, dtmc.new_state(f"rolled{i}", {"rolled": i})) for i in range(6)]
+    stormvogel_result = stormvogel.result.convert_model_checking_result(
+        stormvogel_model, stormpy_result
     )
-    dtmc.add_self_loops()
 
-    stormvogel_results = model_checking(dtmc, 'Pmin=? [F "rolled1"]')
-    print(stormvogel_results)
+    return stormvogel_result

stormvogel/result.py

@@ -42,6 +42,11 @@ def __str__(self) -> str:
             add = ""
         return add + "taken actions: " + str(self.taken_actions)
 
+    def __eq__(self, other) -> bool:
+        if isinstance(other, Scheduler):
+            return self.taken_actions == other.taken_actions
+        return False
+
 
 class Result:
     """Result object represents the model checking results for a given model
@@ -110,15 +115,22 @@ def generate_induced_dtmc(self) -> stormvogel.model.Model | None:
                 raise RuntimeError("This result does not have a scheduler")
 
     def __str__(self) -> str:
-        s = {}
-        if self.scheduler is not None:
-            for index, action in enumerate(self.scheduler.taken_actions.values()):
-                s[index] = str(list(action.labels))
-
         add = ""
         if self.model.name is not None:
             add = "model: " + str(self.model.name) + "\n"
-        return add + "values: \n " + str(self.values) + "\n" + "scheduler: \n " + str(s)
+        return (
+            add
+            + "values: \n "
+            + str(self.values)
+            + "\n"
+            + "scheduler: \n "
+            + str(self.scheduler)
+        )
+
+    def __eq__(self, other) -> bool:
+        if isinstance(other, Result):
+            return self.values == other.values and self.scheduler == other.scheduler
+        return False
 
 
 def convert_model_checking_result(
@@ -148,17 +160,3 @@ def convert_model_checking_result(
         stormvogel_result.add_scheduler(stormpy_result.scheduler)
 
     return stormvogel_result
-
-
-if __name__ == "__main__":
-    path = stormpy.examples.files.prism_dtmc_die
-    prism_program = stormpy.parse_prism_program(path)
-    formula_str = "P=? [F s=7 & d=2]"
-    properties = stormpy.parse_properties(formula_str, prism_program)
-
-    model = stormpy.build_model(prism_program, properties)
-    result = stormpy.model_checking(model, properties[0])
-    print(type(result))
-    stormvogel_model = stormvogel.map.stormpy_to_stormvogel(model)
-    if stormvogel_model is not None:
-        convert_model_checking_result(stormvogel_model, result)

tests/test_model_checking.py

@@ -0,0 +1,29 @@
+import stormvogel.model_checking
+import examples.monty_hall
+import stormpy
+
+
+def test_mdp_model_checking():
+    # we get our result using the stormvogel model checker function indirectly
+    mdp = examples.monty_hall.create_monty_hall_mdp()
+    prop = 'Pmin=? [F "done"]'
+    result = stormvogel.model_checking.model_checking(mdp, prop, True)
+
+    # and directly
+    prop = stormpy.parse_properties(prop)
+
+    stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(mdp)
+    stormpy_result = stormpy.model_checking(
+        stormpy_model, prop[0], extract_scheduler=True
+    )
+    assert mdp is not None
+
+    # to get the correct action labels, we need to convert the model back to stormvogel instead of
+    # using the initial one for now. (otherwise schedulers won't work)
+    stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(stormpy_model)
+
+    stormvogel_result = stormvogel.result.convert_model_checking_result(
+        stormvogel_model, stormpy_result
+    )
+
+    assert result == stormvogel_result