Browse Source

Refactored constraint collector

refactoring
Matthias Volk 8 years ago
parent
commit
540a3f4e0c
  1. 10
      src/core/analysis.cpp
  2. 13
      src/core/result.cpp
  3. 1
      src/core/result.h
  4. 3
      src/mod_core.cpp
  5. 4
      tests/pars/test_parametric.py

10
src/core/analysis.cpp

@ -4,10 +4,12 @@
// Define python bindings
void define_graph_constraints(py::module& m) {
py::class_<storm::analysis::ConstraintCollector<storm::RationalFunction>>(m, "ConstraintCollector", "Collects constraints on parametric Markov chains")
.def(py::init<storm::models::sparse::Dtmc<storm::RationalFunction>>(), "model"_a)
.def_property_readonly("wellformed_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getWellformedConstraints)
.def_property_readonly("graph_preserving_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getGraphPreservingConstraints)
// ConstraintCollector
py::class_<storm::analysis::ConstraintCollector<storm::RationalFunction>, std::shared_ptr<storm::analysis::ConstraintCollector<storm::RationalFunction>>>(m, "ConstraintCollector", "Collector for constraints on parametric Markov chains")
.def(py::init<storm::models::sparse::Dtmc<storm::RationalFunction>>(), "model")
.def_property_readonly("wellformed_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getWellformedConstraints, "Get the constraints ensuring a wellformed model")
.def_property_readonly("graph_preserving_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getGraphPreservingConstraints, "Get the constraints ensuring the graph is preserved")
;
}

13
src/core/result.cpp

@ -63,16 +63,3 @@ void define_result(py::module& m) {
;
}
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")
;
}

1
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_ */

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

4
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()

Loading…
Cancel
Save