diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 29d41b45c..566120827 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -64,6 +64,8 @@ namespace storm { SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, goal.direction()); + std::unique_ptr> scheduler; + storm::storage::BitVector relevantStates(psiStates.size(), true); // Initialize the x vector and solution vector result. // TODO Fabian: maybe relevant states (later) @@ -93,6 +95,7 @@ namespace storm { std::vector constrainedChoiceValues; viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); + return SMGSparseModelCheckingHelperReturnType(std::move(xU), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); assert(false); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 10de545e3..5a7109cac 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -28,7 +28,6 @@ namespace storm { template void SoundGameViHelper::performValueIteration(Environment const& env, std::vector& xL, std::vector& xU, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues) { - // new pair (x_old, x_new) for over_approximation() prepareSolversAndMultipliers(env); // Get precision for convergence check.