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 constraintCollector; constraintCollector(*dtmc); - + 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()); if (std::is_same::value) { - printApproximateResult(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]); + printApproximateResult(valueFunction); } std::cout << std::endl; }