diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 350123670..710362961 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -87,22 +87,26 @@ namespace storm { template MDPSparseModelCheckingHelperReturnType 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 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); + // coalition handling for all states storm::storage::BitVector clippedStatesOfCoalition(transitionMatrix.getRowGroupCount()); clippedStatesOfCoalition.setClippedStatesOfCoalition(allStates, statesOfCoalition); clippedStatesOfCoalition.complement(); - storm::modelchecker::helper::internal::GameViHelper viHelper(transitionMatrix, clippedStatesOfCoalition); - std::unique_ptr> scheduler; if (produceScheduler) { STORM_LOG_WARN("Next formula does not expect that produceScheduler is set to true."); } - viHelper.performNextIteration(env, x, b, goal.direction()); - return MDPSparseModelCheckingHelperReturnType(std::move(x), std::move(scheduler)); + // create multiplier and execute the calculation for 1 step + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->multiplyAndReduce(env, goal.direction(), x, &b, x, nullptr, &statesOfCoalition); + + //STORM_LOG_DEBUG("x = " << storm::utility::vector::toString(x)); + return MDPSparseModelCheckingHelperReturnType(std::move(x)); } template class SparseSmgRpatlHelper; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index a19c1bc54..8c354d945 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -151,16 +151,6 @@ namespace storm { } template - void GameViHelper::performNextIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { - prepareSolversAndMultipliersReachability(env); - _b = b; - _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); - _x2 = _x1; - performIterationStep(env, dir); - x = xNew(); - } - - template void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index d67c090de..d46f9049c 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -30,8 +30,6 @@ namespace storm { */ void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); - void performNextIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir); - /*h * Sets whether an optimal scheduler shall be constructed during the computation */