diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp index 307f4d889..ffeacaf3d 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp @@ -23,13 +23,12 @@ namespace storm { namespace internal { template - SparseSmgLraHelper::SparseSmgLraHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const statesOfCoalition) : _transitionMatrix(transitionMatrix), _x1IsCurrent(false), _x1IsCurrentStrategyVI(false), _statesOfCoalition(statesOfCoalition) { + SparseSmgLraHelper::SparseSmgLraHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { } template std::vector SparseSmgLraHelper::computeLongRunAverageRewardsSound(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel) { - // STORM_LOG_DEBUG("Transition Matrix:\n" << _transitionMatrix); std::vector result; std::vector stateRewardsGetter = std::vector(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); if (rewardModel.hasStateRewards()) { @@ -45,7 +44,7 @@ namespace storm { } else { actionRewardsGetter = [] (uint64_t) { return storm::utility::zero(); }; } - std::vector b = getBVector(stateRewardsGetter, actionRewardsGetter); + _b = getBVector(stateRewardsGetter, actionRewardsGetter); // If requested, allocate memory for the choices made if (this->_produceScheduler) { @@ -56,7 +55,7 @@ namespace storm { } prepareMultiplier(env, rewardModel); - performValueIteration(env, rewardModel, b, actionRewardsGetter, result); + performValueIteration(env, rewardModel, _b, actionRewardsGetter, result); return result; } @@ -83,8 +82,7 @@ namespace storm { auto precision = storm::utility::convertNumber(env.solver().lra().getPrecision()); Environment envMinMax = env; - envMinMax.solver().lra().setPrecision(precision / 2.0); - STORM_LOG_DEBUG(envMinMax.solver().lra().getPrecision()); + envMinMax.solver().lra().setPrecision(precision / storm::utility::convertNumber(2)); do { size_t iteration_count = 0; @@ -92,23 +90,28 @@ namespace storm { _multiplier->multiplyAndReduce(env, _optimizationDirection, xNew(), &b, xNew(), &choicesForStrategies, &_statesOfCoalition); - if (iteration_count % 5 == 0) { // only every 5th iteration + 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); // 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); - STORM_LOG_DEBUG("resultMax: " << _resultForMax); _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) { @@ -116,19 +119,17 @@ namespace storm { storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MinSolver(restrictedMinMatrix); MinSolver.setOptimizationDirection(OptimizationDirection::Maximize); + MinSolver.setProduceChoiceValues(false); _resultForMin = MinSolver.computeLongRunAverageRewards(envMinMax, rewardModel); - STORM_LOG_DEBUG("resultMin: " << _resultForMin); _fixedMinStrat = fixedMinStrat; for (size_t i = 0; i < xNewU().size(); i++) { xNewU()[i] = std::min(xNewU()[i], _resultForMin[i]); } + STORM_LOG_DEBUG("xU " << xNewU()[0]); } } - STORM_LOG_DEBUG("xL " << xNewL()); - STORM_LOG_DEBUG("xU " << xNewU()); - } while (!checkConvergence(precision)); if (_produceScheduler) { @@ -140,7 +141,7 @@ namespace storm { this->_choiceValues.emplace(); } this->_choiceValues->resize(this->_transitionMatrix.getRowCount()); - _choiceValues = calcChoiceValues(envMinMax, rewardModel); + _choiceValues = calcChoiceValues(env, rewardModel); } result = xNewL(); } @@ -150,7 +151,6 @@ namespace storm { storm::storage::BitVector SparseSmgLraHelper::getStrategyFixedBitVec(std::vector const& choices, MinMaxStrategy strategy) { storm::storage::BitVector restrictBy(_transitionMatrix.getRowCount(), true); auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); - STORM_LOG_DEBUG("choices " << choices); for(uint state = 0; state < _transitionMatrix.getRowGroupCount(); state++) { if ((_minimizerStates[state] && strategy == MinMaxStrategy::MaxStrategy) || (!_minimizerStates[state] && strategy == MinMaxStrategy::MinStrategy)) @@ -169,46 +169,8 @@ namespace storm { template std::vector SparseSmgLraHelper::calcChoiceValues(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel) { std::vector choiceValues(_transitionMatrix.getRowCount()); + _multiplier->multiply(env, xNewL(), nullptr, choiceValues); - storm::storage::SparseMatrix restrictedMaxMatrix = _transitionMatrix.restrictRows(_fixedMaxStrat); - storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MaxSolver(restrictedMaxMatrix); - MaxSolver.setOptimizationDirection(OptimizationDirection::Minimize); - MaxSolver.setProduceChoiceValues(true); - MaxSolver.computeLongRunAverageRewards(env, rewardModel); - std::vector minimizerChoices = MaxSolver.getChoiceValues(); - - storm::storage::SparseMatrix restrictedMinMatrix = _transitionMatrix.restrictRows(_fixedMinStrat); - storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MinSolver(restrictedMinMatrix); - MinSolver.setOptimizationDirection(OptimizationDirection::Maximize); - MinSolver.setProduceChoiceValues(true); - MinSolver.computeLongRunAverageRewards(env, rewardModel); - std::vector maximizerChoices = MinSolver.getChoiceValues(); - - auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); - - auto minIt = minimizerChoices.begin(); - auto maxIt = maximizerChoices.begin(); - size_t globalCounter = 0; - for(uint state = 0; state < _transitionMatrix.getRowGroupCount(); state++) { - uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; - for(uint rowGroupIndex = 0; rowGroupIndex < rowGroupSize; rowGroupIndex++) { - if (_minimizerStates[state]) { - choiceValues[globalCounter] = *minIt; - minIt++; - } - else { - choiceValues[globalCounter] = *maxIt; - maxIt++; - } - globalCounter++; - } - if (_minimizerStates[state]) { - maxIt++; - } - else { - minIt++; - } - } return choiceValues; } @@ -223,9 +185,11 @@ namespace storm { storm::storage::Scheduler SparseSmgLraHelper::extractScheduler() const{ auto const& optimalChoices = getProducedOptimalChoices(); storm::storage::Scheduler scheduler(optimalChoices.size()); + for (uint64_t state = 0; state < optimalChoices.size(); ++state) { scheduler.setChoice(optimalChoices[state], state); } + return scheduler; } @@ -233,6 +197,7 @@ namespace storm { std::vector const& SparseSmgLraHelper::getProducedOptimalChoices() const { STORM_LOG_ASSERT(_produceScheduler, "Trying to get the produced optimal choices although no scheduler was requested."); STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); + return this->_producedOptimalChoices.get(); } @@ -240,12 +205,15 @@ namespace storm { void SparseSmgLraHelper::prepareMultiplier(const Environment& env, storm::models::sparse::StandardRewardModel const& rewardModel) { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); - _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; + if (_statesOfCoalition.size()) { + _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; + } + else { + _minimizerStates = storm::storage::BitVector(_transitionMatrix.getRowGroupCount(), _optimizationDirection == OptimizationDirection::Minimize); + } - _x1L = std::vector(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); - _x2L = _x1L; - _x1 = _x1L; - _x2 = _x1; + _xL = std::vector(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + _x = _xL; _fixedMaxStrat = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); _fixedMinStrat = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); @@ -253,8 +221,7 @@ namespace storm { _resultForMin = std::vector(_transitionMatrix.getRowGroupCount()); _resultForMax = std::vector(_transitionMatrix.getRowGroupCount()); - _x1U = std::vector(_transitionMatrix.getRowGroupCount(), std::numeric_limits::infinity()); - _x2U = _x1U; + _xU = std::vector(_transitionMatrix.getRowGroupCount(), std::numeric_limits::infinity()); } template @@ -276,62 +243,32 @@ namespace storm { template std::vector& SparseSmgLraHelper::xNewL() { - return _x1IsCurrent ? _x1L : _x2L; + return _xL; } template std::vector const& SparseSmgLraHelper::xNewL() const { - return _x1IsCurrent ? _x1L : _x2L; - } - - template - std::vector& SparseSmgLraHelper::xOldL() { - return _x1IsCurrent ? _x2L : _x1L; - } - - template - std::vector const& SparseSmgLraHelper::xOldL() const { - return _x1IsCurrent ? _x2L : _x1L; + return _xL; } template std::vector& SparseSmgLraHelper::xNewU() { - return _x1IsCurrent ? _x1U : _x2U; + return _xU; } template std::vector const& SparseSmgLraHelper::xNewU() const { - return _x1IsCurrent ? _x1U : _x2U; - } - - template - std::vector& SparseSmgLraHelper::xOldU() { - return _x1IsCurrent ? _x2U : _x1U; - } - - template - std::vector const& SparseSmgLraHelper::xOldU() const { - return _x1IsCurrent ? _x2U : _x1U; - } - - template - std::vector& SparseSmgLraHelper::xOld() { - return _x1IsCurrent ? _x2 : _x1; - } - - template - std::vector const& SparseSmgLraHelper::xOld() const { - return _x1IsCurrent ? _x2 : _x1; + return _xU; } template std::vector& SparseSmgLraHelper::xNew() { - return _x1IsCurrent ? _x1 : _x2; + return _x; } template std::vector const& SparseSmgLraHelper::xNew() const { - return _x1IsCurrent ? _x1 : _x2; + return _x; } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h index d9be65770..5fb8bf205 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h @@ -29,17 +29,6 @@ namespace storm { SparseSmgLraHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const statesOfCoalition); - /*! - * Performs value iteration with the given state- and action values. - * @param env The environment, containing information on the precision of this computation. - * @param stateValueGetter function that returns for each state index (w.r.t. the input transition matrix) the reward for staying in state. Will only be called for timed states. - * @param actionValueGetter function that returns for each global choice index (w.r.t. the input transition matrix) the reward for taking that choice - * @param exitRates (as in the constructor) - * @param dir Optimization direction. Must be not nullptr in case of nondeterminism - * @param choices if not nullptr, the optimal choices will be inserted in this vector. The vector's size must then be equal to the number of row groups of the input transition matrix. - * @return The (optimal) long run average value of the specified component. - * @note it is possible to call this method multiple times with different values. However, other changes to the environment or the optimization direction might not have the expected effect due to caching. - */ 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); std::vector getChoiceValues() const; @@ -66,26 +55,8 @@ namespace storm { private: - /*! - * Initializes the value iterations with the provided values. - * Resets all information from potential previous calls. - * Must be called before the first call to performIterationStep. - * @param stateValueGetter Function that returns for each state index (w.r.t. the input transitions) the value (e.g. reward) for that state - * @param stateValueGetter Function that returns for each global choice index (w.r.t. the input transitions) the value (e.g. reward) for that choice - */ - void initializeNewValues(ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector const* exitRates = nullptr); - bool checkConvergence(ValueType threshold) const; - - /*! - * Performs a single iteration step. - * @param env The environment. - * @param dir The optimization direction. Has to be given if there is nondeterminism (otherwise it will be ignored) - * @param choices If given, the optimal choices will be inserted at the appropriate states. - * Note that these choices will be inserted w.r.t. the original model states/choices, i.e. the size of the vector should match the state-count of the input model - * @pre when calling this the first time, initializeNewValues must have been called before. Moreover, prepareNextIteration must be called between two calls of this. - */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr, std::vector* choices = nullptr, std::vector* choiceValues = nullptr); struct ConvergenceCheckResult { @@ -99,42 +70,17 @@ namespace storm { std::vector calcChoiceValues(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel); - /*! - * Must be called between two calls of performIterationStep. - */ - void prepareNextIteration(Environment const& env); - - /// Prepares the necessary solvers and multipliers for doing the iterations. - void prepareSolversAndMultipliers(Environment const& env, storm::solver::OptimizationDirection const* dir = nullptr); - - void setInputModelChoices(std::vector& choices, std::vector const& localMecChoices, bool setChoiceZeroToMarkovianStates = false, bool setChoiceZeroToProbabilisticStates = false) const; - - void setInputModelChoiceValues(std::vector& choiceValues, std::vector const& localMecChoiceValues) const; - - /// Returns true iff the given state is a timed state - bool isTimedState(uint64_t const& inputModelStateIndex) const; - std::vector& xNew(); std::vector const& xNew() const; - std::vector& xOld(); - std::vector const& xOld() const; - std::vector& xNewL(); std::vector const& xNewL() const; - std::vector& xOldL(); - std::vector const& xOldL() const; - std::vector& xNewU(); std::vector const& xNewU() const; - std::vector& xOldU(); - std::vector const& xOldU() const; - storm::storage::SparseMatrix const& _transitionMatrix; storm::storage::BitVector const _statesOfCoalition; - ValueType _strategyVIPrecision; storm::storage::BitVector _relevantStates; storm::storage::BitVector _minimizerStates; @@ -144,17 +90,16 @@ namespace storm { std::vector _resultForMax; std::vector _resultForMin; + std::vector _b; + boost::optional> _valueThreshold; storm::solver::OptimizationDirection _optimizationDirection; bool _produceScheduler; bool _produceChoiceValues; bool _isQualitativeSet; - ValueType _uniformizationRate; - std::vector _x1, _x2, _x1L, _x2L, _x1U, _x2U; + std::vector _x, _xL, _xU; std::vector _Tsx1, _Tsx2, _TsChoiceValues; - bool _x1IsCurrent; - bool _x1IsCurrentStrategyVI; std::vector _Isx, _Isb, _IsChoiceValues; std::unique_ptr> _multiplier; std::unique_ptr> _Solver; diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 7fa177d2c..754ca74b2 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -265,8 +265,8 @@ namespace storm { if (env.solver().isForceSoundness()) { storm::modelchecker::helper::internal::SparseSmgLraHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); - auto values = helper.computeLongRunAverageRewardsSound(env, rewardModel.get()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewardsSound(env, rewardModel.get()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); if(checkTask.isShieldingTask()) { @@ -281,8 +281,8 @@ namespace storm { } storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); - auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(values))); if(checkTask.isShieldingTask()) { storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index a91fc03b6..c87b31d5f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -22,7 +22,12 @@ namespace storm { void SoundGameViHelper::prepareSolversAndMultipliers(const Environment& env) { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); _x1IsCurrent = false; - _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; + if (_statesOfCoalition.size()) { + _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; + } + else { + _minimizerStates = storm::storage::BitVector(_transitionMatrix.getRowGroupCount(), _optimizationDirection == OptimizationDirection::Minimize); + } _oldPolicy = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); _timing = std::vector(5, 0); }