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 result = modelchecker.check(*formula); ValueType valueFunction = result->asExplicitQuantitativeCheckResult()[*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::value && storm::settings::parametricSettings().isDerivativesSet()) { ValueType function = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()];