From 2cb060dd2ac9c2f817737c580777101e4081637f Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 3 Jan 2017 10:12:55 +0100
Subject: [PATCH] Moved results in own class
---
src/core/modelchecking.cpp | 44 +-------------------------------------
src/core/result.cpp | 14 ++++++++++++
src/core/result.h | 42 ++++++++++++++++++++++++++++++++++++
src/mod_core.cpp | 2 ++
4 files changed, 59 insertions(+), 43 deletions(-)
create mode 100644 src/core/result.cpp
create mode 100644 src/core/result.h
diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp
index 84488c2..2a1542c 100644
--- a/src/core/modelchecking.cpp
+++ b/src/core/modelchecking.cpp
@@ -1,38 +1,5 @@
#include "modelchecking.h"
-
-// Class holding the model checking result
-class PmcResult {
- public:
- storm::RationalFunction resultFunction;
- std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
- std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
-
- storm::RationalFunction getResultFunction() const {
- return resultFunction;
- }
-
- std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> getConstraintsWellFormed() const {
- return constraintsWellFormed;
- }
-
- std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> getConstraintsGraphPreserving() const {
- return constraintsGraphPreserving;
- }
-
- std::string toString() {
- std::stringstream stream;
- stream << resultFunction << std::endl;
- stream << "Well formed constraints:" << std::endl;
- for (auto constraint : constraintsWellFormed) {
- stream << constraint << std::endl;
- }
- stream << "Graph preserving constraints:" << std::endl;
- for (auto constraint : constraintsGraphPreserving) {
- stream << constraint << std::endl;
- }
- return stream.str();
- }
-};
+#include "result.h"
// Thin wrapper for model checking
double modelChecking(std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
@@ -69,13 +36,4 @@ void define_modelchecking(py::module& m) {
m.def("model_checking_all", &modelCheckingAll, "Perform model checking for all states", py::arg("model"), py::arg("formula"));
m.def("_parametric_model_checking", ¶metricModelChecking, "Perform parametric model checking", py::arg("model"), py::arg("formula"));
m.def("compute_prob01states", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));
-
- // PmcResult
- py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking")
- .def("__str__", &PmcResult::toString)
- .def_property_readonly("result_function", &PmcResult::getResultFunction, "Result as rational function")
- .def_property_readonly("constraints_well_formed", &PmcResult::getConstraintsWellFormed, "Constraints ensuring well-formed probabilities")
- .def_property_readonly("constraints_graph_preserving", &PmcResult::getConstraintsGraphPreserving, "Constraints ensuring graph preservation")
- ;
-
}
diff --git a/src/core/result.cpp b/src/core/result.cpp
new file mode 100644
index 0000000..10c6fd1
--- /dev/null
+++ b/src/core/result.cpp
@@ -0,0 +1,14 @@
+#include "result.h"
+
+// Define python bindings
+void define_result(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_property_readonly("result_function", &PmcResult::getResultFunction, "Result as rational function")
+ .def_property_readonly("constraints_well_formed", &PmcResult::getConstraintsWellFormed, "Constraints ensuring well-formed probabilities")
+ .def_property_readonly("constraints_graph_preserving", &PmcResult::getConstraintsGraphPreserving, "Constraints ensuring graph preservation")
+ ;
+
+}
diff --git a/src/core/result.h b/src/core/result.h
new file mode 100644
index 0000000..4dfad74
--- /dev/null
+++ b/src/core/result.h
@@ -0,0 +1,42 @@
+#ifndef PYTHON_CORE_RESULT_H_
+#define PYTHON_CORE_RESULT_H_
+
+#include "common.h"
+
+// Class holding the parametric model checking result
+class PmcResult {
+ public:
+ storm::RationalFunction resultFunction;
+ std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
+ std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
+
+ storm::RationalFunction getResultFunction() const {
+ return resultFunction;
+ }
+
+ std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> getConstraintsWellFormed() const {
+ return constraintsWellFormed;
+ }
+
+ std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> getConstraintsGraphPreserving() const {
+ return constraintsGraphPreserving;
+ }
+
+ std::string toString() {
+ std::stringstream stream;
+ stream << resultFunction << std::endl;
+ stream << "Well formed constraints:" << std::endl;
+ for (auto constraint : constraintsWellFormed) {
+ stream << constraint << std::endl;
+ }
+ stream << "Graph preserving constraints:" << std::endl;
+ for (auto constraint : constraintsGraphPreserving) {
+ stream << constraint << std::endl;
+ }
+ return stream.str();
+ }
+};
+
+void define_result(py::module& m);
+
+#endif /* PYTHON_CORE_RESULT_H_ */
diff --git a/src/mod_core.cpp b/src/mod_core.cpp
index b7792f4..8f96262 100644
--- a/src/mod_core.cpp
+++ b/src/mod_core.cpp
@@ -1,6 +1,7 @@
#include "common.h"
#include "core/core.h"
+#include "core/result.h"
#include "core/modelchecking.h"
#include "core/bisimulation.h"
#include "core/input.h"
@@ -17,6 +18,7 @@ PYBIND11_PLUGIN(core) {
define_core(m);
define_parse(m);
define_build(m);
+ define_result(m);
define_modelchecking(m);
define_bisimulation(m);
define_input(m);