diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp index ea1948d54..8e3da6930 100644 --- a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp @@ -20,10 +20,11 @@ namespace storm { template void SparseNondeterministicStepBoundedHorizonHelper::getMaybeStatesRowGroupSizes(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, std::vector& maybeStatesRowGroupSizes, uint& choiceValuesCounter) { std::vector rowGroupIndices = transitionMatrix.getRowGroupIndices(); + choiceValuesCounter = 0; for(uint counter = 0; counter < maybeStates.size(); counter++) { if(maybeStates.get(counter)) { - maybeStatesRowGroupSizes.push_back(rowGroupIndices.at(counter)); choiceValuesCounter += transitionMatrix.getRowGroupSize(counter); + maybeStatesRowGroupSizes.push_back(choiceValuesCounter); } } } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 2a352c381..139165ee3 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -110,7 +110,9 @@ namespace storm { } // Create a multiplier for reduction. auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), result, &statesOfCoalition); + auto rowGroupIndices = transitionMatrix.getRowGroupIndices(); + rowGroupIndices.erase(rowGroupIndices.begin()); + multiplier->reduce(env, goal.direction(), b, rowGroupIndices, result, &statesOfCoalition); if (goal.isShieldingTask()) { choiceValues = b; } diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 2324b7833..e5df00b05 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -92,8 +92,13 @@ namespace storm { template void Multiplier::reduce(Environment const& env, OptimizationDirection const& dir, std::vector const& choiceValues, std::vector::index_type> rowGroupIndices, std::vector& result, storm::storage::BitVector const* dirOverride) const { auto choice_it = choiceValues.begin(); - for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { - uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + for(uint state = 0; state < rowGroupIndices.size(); state++) { + uint rowGroupSize; + if(state == 0) { + rowGroupSize = rowGroupIndices[state]; + } else { + rowGroupSize = rowGroupIndices[state] - rowGroupIndices[state-1]; + } if(dirOverride != nullptr) { if((dir == storm::OptimizationDirection::Minimize && !dirOverride->get(state)) || (dir == storm::OptimizationDirection::Maximize && dirOverride->get(state))) { result.at(state) = *std::min_element(choice_it, choice_it + rowGroupSize);