From 7b2b2705797733237437159ba23689997640e811 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Thu, 12 May 2016 14:43:10 +0200
Subject: [PATCH] Binding for constraints

Former-commit-id: 8d697c672c521f9ddee0d88ca13de7e4c80a42be
---
 stormpy/src/core/core.cpp       | 11 +++--------
 stormpy/tests/core/test_core.py | 10 ++++++++++
 2 files changed, 13 insertions(+), 8 deletions(-)

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