Added simple filtering for initial states

src/core/result.cpp

@@ -8,6 +8,17 @@
 
 #include "storm/models/symbolic/StandardRewardModel.h"
 
+template<typename ValueType>
+std::shared_ptr<storm::modelchecker::QualitativeCheckResult> createFilterInitialStatesSparse(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) {
+    return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->getInitialStates());
+}
+
+template<storm::dd::DdType DdType, typename ValueType>
+std::shared_ptr<storm::modelchecker::QualitativeCheckResult> createFilterInitialStatesSymbolic(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> model) {
+   return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(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<storm::RationalFunction>();
             }, "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_<storm::modelchecker::QualitativeCheckResult, std::shared_ptr<storm::modelchecker::QualitativeCheckResult>> qualitativeCheckResult(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results", checkResult);
     py::class_<storm::modelchecker::ExplicitQualitativeCheckResult, std::shared_ptr<storm::modelchecker::ExplicitQualitativeCheckResult>>(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_<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>, std::shared_ptr<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult)
     ;
 
     // QuantitativeCheckResult
     py::class_<storm::modelchecker::QuantitativeCheckResult<double>, std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<double>>> quantitativeCheckResult(m, "_QuantitativeCheckResult", "Abstract class for quantitative model checking results", checkResult);
+    quantitativeCheckResult.def_property_readonly("min", &storm::modelchecker::QuantitativeCheckResult<double>::getMin, "Minimal value")
+        .def_property_readonly("max", &storm::modelchecker::QuantitativeCheckResult<double>::getMax, "Maximal value")
+    ;
+
     py::class_<storm::modelchecker::ExplicitQuantitativeCheckResult<double>, std::shared_ptr<storm::modelchecker::ExplicitQuantitativeCheckResult<double>>>(m, "ExplicitQuantitativeCheckResult", "Explicit quantitative model checking result", quantitativeCheckResult)
         .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult<double> 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<storm::dd::DdType::Sylvan, storm::RationalFunction>::getExplicitValueVector, "Get model checking result values for all states")
     ;
 
+
+    m.def("create_filter_initial_states_sparse", &createFilterInitialStatesSparse<double>, "Create a filter for the initial states on a sparse model", py::arg("model"));
+    m.def("create_filter_initial_states_symbolic", &createFilterInitialStatesSymbolic<storm::dd::DdType::Sylvan, double>, "Create a filter for the initial states on a symbolic model", py::arg("model"));
+
 }
 

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"))

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"))