diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 8e526fb..bd76cf1 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -8,12 +8,10 @@ std::shared_ptr modelChecking(std::shared_ptr< // 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); - std::shared_ptr result = std::make_shared(); - result->resultFunction = checkResult->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + std::shared_ptr result = std::make_shared(storm::verifySparseModel(model, formula)); storm::models::sparse::Dtmc::ConstraintCollector constraintCollector(*(model->template as>())); - result->constraintsWellFormed = constraintCollector.getWellformedConstraints(); - result->constraintsGraphPreserving = constraintCollector.getGraphPreservingConstraints(); + result->setConstraintsWellFormed(constraintCollector.getWellformedConstraints()); + result->setConstraintsGraphPreserving(constraintCollector.getGraphPreservingConstraints()); return result; } diff --git a/src/core/result.cpp b/src/core/result.cpp index fb90420..1e0a762 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -4,9 +4,9 @@ void define_result(py::module& m) { // PmcResult - py::class_>(m, "PmcResult", "Holds the results after parametric model checking") + py::class_>(m, "PmcResult", "Holds the result and additional constraints after parametric model checking") .def("__str__", &PmcResult::toString) - .def_property_readonly("result_function", &PmcResult::getResultFunction, "Result as rational function") + .def_property_readonly("result", &PmcResult::getResult, "Result") .def_property_readonly("constraints_well_formed", &PmcResult::getConstraintsWellFormed, "Constraints ensuring well-formed probabilities") .def_property_readonly("constraints_graph_preserving", &PmcResult::getConstraintsGraphPreserving, "Constraints ensuring graph preservation") ; @@ -31,6 +31,9 @@ void define_result(py::module& m) { .def("as_explicit_quantitative", [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQuantitativeCheckResult(); }, "Convert into explicit quantitative result") + .def("as_explicit_parametric_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); @@ -52,5 +55,12 @@ void define_result(py::module& m) { }, py::arg("state"), "Get result for given state") .def("get_values", &storm::modelchecker::ExplicitQuantitativeCheckResult::getValueVector, "Get model checking result values for all states") ; + py::class_, std::shared_ptr>> parametricQuantitativeCheckResult(m, "_ParametricQuantitativeCheckResult", "Abstract class for parametric quantitative model checking results", checkResult); + py::class_, std::shared_ptr>>(m, "ExplicitParametricQuantitativeCheckResult", "Explicit parametric quantitative model checking result", parametricQuantitativeCheckResult) + .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/src/core/result.h b/src/core/result.h index 4dfad74..97cd80a 100644 --- a/src/core/result.h +++ b/src/core/result.h @@ -5,26 +5,38 @@ // Class holding the parametric model checking result class PmcResult { - public: - storm::RationalFunction resultFunction; + private: + std::shared_ptr checkResult; std::unordered_set> constraintsWellFormed; std::unordered_set> constraintsGraphPreserving; - storm::RationalFunction getResultFunction() const { - return resultFunction; + public: + PmcResult(std::shared_ptr _checkResult) : checkResult(_checkResult) { + } + + std::shared_ptr getResult() { + return checkResult; } std::unordered_set> getConstraintsWellFormed() const { return constraintsWellFormed; } + void setConstraintsWellFormed(std::unordered_set> _constraintsWellFormed) { + this->constraintsWellFormed = _constraintsWellFormed; + } + std::unordered_set> getConstraintsGraphPreserving() const { return constraintsGraphPreserving; } + + void setConstraintsGraphPreserving(std::unordered_set> _constraintsGraphPreserving) { + this->constraintsGraphPreserving = _constraintsGraphPreserving; + } std::string toString() { std::stringstream stream; - stream << resultFunction << std::endl; + stream << *checkResult << std::endl; stream << "Well formed constraints:" << std::endl; for (auto constraint : constraintsWellFormed) { stream << constraint << std::endl; diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 60766b6..0777e3d 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -40,8 +40,10 @@ class TestModelChecking: assert model.nr_transitions == 803 assert model.model_type == stormpy.ModelType.DTMC assert model.has_parameters + initial_state = model.initial_states[0] + assert initial_state == 0 result = stormpy.model_checking(model, formulas[0]) - func = result.result_function + func = result.result.at(initial_state) one = pycarl.FactorizedPolynomial(pycarl.Rational(1)) assert func.denominator == one constraints_well_formed = result.constraints_well_formed diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index b2c084c..3b9c610 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -77,6 +77,8 @@ class TestMatrix: program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program) model = stormpy.build_parametric_model(program, formulas) + initial_state = model.initial_states[0] + assert initial_state == 0 matrix = model.transition_matrix # Check matrix one_pol = pycarl.Rational(1) @@ -86,7 +88,8 @@ class TestMatrix: assert e.value() == one or len(e.value().gather_variables()) > 0 # First model checking result = stormpy.model_checking(model, formulas[0]) - assert len(result.result_function.gather_variables()) > 0 + ratFunc = result.result.at(initial_state) + assert len(ratFunc.gather_variables()) > 0 # Change probabilities two_pol = pycarl.Rational(2) @@ -99,4 +102,5 @@ class TestMatrix: assert e.value() == new_val or e.value() == one # Second model checking result = stormpy.model_checking(model, formulas[0]) - assert len(result.result_function.gather_variables()) == 0 + ratFunc = result.result.at(initial_state) + assert len(ratFunc.gather_variables()) == 0