From befee6332f4d16b79c9643afaa744c2a88e9a559 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 24 Oct 2018 17:49:20 +0200 Subject: [PATCH] Added simple filtering for initial states --- src/core/result.cpp | 24 ++++++++++++++++++++++-- tests/core/test_modelchecking.py | 20 ++++++++++++++++++++ tests/core/test_transformation.py | 16 ++++++++-------- 3 files changed, 50 insertions(+), 10 deletions(-) diff --git a/src/core/result.cpp b/src/core/result.cpp index 4e6728d..9827950 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -8,6 +8,17 @@ #include "storm/models/symbolic/StandardRewardModel.h" +template +std::shared_ptr createFilterInitialStatesSparse(std::shared_ptr> model) { + return std::make_unique(model->getInitialStates()); +} + +template +std::shared_ptr createFilterInitialStatesSymbolic(std::shared_ptr> model) { + return std::make_unique>(model->getReachableStates(), model->getInitialStates()); +} + + // Define python bindings void define_result(py::module& m) { @@ -35,6 +46,7 @@ void define_result(py::module& m) { .def("as_explicit_parametric_quantitative", [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQuantitativeCheckResult(); }, "Convert into explicit quantitative result") + .def("filter", &storm::modelchecker::CheckResult::filter, py::arg("filter"), "Filter the result") .def("__str__", [](storm::modelchecker::CheckResult const& result) { std::stringstream stream; result.writeToStream(stream); @@ -45,16 +57,20 @@ void define_result(py::module& m) { // 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("at", [](storm::modelchecker::ExplicitQualitativeCheckResult const& result, storm::storage::sparse::state_type state) { + .def("at", [](storm::modelchecker::ExplicitQualitativeCheckResult const& result, storm::storage::sparse::state_type state) { return result[state]; }, py::arg("state"), "Get result for given state") - .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") + .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") ; py::class_, std::shared_ptr>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult) ; // QuantitativeCheckResult py::class_, std::shared_ptr>> quantitativeCheckResult(m, "_QuantitativeCheckResult", "Abstract class for quantitative model checking results", checkResult); + quantitativeCheckResult.def_property_readonly("min", &storm::modelchecker::QuantitativeCheckResult::getMin, "Minimal value") + .def_property_readonly("max", &storm::modelchecker::QuantitativeCheckResult::getMax, "Maximal value") + ; + 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]; @@ -81,5 +97,9 @@ void define_result(py::module& m) { .def("get_values", &storm::modelchecker::HybridQuantitativeCheckResult::getExplicitValueVector, "Get model checking result values for all states") ; + + m.def("create_filter_initial_states_sparse", &createFilterInitialStatesSparse, "Create a filter for the initial states on a sparse model", py::arg("model")); + m.def("create_filter_initial_states_symbolic", &createFilterInitialStatesSymbolic, "Create a filter for the initial states on a symbolic model", py::arg("model")); + } diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 1d4b15f..2868953 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -118,6 +118,22 @@ class TestModelChecking: result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 4.166666667) + def test_filter(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas) + 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.at(initial_state), 1 / 6) + filter = stormpy.create_filter_initial_states_sparse(model) + result.filter(filter) + assert result.min == result.max + assert math.isclose(result.min, 1 / 6) + def test_model_checking_prism_dd_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) @@ -126,6 +142,10 @@ class TestModelChecking: assert model.nr_transitions == 20 result = stormpy.check_model_dd(model, formulas[0]) assert type(result) is stormpy.SymbolicQuantitativeCheckResult + filter = stormpy.create_filter_initial_states_symbolic(model) + result.filter(filter) + assert result.min == result.max + assert math.isclose(result.min, 1 / 6, rel_tol=1e-6) def test_model_checking_prism_hybrid_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) diff --git a/tests/core/test_transformation.py b/tests/core/test_transformation.py index 562f85f..e1a322e 100644 --- a/tests/core/test_transformation.py +++ b/tests/core/test_transformation.py @@ -6,18 +6,18 @@ from helpers.helper import get_example_path class TestTransformation: def test_transform_symbolic_dtmc_to_sparse(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) - model = stormpy.build_symbolic_model(program) - assert model.nr_states == 8607 - assert model.nr_transitions == 15113 - assert model.model_type == stormpy.ModelType.DTMC - assert not model.supports_parameters - assert type(model) is stormpy.SymbolicSylvanDtmc - symbolic_model = stormpy.transform_to_sparse_model(model) + symbolic_model = stormpy.build_symbolic_model(program) assert symbolic_model.nr_states == 8607 assert symbolic_model.nr_transitions == 15113 assert symbolic_model.model_type == stormpy.ModelType.DTMC assert not symbolic_model.supports_parameters - assert type(symbolic_model) is stormpy.SparseDtmc + assert type(symbolic_model) is stormpy.SymbolicSylvanDtmc + sparse_model = stormpy.transform_to_sparse_model(symbolic_model) + assert sparse_model.nr_states == 8607 + assert sparse_model.nr_transitions == 15113 + assert sparse_model.model_type == stormpy.ModelType.DTMC + assert not sparse_model.supports_parameters + assert type(sparse_model) is stormpy.SparseDtmc def test_transform_symbolic_parametric_dtmc_to_sparse(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm"))