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> constraintsWellFormed; - std::unordered_set> constraintsGraphPreserving; - - storm::RationalFunction getResultFunction() const { - return resultFunction; - } - - std::unordered_set> getConstraintsWellFormed() const { - return constraintsWellFormed; - } - - std::unordered_set> 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> model, std::shared_ptr 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_>(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_>(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> constraintsWellFormed; + std::unordered_set> constraintsGraphPreserving; + + storm::RationalFunction getResultFunction() const { + return resultFunction; + } + + std::unordered_set> getConstraintsWellFormed() const { + return constraintsWellFormed; + } + + std::unordered_set> 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);