From 54f36dd36980ab5bcefa90284554e820a85d418b Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 29 Oct 2024 09:32:27 +0100 Subject: [PATCH] SparseSmgLraHelper: cleaned up --- .../internal/SparseSmgLraHelper.cpp | 19 ++++++++----------- .../internal/SparseSmgLraHelper.h | 9 +-------- 2 files changed, 9 insertions(+), 19 deletions(-) diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp index ffeacaf3d..6b8f63739 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp @@ -17,6 +17,8 @@ #include "modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" #include "storm/exceptions/UnmetRequirementException.h" +#define SOLVE_MDP 50 + namespace storm { namespace modelchecker { namespace helper { @@ -55,7 +57,7 @@ namespace storm { } prepareMultiplier(env, rewardModel); - performValueIteration(env, rewardModel, _b, actionRewardsGetter, result); + performValueIteration(env, rewardModel, _b, result); return result; } @@ -76,7 +78,7 @@ namespace storm { } template - void SparseSmgLraHelper::performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& b, ValueGetter const& actionValueGetter, std::vector& result, std::vector* choices, std::vector* choiceValues) + void SparseSmgLraHelper::performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& b, std::vector& result) { std::vector choicesForStrategies = std::vector(_transitionMatrix.getRowGroupCount(), 0); auto precision = storm::utility::convertNumber(env.solver().lra().getPrecision()); @@ -90,28 +92,24 @@ namespace storm { _multiplier->multiplyAndReduce(env, _optimizationDirection, xNew(), &b, xNew(), &choicesForStrategies, &_statesOfCoalition); - if (iteration_count % 50 == 0) { // only every 50th iteration - storm::storage::BitVector fixedMaxStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MaxStrategy); - storm::storage::BitVector fixedMinStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MinStrategy); + if (iteration_count % SOLVE_MDP == 0) { // only every 50th iteration + storm::storage::BitVector fixedMaxStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MaxStrategy); + storm::storage::BitVector fixedMinStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MinStrategy); - // compute bounds + // compute bounds if (fixedMaxStrat != _fixedMaxStrat) { storm::storage::SparseMatrix restrictedMaxMatrix = _transitionMatrix.restrictRows(fixedMaxStrat); - STORM_LOG_DEBUG("xL " << xNewL()[0]); storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MaxSolver(restrictedMaxMatrix); - STORM_LOG_DEBUG("xL " << xNewL()[0]); MaxSolver.setOptimizationDirection(OptimizationDirection::Minimize); MaxSolver.setProduceChoiceValues(false); _resultForMax = MaxSolver.computeLongRunAverageRewards(envMinMax, rewardModel); _fixedMaxStrat = fixedMaxStrat; - STORM_LOG_DEBUG("xL " << xNewL()[0]); for (size_t i = 0; i < xNewL().size(); i++) { xNewL()[i] = std::max(xNewL()[i], _resultForMax[i]); } - STORM_LOG_DEBUG("xL " << xNewL()[0]); } if (fixedMinStrat != _fixedMinStrat) { @@ -126,7 +124,6 @@ namespace storm { for (size_t i = 0; i < xNewU().size(); i++) { xNewU()[i] = std::min(xNewU()[i], _resultForMin[i]); } - STORM_LOG_DEBUG("xU " << xNewU()[0]); } } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h index 5fb8bf205..4a6537945 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h @@ -29,7 +29,7 @@ namespace storm { SparseSmgLraHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const statesOfCoalition); - void performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector& result, std::vector* choices = nullptr, std::vector* choiceValues = nullptr); + void performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& b, std::vector& result); std::vector getChoiceValues() const; @@ -57,13 +57,6 @@ namespace storm { bool checkConvergence(ValueType threshold) const; - void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr, std::vector* choiceValues = nullptr); - - struct ConvergenceCheckResult { - bool isPrecisionAchieved; - ValueType currentValue; - }; - storm::storage::BitVector getStrategyFixedBitVec(std::vector const& choices, MinMaxStrategy strategy); std::vector getBVector(std::vector const& stateRewardsGetter, ValueGetter const& actionRewardsGetter);