From 95f83a7224adb07ec75131d961a82b09d2eb32da Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 4 Jan 2017 14:24:02 +0100 Subject: [PATCH] Binding for CheckResult --- src/core/modelchecking.cpp | 12 ++------ src/core/result.cpp | 47 ++++++++++++++++++++++++++++++++ tests/core/test_modelchecking.py | 23 +++++++++++----- tests/storage/test_matrix.py | 9 ++++-- 4 files changed, 71 insertions(+), 20 deletions(-) diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 2a1542c..aac2f5a 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -2,15 +2,8 @@ #include "result.h" // Thin wrapper for model checking -double modelChecking(std::shared_ptr> model, std::shared_ptr const& formula) { - std::unique_ptr checkResult = storm::verifySparseModel(model, formula); - 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(); +std::shared_ptr modelChecking(std::shared_ptr> model, std::shared_ptr const& formula) { + return storm::verifySparseModel(model, formula); } // Thin wrapper for parametric model checking @@ -33,7 +26,6 @@ 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")); m.def("compute_prob01states", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); } diff --git a/src/core/result.cpp b/src/core/result.cpp index 10c6fd1..86452b4 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -11,4 +11,51 @@ void define_result(py::module& m) { .def_property_readonly("constraints_graph_preserving", &PmcResult::getConstraintsGraphPreserving, "Constraints ensuring graph preservation") ; + // CheckResult + py::class_> checkResult(m, "_CheckResult", "Base class for all modelchecking results"); + checkResult.def_property_readonly("_symbolic", &storm::modelchecker::CheckResult::isSymbolic, "Flag if result is symbolic") + .def_property_readonly("_hybrid", &storm::modelchecker::CheckResult::isHybrid, "Flag if result is hybrid") + .def_property_readonly("_quantitative", &storm::modelchecker::CheckResult::isQuantitative, "Flag if result is quantitative") + .def_property_readonly("_qualitative", &storm::modelchecker::CheckResult::isQualitative, "Flag if result is qualitative") + .def_property_readonly("_explicit_qualitative", &storm::modelchecker::CheckResult::isExplicitQualitativeCheckResult, "Flag if result is explicit qualitative") + .def_property_readonly("_explicit_quantitative", &storm::modelchecker::CheckResult::isExplicitQuantitativeCheckResult, "Flag if result is explicit quantitative") + .def_property_readonly("_symbolic_qualitative", &storm::modelchecker::CheckResult::isSymbolicQualitativeCheckResult, "Flag if result is symbolic qualitative") + .def_property_readonly("_symbolic_quantitative", &storm::modelchecker::CheckResult::isSymbolicQuantitativeCheckResult, "Flag if result is symbolic quantitative") + .def_property_readonly("_hybrid_quantitative", &storm::modelchecker::CheckResult::isHybridQuantitativeCheckResult, "Flag if result is hybrid quantitative") + .def_property_readonly("_pareto_curve", &storm::modelchecker::CheckResult::isParetoCurveCheckResult, "Flag if result is a pareto curve") + .def_property_readonly("result_for_all_states", &storm::modelchecker::CheckResult::isResultForAllStates, "Flag if result is for all states") + .def("as_qualitative", [](storm::modelchecker::CheckResult const& result) { + return result.asQualitativeCheckResult(); + }, "Convert into qualitative result") + .def("as_quantitative", [](storm::modelchecker::CheckResult const& result) { + return result.asQuantitativeCheckResult(); + }, "Convert into quantitative result") + .def("as_explicit_qualitative", [](storm::modelchecker::CheckResult const& result) { + return result.asExplicitQualitativeCheckResult(); + }, "Convert into explicit qualitative result") + .def("as_explicit_quantitative", [](storm::modelchecker::CheckResult const& result) { + return result.asExplicitQuantitativeCheckResult(); + }, "Convert into explicit quantitative result") + .def("__str__", [](storm::modelchecker::CheckResult const& result) { + std::stringstream stream; + result.writeToStream(stream); + return stream.str(); + }) + ; + + // QualitativeCheckResult + py::class_> qualitativeCheckResult(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results", checkResult); + py::class_>(m, "ExplicitQualitativeCheckResult", "Explicit qualitative model checking result", qualitativeCheckResult) + .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") + ; + + // QuantitativeCheckResult + py::class_, std::shared_ptr>> quantitativeCheckResult(m, "_QuantitativeCheckResult", "Abstract class for quantitative model checking results", checkResult); + py::class_, std::shared_ptr>>(m, "ExplicitQuantitativeCheckResult", "Explicit quantitative model checking result", quantitativeCheckResult) + .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& result, storm::storage::sparse::state_type state) { + return result[state]; + }, py::arg("state"), "Get result for given state") + .def("get_values", &storm::modelchecker::ExplicitQuantitativeCheckResult::getValueVector, "Get model checking result values for all states") + ; + } diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index d6ec19d..68c6347 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -11,8 +11,11 @@ class TestModelChecking: model = stormpy.build_model(program, formulas[0]) assert model.nr_states == 13 assert model.nr_transitions == 20 + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 result = stormpy.model_checking(model, formulas[0]) - assert math.isclose(result, 0.16666666666666663) + assert math.isclose(result.at(initial_state), 0.16666666666666663) def test_model_checking_all_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) @@ -20,9 +23,10 @@ class TestModelChecking: 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]) + result = stormpy.model_checking(model, formulas[0]) + assert result.result_for_all_states reference = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0] - assert all(map(math.isclose, results, reference)) + assert all(map(math.isclose, result.get_values(), reference)) def test_parametric_state_elimination(self): import pycarl @@ -48,10 +52,15 @@ class TestModelChecking: def test_model_checking_prob01(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) - model = stormpy.build_model(program, formulas[0]) - phiStates = stormpy.BitVector(model.nr_states, True) - psiStates = stormpy.BitVector(model.nr_states, [model.nr_states-1]) + formulaPhi = stormpy.parse_formulas("true")[0] + formulaPsi = stormpy.parse_formulas("\"six\"")[0] + model = stormpy.build_model(program, formulaPsi) + phiResult = stormpy.model_checking(model, formulaPhi) + phiStates = phiResult.get_truth_values() + assert phiStates.number_of_set_bits() == model.nr_states + psiResult = stormpy.model_checking(model, formulaPsi) + psiStates = psiResult.get_truth_values() + assert psiStates.number_of_set_bits() == 1 (prob0, prob1) = stormpy.compute_prob01states(model, phiStates, psiStates) assert prob0.number_of_set_bits() == 9 assert prob1.number_of_set_bits() == 1 diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 85f191b..97d7863 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -38,7 +38,8 @@ class TestMatrix: # First model checking formulas = stormpy.parse_formulas("P=? [ F \"one\" ]") result = stormpy.model_checking(model, formulas[0]) - assert math.isclose(result, 0.16666666666666663) + resValue = result.at(model.initial_states[0]) + assert math.isclose(resValue, 0.16666666666666663) # Change probabilities i = 0 @@ -53,7 +54,8 @@ class TestMatrix: assert e.value() == 0.3 or e.value() == 0.7 or e.value() == 1 or e.value() == 0 # Second model checking result = stormpy.model_checking(model, formulas[0]) - assert math.isclose(result, 0.06923076923076932) + resValue = result.at(model.initial_states[0]) + assert math.isclose(resValue, 0.06923076923076932) # Change probabilities again for state in stormpy.state.State(0, model): @@ -65,7 +67,8 @@ class TestMatrix: transition.set_value(0.2) # Third model checking result = stormpy.model_checking(model, formulas[0]) - assert math.isclose(result, 0.3555555555555556) + resValue = result.at(model.initial_states[0]) + assert math.isclose(resValue, 0.3555555555555556) def test_change_parametric_sparse_matrix_modelchecking(self): import stormpy.logic