Fixed min in prob01max_states (#192)

moves-rwth · Nov 25, 2024 · 9b89bfc · 9b89bfc
2 parents b71e71d + b0d56ea
commit 9b89bfc
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 7 deletions.
diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py
@@ -464,7 +464,7 @@ def prob01max_states(model, eventually_formula):
     labelprop = core.Property("label-prop", labelform)
     phiStates = BitVector(model.nr_states, True)
     psiStates = model_checking(model, labelprop).get_truth_values()
-    return compute_prob01min_states(model, phiStates, psiStates)
+    return compute_prob01max_states(model, phiStates, psiStates)
 
 
 def compute_prob01_states(model, phi_states, psi_states):

diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py
@@ -141,16 +141,20 @@ def test_model_checking_prob01(self):
         (prob0, prob1) = stormpy.compute_prob01_states(model, phiStates, psiStates)
         assert prob0.number_of_set_bits() == 9
         assert prob1.number_of_set_bits() == 1
-        (prob0, prob1) = stormpy.compute_prob01min_states(model, phiStates, psiStates)
-        assert prob0.number_of_set_bits() == 9
-        assert prob1.number_of_set_bits() == 1
-        (prob0, prob1) = stormpy.compute_prob01max_states(model, phiStates, psiStates)
-        assert prob0.number_of_set_bits() == 9
-        assert prob1.number_of_set_bits() == 1
         labelprop = stormpy.core.Property("cora", formulaPsi.raw_formula)
         result = stormpy.model_checking(model, labelprop)
         assert result.get_truth_values().number_of_set_bits() == 1
 
+        program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm"))
+        formulas = stormpy.parse_properties_for_prism_program('Pmin=? [ F "finished" & "all_coins_equal_1"]', program)
+        model = stormpy.build_model(program, formulas)
+        prob0, prob1 = stormpy.prob01min_states(model, formulas[0].raw_formula.subformula)
+        assert prob0.number_of_set_bits() == 94
+        assert prob1.number_of_set_bits() == 15
+        prob0, prob1 = stormpy.prob01max_states(model, formulas[0].raw_formula.subformula)
+        assert prob0.number_of_set_bits() == 83
+        assert prob1.number_of_set_bits() == 18
+
     def test_model_checking_ctmc(self):
         model = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn"))
         formulas = stormpy.parse_properties('T=? [ F "failed" ]')