From 43a1d0bc73ff4d1ce56d77281af7c1be1acd9da8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 8 Feb 2015 13:52:36 +0100
Subject: [PATCH] Added debug output.
Former-commit-id: 20ee3ec777ff3491d1a8bc2eeae4a962351ce1ff
---
.../reachability/SparseDtmcEliminationModelChecker.cpp | 1 +
src/stormParametric.cpp | 8 ++++----
2 files changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 5bee46f8b..1a3e54ab2 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -538,6 +538,7 @@ namespace storm {
}
// Now, we return the value for the only initial state.
+ STORM_LOG_DEBUG("Simplifying and returning result.");
if (stateRewards) {
return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
} else {
diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp
index 40388cca6..ade3e3451 100644
--- a/src/stormParametric.cpp
+++ b/src/stormParametric.cpp
@@ -197,10 +197,6 @@ void check() {
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());
@@ -209,6 +205,10 @@ void check() {
}
std::cout << std::endl;
+ if (storm::settings::parametricSettings().exportResultToFile()) {
+ storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
+ }
+
// Generate derivatives for sensitivity analysis if requested.
if (std::is_same<ValueType, storm::RationalFunction>::value && storm::settings::parametricSettings().isDerivativesSet()) {
ValueType function = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];