diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 78d554346..b0b16ccc5 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -27,26 +27,32 @@ namespace storm { std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); - // Reduce the matrix to relevant states - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); clippedStatesOfCoalition.complement(); - storm::modelchecker::helper::internal::GameViHelper viHelper(submatrix, clippedStatesOfCoalition); - std::unique_ptr> scheduler; - if (produceScheduler) { - viHelper.setProduceScheduler(true); + storm::modelchecker::helper::internal::GameViHelper viHelper(transitionMatrix, clippedStatesOfCoalition); + if(!relevantStates.empty()) { + // Reduce the matrix to relevant states. + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + // Update the GameViHelper. + viHelper = storm::modelchecker::helper::internal::GameViHelper(submatrix, clippedStatesOfCoalition); + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } + // Perform value iteration. + viHelper.performValueIteration(env, x, b, goal.direction()); + if(goal.isShieldingTask()) { + viHelper.getChoiceValues(env, x, constrainedChoiceValues); + } } - viHelper.performValueIteration(env, x, b, goal.direction()); - if(goal.isShieldingTask()) { - viHelper.getChoiceValues(env, x, constrainedChoiceValues); - } + // Fill up the result x with 0s and 1s for not relevant states. viHelper.fillResultVector(x, relevantStates, psiStates); + // Fill up the constrainedChoice Values to full size. viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + std::unique_ptr> scheduler; if (produceScheduler) { scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); }