diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index 842c8a067..98d9332c6 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -30,10 +30,6 @@ class PmcResult { std::unordered_set> constraintsWellFormed; std::unordered_set> 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_>(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") ; } diff --git a/stormpy/tests/core/test_core.py b/stormpy/tests/core/test_core.py index ece3771fc..416b7e894 100644 --- a/stormpy/tests/core/test_core.py +++ b/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