diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index b3b89688e..d4e06bbde 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -97,25 +97,20 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { - // create vector x for result, bitvector allStates with a true for each state and a vector b for the probability to get to state psi + // Create vector x for result, bitvector allStates with a true for each state and a vector b for the probability for each state to get to a psi state, choiceValues is to store choices for shielding. std::vector x = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); storm::storage::BitVector allStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(allStates, psiStates); - + std::vector choiceValues = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); statesOfCoalition.complement(); - if (produceScheduler) { STORM_LOG_WARN("Next formula does not expect that produceScheduler is set to true."); } - - // create multiplier and execute the calculation for 1 step + // Create a multiplier for reduction. auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); - std::vector choiceValues = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), x, &statesOfCoalition); if (goal.isShieldingTask()) { - multiplier->multiply(env, x, &b, choiceValues); - multiplier->reduce(env, goal.direction(), choiceValues, transitionMatrix.getRowGroupIndices(), x, &statesOfCoalition); - } else { - multiplier->multiplyAndReduce(env, goal.direction(), x, &b, x, nullptr, &statesOfCoalition); + choiceValues = b; } return SMGSparseModelCheckingHelperReturnType(std::move(x), std::move(allStates), nullptr, std::move(choiceValues)); }