PmcResult is CheckResult + constraints

src/core/modelchecking.cpp

@@ -8,12 +8,10 @@ std::shared_ptr<storm::modelchecker::CheckResult> modelChecking(std::shared_ptr<
 
 // Thin wrapper for parametric model checking
 std::shared_ptr<PmcResult> parametricModelChecking(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
-    std::unique_ptr<storm::modelchecker::CheckResult> checkResult = storm::verifySparseModel<storm::RationalFunction>(model, formula);
-    std::shared_ptr<PmcResult> result = std::make_shared<PmcResult>();
-    result->resultFunction = checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()];
+    std::shared_ptr<PmcResult> result = std::make_shared<PmcResult>(storm::verifySparseModel<storm::RationalFunction>(model, formula));
     storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector constraintCollector(*(model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>()));
-    result->constraintsWellFormed = constraintCollector.getWellformedConstraints();
-    result->constraintsGraphPreserving = constraintCollector.getGraphPreservingConstraints();
+    result->setConstraintsWellFormed(constraintCollector.getWellformedConstraints());
+    result->setConstraintsGraphPreserving(constraintCollector.getGraphPreservingConstraints());
     return result;
 }
 

src/core/result.cpp

@@ -4,9 +4,9 @@
 void define_result(py::module& m) {
 
     // PmcResult
-    py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking")
+    py::class_<PmcResult, std::shared_ptr<PmcResult>>(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<double>();
             }, "Convert into explicit quantitative result")
+        .def("as_explicit_parametric_quantitative", [](storm::modelchecker::CheckResult const& result) {
+                return result.asExplicitQuantitativeCheckResult<storm::RationalFunction>();
+            }, "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<double>::getValueVector, "Get model checking result values for all states")
     ;
+    py::class_<storm::modelchecker::QuantitativeCheckResult<storm::RationalFunction>, std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<storm::RationalFunction>>> parametricQuantitativeCheckResult(m, "_ParametricQuantitativeCheckResult", "Abstract class for parametric quantitative model checking results", checkResult);
+    py::class_<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>, std::shared_ptr<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>>>(m, "ExplicitParametricQuantitativeCheckResult", "Explicit parametric quantitative model checking result", parametricQuantitativeCheckResult)
+        .def("at", [](storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction> 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<storm::RationalFunction>::getValueVector, "Get model checking result values for all states")
+    ;
 
 }

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<storm::modelchecker::CheckResult> checkResult;
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
 
-        storm::RationalFunction getResultFunction() const {
-            return resultFunction;
+    public:
+        PmcResult(std::shared_ptr<storm::modelchecker::CheckResult> _checkResult) : checkResult(_checkResult) {
+        }
+
+        std::shared_ptr<storm::modelchecker::CheckResult> getResult() {
+            return checkResult;
         }
 
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> getConstraintsWellFormed() const {
             return constraintsWellFormed;
         }
 
+        void setConstraintsWellFormed(std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> _constraintsWellFormed) {
+            this->constraintsWellFormed = _constraintsWellFormed;
+        }
+
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> getConstraintsGraphPreserving() const {
             return constraintsGraphPreserving;
         }
+        
+        void setConstraintsGraphPreserving(std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> _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;

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

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