From 5f6dc2f944a756c6c527ff58105a6b0cf14881fa Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Wed, 20 Jan 2016 10:25:53 +0100
Subject: [PATCH] Output for model checking result

Former-commit-id: 942600dc3f4daf6a7e5f48e77578de990421ddec
---
 src/python/storm-core.cpp | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

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<storm::models::ModelBase> buildModel(storm::prism::Program const
     return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<storm::logic::Formula>>(1,formula)).model;
 }
 
-void printResult(std::shared_ptr<storm::modelchecker::CheckResult> result) {
-    result->writeToStream(std::cout);
+std::unique_ptr<storm::modelchecker::CheckResult> performStateElimination(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+    std::cout << "Perform state elimination" << std::endl;
+    std::unique_ptr<storm::modelchecker::CheckResult> result = storm::verifySparseModel<storm::RationalFunction>(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_<storm::modelchecker::CheckResult, std::unique_ptr<storm::modelchecker::CheckResult>, boost::noncopyable>("CheckResult", no_init)
     ;
-    register_ptr_to_python<std::shared_ptr<storm::modelchecker::CheckResult>>();
-
-    def("print_result", printResult);
 
 
     ////////////////////////////////////////////
@@ -110,5 +111,5 @@ BOOST_PYTHON_MODULE(_core)
     ;
 
 
-    def("perform_state_elimination", boost::python::converter::adapt_unique(storm::verifySparseModel<storm::RationalFunction>));
+    def("perform_state_elimination", boost::python::converter::adapt_unique(performStateElimination));
 }