diff --git a/src/python/boostPyExtension.h b/src/python/boostPyExtension.h index bfdc780ca..ad3a36f37 100644 --- a/src/python/boostPyExtension.h +++ b/src/python/boostPyExtension.h @@ -4,16 +4,16 @@ namespace boost { namespace python { namespace converter { - template - PyObject* shared_ptr_to_python(std::shared_ptr const& x) - { - if (!x) - return python::detail::none(); - else if (shared_ptr_deleter* d = std::get_deleter(x)) - return incref( d->owner.get() ); - else - return converter::registered const&>::converters.to_python(&x); - } + template + PyObject* shared_ptr_to_python(std::shared_ptr const& x) + { + if (!x) + return python::detail::none(); + else if (shared_ptr_deleter* d = std::get_deleter(x)) + return incref( d->owner.get() ); + else + return converter::registered const&>::converters.to_python(&x); + } /// @brief Adapter a non-member function that returns a unique_ptr to /// a python function object that returns a raw pointer but @@ -41,4 +41,4 @@ namespace boost { namespace python { namespace converter { ); } - }}} // namespace boost::python::converter +}}} // namespace boost::python::converter diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp index c1eed04fe..6a35d6b32 100644 --- a/src/python/storm-core.cpp +++ b/src/python/storm-core.cpp @@ -8,6 +8,7 @@ #include "helpers.h" #include "boostPyExtension.h" +// Holds the rational function and constraints after parametric model checking class PmcResult { public: storm::RationalFunction resultFunction; @@ -15,22 +16,23 @@ public: std::unordered_set> constraintsGraphPreserving; }; +// Thin wrapper for model building std::shared_ptr buildModel(storm::prism::Program const& program, std::shared_ptr const& formula) { return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; } +// Thin wrapper for parametric state elimination std::shared_ptr performStateElimination(std::shared_ptr> model, std::shared_ptr const& formula) { - std::cout << "Perform state elimination" << std::endl; std::unique_ptr checkResult = storm::verifySparseModel(model, formula); std::shared_ptr result = std::make_shared(); result->resultFunction = (checkResult->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]); - std::cout << "Result: " << result->resultFunction << std::endl; storm::models::sparse::Dtmc::ConstraintCollector constraintCollector(*(model->template as>())); result->constraintsWellFormed = constraintCollector.getWellformedConstraints(); result->constraintsGraphPreserving = constraintCollector.getGraphPreservingConstraints(); return result; } +// Thin wrapper for initializing void setupStormLib(std::string const& args) { storm::utility::setUp(); storm::settings::SettingsManager::manager().setFromString(args); @@ -39,9 +41,7 @@ void setupStormLib(std::string const& args) { BOOST_PYTHON_MODULE(_core) { using namespace boost::python; - def("setUp", setupStormLib); - - + def("set_up", setupStormLib); //////////////////////////////////////////// @@ -49,7 +49,6 @@ BOOST_PYTHON_MODULE(_core) //////////////////////////////////////////// defineClass("Program", "") - //class_("Program") .add_property("nr_modules", &storm::prism::Program::getNumberOfModules) ; @@ -57,7 +56,7 @@ BOOST_PYTHON_MODULE(_core) //////////////////////////////////////////// // PmcResult //////////////////////////////////////////// - class_, boost::noncopyable>("PmcResult", "") + class_, boost::noncopyable>("PmcResult", "Holds the results after parametric model checking") .add_property("result_function", &PmcResult::resultFunction) .add_property("constraints_well_formed", &PmcResult::constraintsWellFormed) .add_property("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving) @@ -70,50 +69,49 @@ BOOST_PYTHON_MODULE(_core) //////////////////////////////////////////// enum_("ModelType") - .value("dtmc", storm::models::ModelType::Dtmc) - .value("mdp", storm::models::ModelType::Mdp) - .value("ctmc", storm::models::ModelType::Ctmc) - .value("ma", storm::models::ModelType::MarkovAutomaton) - ; + .value("DTMC", storm::models::ModelType::Dtmc) + .value("MDP", storm::models::ModelType::Mdp) + .value("CTMC", storm::models::ModelType::Ctmc) + .value("MA", storm::models::ModelType::MarkovAutomaton) + ; defineClass("ModelBase", "") - .add_property("nr_states", &storm::models::ModelBase::getNumberOfStates) - .add_property("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions) - .add_property("model_type", &storm::models::ModelBase::getType) - .def("as_dtmc", &storm::models::ModelBase::as>) - .def("as_pdtmc", &storm::models::ModelBase::as>) - .def("as_pmdp", &storm::models::ModelBase::as>) - + .add_property("nr_states", &storm::models::ModelBase::getNumberOfStates) + .add_property("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions) + .add_property("model_type", &storm::models::ModelBase::getType) + .def("as_dtmc", &storm::models::ModelBase::as>) + .def("as_pdtmc", &storm::models::ModelBase::as>) + .def("as_pmdp", &storm::models::ModelBase::as>) ; - defineClass, storm::models::ModelBase, boost::noncopyable>("SparseParametricModel", ""); defineClass, storm::models::ModelBase, boost::noncopyable>("SparseModel", ""); - defineClass, storm::models::sparse::Model, boost::noncopyable>("Dtmc", ""); + defineClass, storm::models::sparse::Model, boost::noncopyable>("SparseDtmc", ""); + defineClass, storm::models::sparse::Model>("SparseMdp", ""); - defineClass, storm::models::sparse::Model>("SparseParametricMc", ""); + defineClass, storm::models::ModelBase, boost::noncopyable>("SparseParametricModel", ""); + defineClass, storm::models::sparse::Model>("SparseParametricDtmc", ""); defineClass, storm::models::sparse::Model>("SparseParametricMdp", ""); defineClass>, void, void>("FormulaVec", "Vector of formulas") - .def(vector_indexing_suite>, true>()) - ; + .def(vector_indexing_suite>, true>()) + ; def("parse_formulae", storm::parseFormulasForProgram); def("parse_program", storm::parseProgram); def("build_model", buildModel, return_value_policy()); - def("buildodelFromPrismProgram", storm::buildSymbolicModel); - def("buildParametricModelFromPrismProgram", storm::buildSymbolicModel); + def("build_model_from_prism_program", storm::buildSymbolicModel); + def("build_parametric_model_from_prism_program", storm::buildSymbolicModel); ////////////////////////////////////////////// // Model Checking ////////////////////////////////////////////// class_("ModelProgramPair", no_init) - .add_property("model", &storm::storage::ModelFormulasPair::model) - .add_property("program", &storm::storage::ModelFormulasPair::formulas) + .add_property("model", &storm::storage::ModelFormulasPair::model) + .add_property("program", &storm::storage::ModelFormulasPair::formulas) ; - def("perform_state_elimination", performStateElimination); } diff --git a/src/python/storm-logic.cpp b/src/python/storm-logic.cpp index 78be3af27..a6da9725f 100644 --- a/src/python/storm-logic.cpp +++ b/src/python/storm-logic.cpp @@ -86,10 +86,4 @@ BOOST_PYTHON_MODULE(_logic) defineClass("BooleanBinaryStateFormula", ""); - - - - - - -} \ No newline at end of file +}