Bindings for graph constraints

src/core/result.cpp

@@ -1,4 +1,5 @@
 #include "result.h"
+#include "storm/analysis/GraphConditions.h"
 
 // Thin wrapper
 template<typename ValueType>
@@ -60,5 +61,18 @@ void define_result(py::module& m) {
         }, py::arg("state"), "Get result for given state")
         .def("get_values", &getValues<storm::RationalFunction>, "Get model checking result values for all states")
     ;
+}
+
+
+void define_constraints(py::module& m) {
 
+    // ConstraintCollector
+    py::class_<storm::analysis::ConstraintCollector<storm::RationalFunction>, std::shared_ptr<storm::analysis::ConstraintCollector<storm::RationalFunction>>>(m, "ConstraintCollector", "Collector for constraints")
+       //.def(py::init<storm::models::sparse::Dtmc<storm::RationalFunction>>, py::arg("dtmc"))
+       .def("__init__", [](storm::analysis::ConstraintCollector<storm::RationalFunction> &instance, storm::models::sparse::Dtmc<storm::RationalFunction> const& dtmc) -> void {
+                new (&instance) storm::analysis::ConstraintCollector<storm::RationalFunction>(dtmc);
+            })
+       .def("wellformed_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getWellformedConstraints, "Get the constraints ensuring a wellformed model")
+       .def("graph_preserving_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getGraphPreservingConstraints, "Get the constraints ensuring the graph is preserved")
+    ;
 }

src/core/result.h

@@ -3,8 +3,7 @@
 
 #include "common.h"
 
-
-
 void define_result(py::module& m);
+void define_constraints(py::module& m);
 
 #endif /* PYTHON_CORE_RESULT_H_ */

src/mod_core.cpp

@@ -21,6 +21,7 @@ PYBIND11_PLUGIN(core) {
     define_build(m);
     define_export(m);
     define_result(m);
+    define_constraints(m);
     define_modelchecking(m);
     define_bisimulation(m);
     define_input(m);

tests/core/test_parametric.py

@@ -0,0 +1,29 @@
+import stormpy
+import stormpy.logic
+from helpers.helper import get_example_path
+
+class TestParametric:
+
+    def test_constraints_collector(self):
+        #TODO decide whether we have CLN or GMP based on some flag in stormpy.
+        import pycarl
+        import pycarl.cln
+        import pycarl.gmp
+        from pycarl.formula import FormulaType, Relation
+        import pycarl.cln.formula
+        import pycarl.gmp.formula
+        program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
+        prop = "P=? [F s=5]"
+        formulas = stormpy.parse_properties_for_prism_program(prop, program)
+        model = stormpy.build_parametric_model(program, formulas)
+        collector = stormpy.ConstraintCollector(model)
+        constraints_well_formed = collector.wellformed_constraints()
+        for formula in constraints_well_formed:
+            assert formula.type == FormulaType.CONSTRAINT
+            constraint = formula.get_constraint()
+            assert constraint.relation == Relation.LEQ
+        constraints_graph_preserving = collector.graph_preserving_constraints()
+        for formula in constraints_graph_preserving:
+            assert formula.type == FormulaType.CONSTRAINT
+            constraint = formula.get_constraint()
+            assert constraint.relation == Relation.NEQ