From e32482b7a99c0d89ca1030032e2e6842804d3446 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 8 Feb 2015 16:22:27 +0100
Subject: [PATCH] Added debug output.

Former-commit-id: 247b615c1e7c5b4c0a7681457966c8e10fe8f34f
---
 .../reachability/SparseDtmcEliminationModelChecker.cpp     | 2 +-
 src/stormParametric.cpp                                    | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 7f5ea4ea5..f7cc0a274 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -543,7 +543,7 @@ namespace storm {
 //                if (storm::settings::parametricSettings().isSimplifySet()) {
 //                    return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
 //                } else {
-                    return stateRewards.get()[*initialStates.begin()];
+                    return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
 //                }
             } else {
 //                if (storm::settings::parametricSettings().isSimplifySet()) {
diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp
index ade3e3451..1d44a79cf 100644
--- a/src/stormParametric.cpp
+++ b/src/stormParametric.cpp
@@ -194,9 +194,16 @@ void check() {
     storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector;
     constraintCollector(*dtmc);
 
+    STORM_LOG_DEBUG("Computing function...");
+
     std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula);
+    
+    STORM_LOG_DEBUG("Computed the final result.");
+    
     ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
     
+    STORM_LOG_DEBUG("Extracted value function.");
+    
     // Report the result.
     STORM_PRINT_AND_LOG(std::endl << "Result (initial state): ");
     result->writeToStream(std::cout, model->getInitialStates());