Browse Source

Moved results in own class

refactoring
Matthias Volk 8 years ago
parent
commit
2cb060dd2a
  1. 44
      src/core/modelchecking.cpp
  2. 14
      src/core/result.cpp
  3. 42
      src/core/result.h
  4. 2
      src/mod_core.cpp

44
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", &parametricModelChecking, "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")
;
}

14
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")
;
}

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

2
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);

Loading…
Cancel
Save