small changes and added one more test

stormvogel/model_checking.py

@@ -5,7 +5,7 @@
 
 
 def model_checking(
-    model: stormvogel.model.Model, prop: str, scheduler: bool = False
+    model: stormvogel.model.Model, prop: str, scheduler: bool = True
 ) -> stormvogel.result.Result | None:
     """
     Instead of calling this function, the stormpy model checker can be used by first mapping a model to a stormpy model,
@@ -16,10 +16,13 @@ def model_checking(
     prop = stormpy.parse_properties(prop)
 
     stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(model)
-    stormpy_result = stormpy.model_checking(
-        stormpy_model, prop[0], extract_scheduler=scheduler
-    )
-    assert model is not None
+
+    if model.supports_actions() and scheduler:
+        stormpy_result = stormpy.model_checking(
+            stormpy_model, prop[0], extract_scheduler=True
+        )
+    else:
+        stormpy_result = stormpy.model_checking(stormpy_model, prop[0])
 
     # 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)

tests/test_model_checking.py

@@ -1,9 +1,12 @@
 import stormvogel.model_checking
 import examples.monty_hall
+import examples.die
 import stormpy
 
 
-def test_mdp_model_checking():
+def test_model_checking():
+    # TODO this test is maybe too trivial?
+
     # we get our result using the stormvogel model checker function indirectly
     mdp = examples.monty_hall.create_monty_hall_mdp()
     prop = 'Pmin=? [F "done"]'
@@ -16,10 +19,23 @@ def test_mdp_model_checking():
     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
+    )
+
+    # now we do it for a dtmc:
+    dtmc = examples.die.create_die_dtmc()
+    prop = 'Pmin=? [F "rolled1"]'
+    result = stormvogel.model_checking.model_checking(dtmc, prop, True)
+
+    # indirectly:
+    prop = stormpy.parse_properties(prop)
+    stormpy_model = stormvogel.mapping.stormvogel_to_stormpy(dtmc)
+    stormpy_result = stormpy.model_checking(stormpy_model, prop[0])
+
     stormvogel_model = stormvogel.mapping.stormpy_to_stormvogel(stormpy_model)
 
     stormvogel_result = stormvogel.result.convert_model_checking_result(