From 540a3f4e0cbb246311c4f864316b8d95dab3d4a0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 19 Jul 2017 15:05:26 +0200 Subject: [PATCH] Refactored constraint collector --- src/core/analysis.cpp | 10 ++++++---- src/core/result.cpp | 13 ------------- src/core/result.h | 1 - src/mod_core.cpp | 3 ++- tests/pars/test_parametric.py | 4 ++-- 5 files changed, 10 insertions(+), 21 deletions(-) diff --git a/src/core/analysis.cpp b/src/core/analysis.cpp index 0684969..e7ab72e 100644 --- a/src/core/analysis.cpp +++ b/src/core/analysis.cpp @@ -4,10 +4,12 @@ // Define python bindings void define_graph_constraints(py::module& m) { - py::class_>(m, "ConstraintCollector", "Collects constraints on parametric Markov chains") - .def(py::init>(), "model"_a) - .def_property_readonly("wellformed_constraints", &storm::analysis::ConstraintCollector::getWellformedConstraints) - .def_property_readonly("graph_preserving_constraints", &storm::analysis::ConstraintCollector::getGraphPreservingConstraints) + + // ConstraintCollector + py::class_, std::shared_ptr>>(m, "ConstraintCollector", "Collector for constraints on parametric Markov chains") + .def(py::init>(), "model") + .def_property_readonly("wellformed_constraints", &storm::analysis::ConstraintCollector::getWellformedConstraints, "Get the constraints ensuring a wellformed model") + .def_property_readonly("graph_preserving_constraints", &storm::analysis::ConstraintCollector::getGraphPreservingConstraints, "Get the constraints ensuring the graph is preserved") ; } diff --git a/src/core/result.cpp b/src/core/result.cpp index 3af4fed..6d7d9ab 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -63,16 +63,3 @@ void define_result(py::module& m) { ; } - -void define_constraints(py::module& m) { - - // ConstraintCollector - py::class_, std::shared_ptr>>(m, "ConstraintCollector", "Collector for constraints") - //.def(py::init>, py::arg("dtmc")) - .def("__init__", [](storm::analysis::ConstraintCollector &instance, storm::models::sparse::Dtmc const& dtmc) -> void { - new (&instance) storm::analysis::ConstraintCollector(dtmc); - }) - .def("wellformed_constraints", &storm::analysis::ConstraintCollector::getWellformedConstraints, "Get the constraints ensuring a wellformed model") - .def("graph_preserving_constraints", &storm::analysis::ConstraintCollector::getGraphPreservingConstraints, "Get the constraints ensuring the graph is preserved") - ; -} diff --git a/src/core/result.h b/src/core/result.h index 70ef135..794000e 100644 --- a/src/core/result.h +++ b/src/core/result.h @@ -4,6 +4,5 @@ #include "common.h" void define_result(py::module& m); -void define_constraints(py::module& m); #endif /* PYTHON_CORE_RESULT_H_ */ diff --git a/src/mod_core.cpp b/src/mod_core.cpp index b86e04a..d98d603 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -5,6 +5,7 @@ #include "core/modelchecking.h" #include "core/bisimulation.h" #include "core/input.h" +#include "core/analysis.h" PYBIND11_MODULE(core, m) { m.doc() = "core"; @@ -20,8 +21,8 @@ PYBIND11_MODULE(core, m) { define_build(m); define_export(m); define_result(m); - define_constraints(m); define_modelchecking(m); define_bisimulation(m); define_input(m); + define_graph_constraints(m); } diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index 435ff66..c5330e3 100644 --- a/tests/pars/test_parametric.py +++ b/tests/pars/test_parametric.py @@ -17,12 +17,12 @@ class TestParametric: 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() + 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() + constraints_graph_preserving = collector.graph_preserving_constraints for formula in constraints_graph_preserving: assert formula.type == FormulaType.CONSTRAINT constraint = formula.get_constraint()