diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 6e08f8277..37a04da9c 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -19,23 +19,12 @@ namespace storm { template void BoundedGloballyGameViHelper::prepareSolversAndMultipliers(const Environment& env) { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); -/* - _x1IsCurrent = false; -*/ } template void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { prepareSolversAndMultipliers(env); -/* - _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); -*/ - _x1 = x; - _x2 = _x1; - -/* STORM_LOG_DEBUG("_b = " << _b); - STORM_LOG_DEBUG("_x1 = " << _x1); - STORM_LOG_DEBUG("_x2 = " << _x2);*/ + _x = x; if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { @@ -46,24 +35,9 @@ namespace storm { for (uint64_t iter = 0; iter < upperBound; iter++) { performIterationStep(env, dir); -/* STORM_LOG_DEBUG("After iteration " << iter << ":"); - STORM_LOG_DEBUG("_x1 = " << _x1); - STORM_LOG_DEBUG("_x2 = " << _x2);*/ - -/* if (storm::utility::resources::isTerminate()) { - break; - }*/ } -/* - x = xNew(); -*/ - x = _x1; - -/* if (isProduceSchedulerSet()) { - // We will be doing one more iteration step and track scheduler choices this time. - performIterationStep(env, dir, &_producedOptimalChoices.get()); - }*/ + x = _x; } template @@ -71,27 +45,15 @@ namespace storm { if (!_multiplier) { prepareSolversAndMultipliers(env); } -/* _x1IsCurrent = !_x1IsCurrent;*/ // multiplyandreducegaussseidel // Ax + b if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, nullptr, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, nullptr, &_statesOfCoalition); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, choices, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition); } - -/* // compare applyPointwise - storm::utility::vector::applyPointwise(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { - if(storm::solver::maximize(dir)) { - if(a > b) return a; - else return b; - } else { - if(a > b) return a; - else return b; - } - });*/ } template @@ -142,26 +104,6 @@ namespace storm { return scheduler; } -/* template - std::vector& BoundedGloballyGameViHelper::xNew() { - return _x1IsCurrent ? _x1 : _x2; - } - - template - std::vector const& BoundedGloballyGameViHelper::xNew() const { - return _x1IsCurrent ? _x1 : _x2; - } - - template - std::vector& BoundedGloballyGameViHelper::xOld() { - return _x1IsCurrent ? _x2 : _x1; - } - - template - std::vector const& BoundedGloballyGameViHelper::xOld() const { - return _x1IsCurrent ? _x2 : _x1; - }*/ - template class BoundedGloballyGameViHelper; #ifdef STORM_HAVE_CARL template class BoundedGloballyGameViHelper; diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index 512031b49..c13286e41 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -30,7 +30,7 @@ namespace storm { */ void fillResultVector(std::vector& result, storm::storage::BitVector psiStates); - /*h + /*! * Sets whether an optimal scheduler shall be constructed during the computation */ void setProduceScheduler(bool value); @@ -45,13 +45,6 @@ namespace storm { private: void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); -/* std::vector& xNew(); - std::vector const& xNew() const; - - std::vector& xOld(); - std::vector const& xOld() const; - bool _x1IsCurrent;*/ - /*! * @pre before calling this, a computation call should have been performed during which scheduler production was enabled. * @return the produced scheduler of the most recent call. @@ -66,7 +59,7 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::BitVector _statesOfCoalition; - std::vector _x1, _x2; + std::vector _x; std::unique_ptr> _multiplier; bool _produceScheduler = false; diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 9e0ed3285..3a1343f90 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h @@ -30,7 +30,7 @@ namespace storm { */ void fillResultVector(std::vector& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates); - /*h + /*! * Sets whether an optimal scheduler shall be constructed during the computation */ void setProduceScheduler(bool value);