From 7e5867252d6298df9d3095d1c4cc0bf304a3af01 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 29 Oct 2024 09:39:48 +0100 Subject: [PATCH] SoundGameViHelper: cleaned up --- .../modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp | 4 ---- .../modelchecker/rpatl/helper/internal/SoundGameViHelper.h | 4 ++-- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index c87b31d5f..aab2935d6 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -40,7 +40,6 @@ namespace storm { ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); - //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x1L = xL; _x2L = _x1L; @@ -156,7 +155,6 @@ namespace storm { // iterating over all MSECs for (auto smec_it : MSEC) { ValueType bestExit = 0; - // if (smec_it.isErgodic(restrictedMatrix)) continue; auto stateSet = smec_it.getStateSet(); for (uint state : stateSet) { if (_psiStates[state]) { @@ -239,10 +237,8 @@ namespace storm { auto x1It = xNewL().begin(); auto x1Ite = xNewL().end(); auto x2It = xNewU().begin(); - // The difference between maxDiff and minDiff is zero at this point. Thus, it doesn't make sense to check the threshold now. for (; x1It != x1Ite; x1It++, x2It++) { ValueType diff = (*x2It - *x1It); - // Potentially update maxDiff or minDiff if (diff > threshold) { return false; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index 45d583b7b..e90099fde 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -72,8 +72,6 @@ namespace storm { void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result, std::vector& x); - // multiplier now public for testing - std::unique_ptr> _multiplier; private: /*! * Performs one iteration step for value iteration @@ -113,6 +111,8 @@ namespace storm { */ std::vector& getProducedOptimalChoices(); + std::unique_ptr> _multiplier; + storm::storage::SparseMatrix _transitionMatrix; storm::storage::SparseMatrix _backwardTransitions; storm::storage::SparseMatrix _restrictedTransitions;