From d63086d7e3e328cb42fa62fb169e3c644ab9197f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 7 Feb 2015 02:46:48 +0100
Subject: [PATCH] Enabled output file, this time fo' real.

Former-commit-id: 64c17ea23eff44f838fdea936292a3b82542a9f3
---
 src/stormParametric.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp
index eba96ef4b..09cfa47d5 100644
--- a/src/stormParametric.cpp
+++ b/src/stormParametric.cpp
@@ -193,14 +193,19 @@ void check() {
     
     storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector;
     constraintCollector(*dtmc);
-    
+
     std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula);
+    ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
+    
+    if (storm::settings::parametricSettings().exportResultToFile()) {
+        storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
+    }
 
     // Report the result.
     STORM_PRINT_AND_LOG(std::endl << "Result (initial state): ");
     result->writeToStream(std::cout, model->getInitialStates());
     if (std::is_same<ValueType, storm::RationalFunction>::value) {
-        printApproximateResult(result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()]);
+        printApproximateResult(valueFunction);
     }
     std::cout << std::endl;
 }