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 constraintCollector; constraintCollector(*dtmc); + STORM_LOG_DEBUG("Computing function..."); + std::unique_ptr result = modelchecker.check(*formula); + + STORM_LOG_DEBUG("Computed the final result."); + ValueType valueFunction = result->asExplicitQuantitativeCheckResult()[*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());