Binding for constraints

Former-commit-id: 8d697c672c

stormpy/src/core/core.cpp

@@ -30,10 +30,6 @@ class PmcResult {
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
 
-        /*storm::RationalFunction getFunc() {
-            return resultFunction;
-        }*/
-
         std::string toString() {
             std::stringstream stream;
             stream << resultFunction << std::endl;
@@ -142,10 +138,9 @@ void define_core(py::module& m) {
     // PmcResult
     py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking")
         .def("__str__", &PmcResult::toString)
-        //.def("result_function", &PmcResult::getFunc, "Result as rational function")
-        //.def_readwrite("result_function", &PmcResult::resultFunction, "Result as rational function")
-        //.def_readwrite("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
-        //.def_readwrite("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
+        .def_readonly("result_function", &PmcResult::resultFunction, "Result as rational function")
+        .def_readonly("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
+        .def_readonly("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
     ;
 
 }

stormpy/tests/core/test_core.py

@@ -57,6 +57,7 @@ class TestCore:
     
     def test_state_elimination(self):
         import pycarl
+        import pycarl.formula
         program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm")
         prop = "P=? [F \"target\"]"
         formulas = stormpy.parse_formulas_for_program(prop, program)
@@ -67,3 +68,12 @@ class TestCore:
         assert model.model_type() == stormpy.ModelType.DTMC
         assert model.parametric()
         result = stormpy.perform_state_elimination(model, formulas[0])
+        func = result.result_function
+        one = pycarl.FactorizedPolynomial(pycarl.Rational(1))
+        assert func.denominator == one
+        constraints_well_formed = result.constraints_well_formed
+        for constraint in constraints_well_formed:
+            assert constraint.rel() == pycarl.formula.Relation.GEQ or constraint.rel() == pycarl.formula.Relation.LEQ
+        constraints_graph_preserving = result.constraints_graph_preserving
+        for constraint in constraints_graph_preserving:
+            assert constraint.rel() == pycarl.formula.Relation.GREATER