diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp index 4f9dcd2a5..f44df8caf 100644 --- a/src/python/storm-core.cpp +++ b/src/python/storm-core.cpp @@ -14,8 +14,12 @@ std::shared_ptr buildModel(storm::prism::Program const return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; } -void printResult(std::shared_ptr result) { - result->writeToStream(std::cout); +std::unique_ptr performStateElimination(std::shared_ptr> model, std::shared_ptr const& formula) { + std::cout << "Perform state elimination" << std::endl; + std::unique_ptr result = storm::verifySparseModel(model, formula); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); + std::cout << "Result: " << *result << std::endl; + return result; } void setupStormLib(std::string const& args) { @@ -58,9 +62,6 @@ BOOST_PYTHON_MODULE(_core) //////////////////////////////////////////// class_, boost::noncopyable>("CheckResult", no_init) ; - register_ptr_to_python>(); - - def("print_result", printResult); //////////////////////////////////////////// @@ -110,5 +111,5 @@ BOOST_PYTHON_MODULE(_core) ; - def("perform_state_elimination", boost::python::converter::adapt_unique(storm::verifySparseModel)); + def("perform_state_elimination", boost::python::converter::adapt_unique(performStateElimination)); }