diff --git a/stormpy/src/core/modelchecking.cpp b/stormpy/src/core/modelchecking.cpp index dc1a7d08f..5cd053af8 100644 --- a/stormpy/src/core/modelchecking.cpp +++ b/stormpy/src/core/modelchecking.cpp @@ -40,6 +40,12 @@ double modelChecking(std::shared_ptr> model return checkResult->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; } +// Thin wrapper for model checking for all states +std::vector modelCheckingAll(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr checkResult = storm::verifySparseModel(model, formula); + return checkResult->asExplicitQuantitativeCheckResult().getValueVector(); +} + // Thin wrapper for parametric model checking std::shared_ptr parametricModelChecking(std::shared_ptr> model, std::shared_ptr const& formula) { std::unique_ptr checkResult = storm::verifySparseModel(model, formula); @@ -56,6 +62,7 @@ void define_modelchecking(py::module& m) { // Model checking m.def("_model_checking", &modelChecking, "Perform model checking", py::arg("model"), py::arg("formula")); + m.def("model_checking_all", &modelCheckingAll, "Perform model checking for all states", py::arg("model"), py::arg("formula")); m.def("_parametric_model_checking", ¶metricModelChecking, "Perform parametric model checking", py::arg("model"), py::arg("formula")); // PmcResult diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py index 2a8e54b84..673e489b7 100644 --- a/stormpy/tests/core/test_modelchecking.py +++ b/stormpy/tests/core/test_modelchecking.py @@ -2,7 +2,7 @@ import stormpy import stormpy.logic class TestModelChecking: - def test_state_elimination(self): + def test_model_checking_dtmc(self): program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm") formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_model(program, formulas[0]) @@ -11,6 +11,16 @@ class TestModelChecking: result = stormpy.model_checking(model, formulas[0]) assert result == 0.16666666666666663 + def test_model_checking_all_dtmc(self): + program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm") + formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas[0]) + assert model.nr_states() == 13 + assert model.nr_transitions() == 20 + results = stormpy.model_checking_all(model, formulas[0]) + results_orig = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0] + assert results == results_orig + def test_parametric_state_elimination(self): import pycarl import pycarl.formula