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;