From 4bfa6776ed0e0b0787807dc4ef5cf7aa6edda3a8 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 18 Jan 2017 23:25:48 +0100 Subject: [PATCH] prob01min and prob01max now map on prob01 for dtmcs --- lib/stormpy/__init__.py | 4 ++++ tests/core/test_modelchecking.py | 6 ++++++ 2 files changed, 10 insertions(+) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 3749e51..04e2390 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -76,12 +76,16 @@ def compute_prob01_states(model, phi_states, psi_states): return core._compute_prob01states_double(model, phi_states, psi_states) def compute_prob01min_states(model, phi_states, psi_states): + if model.model_type == ModelType.DTMC: + return compute_prob01_states(model, phi_states, psi_states) if model.supports_parameters: return core._compute_prob01states_min_rationalfunc(model, phi_states, psi_states) else: return core._compute_prob01states_min_double(model, phi_states, psi_states) def compute_prob01max_states(model, phi_states, psi_states): + if model.model_type == ModelType.DTMC: + return compute_prob01_states(model, phi_states, psi_states) if model.supports_parameters: return core._compute_prob01states_max_rationalfunc(model, phi_states, psi_states) else: diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index b4097c1..017b156 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -64,6 +64,12 @@ class TestModelChecking: (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