diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index b0b16ccc5..84b756dee 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -131,33 +131,28 @@ namespace storm { // Initialize the solution vector. std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::one()); - - // Reduce the matrix to relevant states - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - - std::vector constrainedChoiceValues = std::vector(submatrix.getRowCount(), storm::utility::zero()); + std::vector constrainedChoiceValues = std::vector(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates).size(), storm::utility::zero()); storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); - // Use the bounded globally game vi helper - storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(submatrix, clippedStatesOfCoalition); - std::unique_ptr> scheduler; - if (produceScheduler) { - viHelper.setProduceScheduler(true); - } - - // in case of upperBound = 0 the states which are initially "safe" are filled with ones - if(upperBound > 0) - { + // Use the bounded globally game vi helper. + storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(transitionMatrix, clippedStatesOfCoalition); + if(!relevantStates.empty() && upperBound > 0) { + // Reduce the matrix to relevant states. + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + // Update the BoundedGloballyViHelper. + storm::modelchecker::helper::internal::BoundedGloballyGameViHelper viHelper(submatrix, clippedStatesOfCoalition); + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues); } - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); viHelper.fillResultVector(x, relevantStates); viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); - + std::unique_ptr> scheduler; if (produceScheduler) { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates)); }