diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp new file mode 100644 index 000000000..92df53597 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp @@ -0,0 +1,271 @@ +#include "SparseSmgLraHelper.h" + +#include "storm/storage/MaximalEndComponent.h" +#include "storm/storage/StronglyConnectedComponent.h" + +#include "storm/utility/graph.h" +#include "storm/utility/vector.h" +#include "storm/utility/macros.h" +#include "storm/utility/SignalHandler.h" + +#include "storm/environment/solver/SolverEnvironment.h" +#include "storm/environment/solver/LongRunAverageSolverEnvironment.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/environment/solver/GameSolverEnvironment.h" + +#include "modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" +#include "storm/exceptions/UnmetRequirementException.h" + +namespace storm { + namespace modelchecker { + namespace helper { + namespace internal { + + template + SparseSmgLraHelper::SparseSmgLraHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const statesOfCoalition) : _transitionMatrix(transitionMatrix), _x1IsCurrent(false), _x1IsCurrentStrategyVI(false), _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; + if (rewardModel.hasStateRewards()) { + stateRewardsGetter = rewardModel.getStateRewardVector(); + } + ValueGetter actionRewardsGetter; + if (rewardModel.hasStateActionRewards() || rewardModel.hasTransitionRewards()) { + if (rewardModel.hasTransitionRewards()) { + actionRewardsGetter = [&] (uint64_t globalChoiceIndex) { return rewardModel.getStateActionAndTransitionReward(globalChoiceIndex, this->_transitionMatrix); }; + } else { + actionRewardsGetter = [&] (uint64_t globalChoiceIndex) { return rewardModel.getStateActionReward(globalChoiceIndex); }; + } + } else { + actionRewardsGetter = [] (uint64_t) { return storm::utility::zero(); }; + } + STORM_LOG_DEBUG("rewards: " << rewardModel.getStateRewardVector()); + prepareMultiplier(env, rewardModel); + performValueIteration(env, rewardModel, stateRewardsGetter, actionRewardsGetter, result); + + return result; + } + + template + void SparseSmgLraHelper::performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector& result, std::vector* choices, std::vector* choiceValues) + { + std::vector choicesForStrategies = std::vector(_transitionMatrix.getRowGroupCount(), 0); + ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); + + do + { + _x1IsCurrent = !_x1IsCurrent; + // Convergent recommender procedure + + _multiplier->multiplyAndReduce(env, _optimizationDirection, xOld(), nullptr, xNew(), &choicesForStrategies, &_statesOfCoalition); + for (size_t i = 0; i < xNew().size(); i++) + { + xNew()[i] = xNew()[i] + stateValueGetter[i]; + } + + storm::storage::BitVector fixedMaxStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MaxStrategy); + storm::storage::BitVector fixedMinStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MinStrategy); + storm::storage::SparseMatrix restrictedMaxMatrix = _transitionMatrix.restrictRows(fixedMaxStrat); + + storm::storage::SparseMatrix restrictedMinMatrix = _transitionMatrix.restrictRows(fixedMinStrat); + + // compute bounds + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MaxSolver(restrictedMaxMatrix); + MaxSolver.setOptimizationDirection(OptimizationDirection::Minimize); + std::vector resultForMax = MaxSolver.computeLongRunAverageRewards(env, rewardModel); + + for (size_t i = 0; i < xNewL().size(); i++) + { + xNewL()[i] = std::max(xOldL()[i], resultForMax[i]); + } + + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MinSolver(restrictedMinMatrix); + MinSolver.setOptimizationDirection(OptimizationDirection::Maximize); + std::vector resultForMin = MinSolver.computeLongRunAverageRewards(env, rewardModel); + + for (size_t i = 0; i < xNewU().size(); i++) + { + xNewU()[i] = std::min(xOldU()[i], resultForMin[i]); + } + + STORM_LOG_DEBUG("xL " << xNewL()); + STORM_LOG_DEBUG("xU " << xNewU()); + + } while (!checkConvergence(precision)); + result = xNewU(); + } + + + template + 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 < rowGroupIndices.size() - 1; state++) { + if ((_minimizerStates[state] && strategy == MinMaxStrategy::MaxStrategy) || (!_minimizerStates[state] && strategy == MinMaxStrategy::MinStrategy)) + continue; + + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + for(uint rowGroupIndex = 0; rowGroupIndex < rowGroupSize; rowGroupIndex++) { + if ((rowGroupIndex) != choices[state]) { + restrictBy.set(rowGroupIndex + rowGroupIndices[state], false); + } + } + } + return restrictBy; + } + + + template + 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; + + _x1L = std::vector(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + _x2L = _x1L; + _x1 = _x1L; + _x2 = _x1; + + _x1U = std::vector(_transitionMatrix.getRowGroupCount(), std::numeric_limits::infinity()); + _x2U = _x1U; + } + + template + bool SparseSmgLraHelper::checkConvergence(ValueType threshold) const { + STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); + // Now check whether the currently produced results are precise enough + STORM_LOG_ASSERT(threshold > storm::utility::zero(), "Did not expect a non-positive threshold."); + auto x1It = xNewL().begin(); + auto x1Ite = xNewL().end(); + auto x2It = xNewU().begin(); + ValueType maxDiff = ((*x2It) - (*x1It)); + ValueType minDiff = maxDiff; + // The difference between maxDiff and minDiff is zero at this point. Thus, it doesn't make sense to check the threshold now. + for (++x1It, ++x2It; x1It != x1Ite; ++x1It, ++x2It) { + ValueType diff = (*x2It - *x1It); + // Potentially update maxDiff or minDiff + bool skipCheck = false; + if (maxDiff < diff) { + maxDiff = diff; + } else if (minDiff > diff) { + minDiff = diff; + } else { + skipCheck = true; + } + // Check convergence + if (!skipCheck && (maxDiff - minDiff) > threshold) { + return false; + } + } + return true; + } + + template + std::vector& SparseSmgLraHelper::xNewL() { + return _x1IsCurrent ? _x1L : _x2L; + } + + 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; + } + + template + std::vector& SparseSmgLraHelper::xNewU() { + return _x1IsCurrent ? _x1U : _x2U; + } + + 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; + } + + template + std::vector& SparseSmgLraHelper::xNew() { + return _x1IsCurrent ? _x1 : _x2; + } + + template + std::vector const& SparseSmgLraHelper::xNew() const { + return _x1IsCurrent ? _x1 : _x2; + } + + + template + void SparseSmgLraHelper::setRelevantStates(storm::storage::BitVector relevantStates){ + _relevantStates = relevantStates; + } + + template + void SparseSmgLraHelper::setValueThreshold(storm::logic::ComparisonType const& comparisonType, const ValueType &thresholdValue) { + _valueThreshold = std::make_pair(comparisonType, thresholdValue); + } + + template + void SparseSmgLraHelper::setOptimizationDirection(storm::solver::OptimizationDirection const& direction) { + _optimizationDirection = direction; + } + + template + void SparseSmgLraHelper::setProduceScheduler(bool value) { + _produceScheduler = value; + } + + template + void SparseSmgLraHelper::setProduceChoiceValues(bool value) { + _produceChoiceValues = value; + } + + template + void SparseSmgLraHelper::setQualitative(bool value) { + _isQualitativeSet = value; + } + + template class SparseSmgLraHelper; +#ifdef STORM_HAVE_CARL + template class SparseSmgLraHelper; +#endif + + } + } + } +} + diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h new file mode 100644 index 000000000..f4bb609e0 --- /dev/null +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h @@ -0,0 +1,154 @@ +#pragma once + +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/BitVector.h" +#include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" +#include "storm/logic/ComparisonType.h" + + +namespace storm { + class Environment; + + + namespace modelchecker { + namespace helper { + namespace internal { + + enum class MinMaxStrategy { + MaxStrategy, + MinStrategy + }; + + template + class SparseSmgLraHelper { + public: + /// Function mapping from indices to values + typedef std::function ValueGetter; + + 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); + + + + void prepareMultiplier(const Environment& env, storm::models::sparse::StandardRewardModel const& rewardModel); + + std::vector computeLongRunAverageRewardsSound(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel); + + void setRelevantStates(storm::storage::BitVector relevantStates); + + void setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& thresholdValue); + + void setOptimizationDirection(storm::solver::OptimizationDirection const& direction); + + void setProduceScheduler(bool value); + + void setProduceChoiceValues(bool value); + + void setQualitative(bool value); + + 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 { + bool isPrecisionAchieved; + ValueType currentValue; + }; + + storm::storage::BitVector getStrategyFixedBitVec(std::vector const& choices, MinMaxStrategy strategy); + + /*! + * 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; + 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 _Tsx1, _Tsx2, _TsChoiceValues; + bool _x1IsCurrent; + bool _x1IsCurrentStrategyVI; + std::vector _Isx, _Isb, _IsChoiceValues; + std::unique_ptr> _multiplier; + std::unique_ptr> _Solver; + std::unique_ptr> _DetIsSolver; + std::unique_ptr _IsSolverEnv; + }; + } + } + } +} diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 30001ce75..6cd0a5560 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -14,6 +14,8 @@ #include "storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h" #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h" +#include "storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h" + #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" #include "storm/logic/FragmentSpecification.h" @@ -240,11 +242,12 @@ namespace storm { template std::unique_ptr SparseSmgRpatlModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask); - storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); + storm::modelchecker::helper::internal::SparseSmgLraHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); - auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + auto values = helper.computeLongRunAverageRewardsSound(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); auto shield = tempest::shields::createQuantitativeShield(std::make_shared>(this->getModel()), helper.getChoiceValues(), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, statesOfCoalition); @@ -253,6 +256,7 @@ namespace storm { if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } + */ return result; }