From 4c514cecdd143f0888c47c991e0eeeaa9d659fe9 Mon Sep 17 00:00:00 2001 From: sp Date: Tue, 5 Nov 2024 14:19:36 +0100 Subject: [PATCH 01/21] L(S) and G(S) (from paper) --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 3 +- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 38 +++ .../rpatl/helper/SparseSmgRpatlHelper.h | 1 + .../helper/internal/SoundGameViHelper.cpp | 255 ++++++++++++++++++ .../rpatl/helper/internal/SoundGameViHelper.h | 119 ++++++++ 5 files changed, 414 insertions(+), 2 deletions(-) create mode 100644 src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp create mode 100644 src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 79cc6fc87..cb110be26 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -141,8 +141,7 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - - auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilitiesSound(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 31ddac9da..784fc27d5 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -9,6 +9,7 @@ #include "storm/utility/vector.h" #include "storm/utility/graph.h" #include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h" +#include "storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h" namespace storm { namespace modelchecker { @@ -59,6 +60,43 @@ namespace storm { return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } + template + SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, statesOfCoalition); + + // Initialize the x vector and solution vector result. + // TODO Fabian: maybe relevant states (later) + std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + // std::transform(xL.begin(), xL.end(), psiStates.begin(), xL, [](double& a) { a *= 3; }) // TODO Fabian + // assigning 1s to the xL vector for all Goal states + assert(xL.size() == psiStates.size()); + for (size_t i = 0; i < xL.size(); i++) + { + if (psiStates[xL.size() - i]) + xL[i] = 1; + } + STORM_LOG_DEBUG("xL " << xL); + std::vector xU = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); + // assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f + assert(xU.size() == probGreater0.size()); + for (size_t i = 0; i < xL.size(); i++) + { + if (probGreater0[i]) + xU[i] = 1; + } + STORM_LOG_DEBUG("xU " << xU); + + std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + // std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); // TODO Fabian: do I need this? + std::vector constrainedChoiceValues; + + viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); + + assert(false); + } + template storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) { storm::storage::Scheduler completeScheduler(psiStates.size()); diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 0592c929b..741d5961d 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -35,6 +35,7 @@ namespace storm { class SparseSmgRpatlHelper { public: static SMGSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); + static SMGSparseModelCheckingHelperReturnType computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); static SMGSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); static SMGSparseModelCheckingHelperReturnType computeNextProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint); static SMGSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound); diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp new file mode 100644 index 000000000..239a89d31 --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -0,0 +1,255 @@ +#include "SoundGameViHelper.h" + +#include "storm/environment/Environment.h" +#include "storm/environment/solver/SolverEnvironment.h" +#include "storm/environment/solver/GameSolverEnvironment.h" + + +#include "storm/utility/SignalHandler.h" +#include "storm/utility/vector.h" + +namespace storm { + namespace modelchecker { + namespace helper { + namespace internal { + + template + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + // Intentionally left empty. + } + + template + void SoundGameViHelper::prepareSolversAndMultipliers(const Environment& env) { + STORM_LOG_DEBUG("\n" << _transitionMatrix); + _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); + _x1IsCurrent = false; + } + + template + void SoundGameViHelper::performValueIteration(Environment const& env, std::vector& xL, std::vector& xU, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues) { + // new pair (x_old, x_new) for over_approximation() + + prepareSolversAndMultipliers(env); + // Get precision for convergence check. + ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); + + STORM_LOG_DEBUG("hello" << "world"); + uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); + //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + _x1L = xL; + _x2L = _x1L; + + _x1U = xU; + _x2U = _x1U; + + if (this->isProduceSchedulerSet()) { + if (!this->_producedOptimalChoices.is_initialized()) { + this->_producedOptimalChoices.emplace(); + } + this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); + } + + uint64_t iter = 0; + constrainedChoiceValues = std::vector(xL.size(), storm::utility::zero()); // ?? + + while (iter < maxIter) { + performIterationStep(env, dir); + if (checkConvergence(precision)) { + //_multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); // TODO Fabian: ??? + break; + } + if (storm::utility::resources::isTerminate()) { + break; + } + ++iter; + } + xL = xNewL(); + xU = xNewU(); + + STORM_LOG_DEBUG("result xL: " << xL); + STORM_LOG_DEBUG("result xU: " << xU); + + if (isProduceSchedulerSet()) { + // We will be doing one more iteration step and track scheduler choices this time. + performIterationStep(env, dir, &_producedOptimalChoices.get()); + } + } + + template + void SoundGameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { + // under approximation + if (!_multiplier) { + prepareSolversAndMultipliers(env); + } + _x1IsCurrent = !_x1IsCurrent; + + if (choices == nullptr) { + _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), nullptr, &_statesOfCoalition); + } else { + _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), choices, &_statesOfCoalition); + } + + // over_approximation + + if (choices == nullptr) { + _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); + } else { + _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), choices, &_statesOfCoalition); + } + + // TODO Fabian: find_MSECs() & deflate() + + } + + template + bool SoundGameViHelper::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 = xOldL().begin(); + auto x1Ite = xOldL().end(); + auto x2It = xNewL().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 + void SoundGameViHelper::setProduceScheduler(bool value) { + _produceScheduler = value; + } + + template + bool SoundGameViHelper::isProduceSchedulerSet() const { + return _produceScheduler; + } + + template + void SoundGameViHelper::setShieldingTask(bool value) { + _shieldingTask = value; + } + + template + bool SoundGameViHelper::isShieldingTask() const { + return _shieldingTask; + } + + template + void SoundGameViHelper::updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix) { + _transitionMatrix = newTransitionMatrix; + } + + template + void SoundGameViHelper::updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition) { + _statesOfCoalition = newStatesOfCoalition; + } + + template + std::vector const& SoundGameViHelper::getProducedOptimalChoices() const { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "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(); + } + + template + std::vector& SoundGameViHelper::getProducedOptimalChoices() { + STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "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(); + } + + template + storm::storage::Scheduler SoundGameViHelper::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; + } + + template + void SoundGameViHelper::getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues) { + _multiplier->multiply(env, x, nullptr, choiceValues); + } + + template + void SoundGameViHelper::fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices) { + std::vector allChoices = std::vector(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero()); + auto choice_it = choiceValues.begin(); + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + if (psiStates.get(state)) { + for(uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + allChoices.at(rowGroupIndices.at(state) + choice) = *choice_it; + } + } + } + choiceValues = allChoices; + } + + template + std::vector& SoundGameViHelper::xNewL() { + return _x1IsCurrent ? _x1L : _x2L; + } + + template + std::vector const& SoundGameViHelper::xNewL() const { + return _x1IsCurrent ? _x1L : _x2L; + } + + template + std::vector& SoundGameViHelper::xOldL() { + return _x1IsCurrent ? _x2L : _x1L; + } + + template + std::vector const& SoundGameViHelper::xOldL() const { + return _x1IsCurrent ? _x2L : _x1L; + } + + template + std::vector& SoundGameViHelper::xNewU() { + return _x1IsCurrent ? _x1U : _x2U; + } + + template + std::vector const& SoundGameViHelper::xNewU() const { + return _x1IsCurrent ? _x1U : _x2U; + } + + template + std::vector& SoundGameViHelper::xOldU() { + return _x1IsCurrent ? _x2U : _x1U; + } + + template + std::vector const& SoundGameViHelper::xOldU() const { + return _x1IsCurrent ? _x2U : _x1U; + } + + template class SoundGameViHelper; +#ifdef STORM_HAVE_CARL + template class SoundGameViHelper; +#endif + } + } + } +} diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h new file mode 100644 index 000000000..f4e3d5b35 --- /dev/null +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -0,0 +1,119 @@ +#pragma once + +#include "storm/storage/SparseMatrix.h" +#include "storm/solver/LinearEquationSolver.h" +#include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" + +namespace storm { + class Environment; + + namespace storage { + template class Scheduler; + } + + namespace modelchecker { + namespace helper { + namespace internal { + + template + class SoundGameViHelper { + public: + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); + + void prepareSolversAndMultipliers(const Environment& env); + + /*! + * Perform value iteration until convergence + */ + void performValueIteration(Environment const& env, std::vector& xL, std::vector& xU, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues); + + /*! + * Sets whether an optimal scheduler shall be constructed during the computation + */ + void setProduceScheduler(bool value); + + /*! + * @return whether an optimal scheduler shall be constructed during the computation + */ + bool isProduceSchedulerSet() const; + + /*! + * Sets whether an optimal scheduler shall be constructed during the computation + */ + void setShieldingTask(bool value); + + /*! + * @return whether an optimal scheduler shall be constructed during the computation + */ + bool isShieldingTask() const; + + /*! + * Changes the transitionMatrix to the given one. + */ + void updateTransitionMatrix(storm::storage::SparseMatrix newTransitionMatrix); + + /*! + * Changes the statesOfCoalition to the given one. + */ + void updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition); + + storm::storage::Scheduler extractScheduler() const; + + void getChoiceValues(Environment const& env, std::vector const& x, std::vector& choiceValues); + + /*! + * Fills the choice values vector to the original size with zeros for ~psiState choices. + */ + void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + + private: + /*! + * Performs one iteration step for value iteration + */ + void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + + /*! + * Checks whether the curently computed value achieves the desired precision + */ + bool checkConvergence(ValueType precision) 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; + + 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. + */ + std::vector const& getProducedOptimalChoices() const; + + /*! + * @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. + */ + std::vector& getProducedOptimalChoices(); + + storm::storage::SparseMatrix _transitionMatrix; + storm::storage::BitVector _statesOfCoalition; + std::vector _x, _x1L, _x2L, _x1U, _x2U; + std::unique_ptr> _multiplier; + + bool _produceScheduler = false; + bool _shieldingTask = false; + boost::optional> _producedOptimalChoices; + }; + } + } + } +} From 61b59e64fc03b8dec1311ced45760720495db59c Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Fri, 19 Jul 2024 11:27:26 +0200 Subject: [PATCH 02/21] reducedMinimizerActions BitVec --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 6 +- .../helper/internal/SoundGameViHelper.cpp | 63 +++++++++++++++---- .../rpatl/helper/internal/SoundGameViHelper.h | 9 ++- 3 files changed, 63 insertions(+), 15 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 784fc27d5..1a346333b 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -63,7 +63,7 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { - storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, statesOfCoalition); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, statesOfCoalition, goal.direction()); // Initialize the x vector and solution vector result. // TODO Fabian: maybe relevant states (later) @@ -73,7 +73,7 @@ namespace storm { assert(xL.size() == psiStates.size()); for (size_t i = 0; i < xL.size(); i++) { - if (psiStates[xL.size() - i]) + if (psiStates[i]) xL[i] = 1; } STORM_LOG_DEBUG("xL " << xL); @@ -81,7 +81,7 @@ namespace storm { storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); // assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f assert(xU.size() == probGreater0.size()); - for (size_t i = 0; i < xL.size(); i++) + for (size_t i = 0; i < xL.size(); i++) // TODO Fabian: do this more efficient { if (probGreater0[i]) xU[i] = 1; diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 239a89d31..a3817540b 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -14,7 +14,7 @@ namespace storm { namespace internal { template - SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) { + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) { // Intentionally left empty. } @@ -23,6 +23,7 @@ namespace storm { STORM_LOG_DEBUG("\n" << _transitionMatrix); _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); _x1IsCurrent = false; + _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; } template @@ -77,30 +78,70 @@ namespace storm { template void SoundGameViHelper::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices) { + storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)}; + // under approximation if (!_multiplier) { prepareSolversAndMultipliers(env); } _x1IsCurrent = !_x1IsCurrent; - if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), nullptr, &_statesOfCoalition); - } else { - _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), choices, &_statesOfCoalition); - } + std::vector choiceValues = xNewL(); + choiceValues.resize(this->_transitionMatrix.getRowCount()); + + _multiplier->multiply(env, xOldL(), nullptr, choiceValues); + reduceChoiceValues(choiceValues, &reducedMinimizerActions); + xNewL() = choiceValues; // over_approximation - if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); - } else { - _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), choices, &_statesOfCoalition); - } + _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); // TODO Fabian: find_MSECs() & deflate() + } + + template + void SoundGameViHelper::reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result) + { + // result BitVec should be initialized with 1s outside the function + // restrict rows + + auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); + auto choice_it = choiceValues.begin(); + STORM_LOG_DEBUG("MinStates " << _minimizerStates); + STORM_LOG_DEBUG("init choiceVal " << choiceValues); + + + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + ValueType optChoice; + if (_minimizerStates[state]) { // check if current state is minimizer state + // getting the optimal minimizer choice for the given state + optChoice = *std::min_element(choice_it, choice_it + rowGroupSize); + + for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + if (*choice_it > optChoice) { + result->set(rowGroupIndices[state] + choice, 0); + } + } + // reducing the xNew() (choiceValues) vector for minimizer states + choiceValues[state] = optChoice; + } + else + { + optChoice = *std::max_element(choice_it, choice_it + rowGroupSize); + // reducing the xNew() (choiceValues) vector for maximizer states + choiceValues[state] = optChoice; + choice_it += rowGroupSize; + } + } + choiceValues.resize(this->_transitionMatrix.getRowGroupCount()); + STORM_LOG_DEBUG("reduced BitVec: " << *result); + STORM_LOG_DEBUG("reduced x Vector: " << choiceValues); } + template bool SoundGameViHelper::checkConvergence(ValueType threshold) const { STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first."); diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index f4e3d5b35..21ec6b464 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -19,7 +19,7 @@ namespace storm { template class SoundGameViHelper { public: - SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition); + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection); void prepareSolversAndMultipliers(const Environment& env); @@ -73,6 +73,10 @@ namespace storm { */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result); + // + // für alle minimizer states -> reduce zu optimal actions + /*! * Checks whether the curently computed value achieves the desired precision */ @@ -92,6 +96,8 @@ namespace storm { bool _x1IsCurrent; + storm::storage::BitVector _minimizerStates; + /*! * @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. @@ -108,6 +114,7 @@ namespace storm { storm::storage::BitVector _statesOfCoalition; std::vector _x, _x1L, _x2L, _x1U, _x2U; std::unique_ptr> _multiplier; + OptimizationDirection _optimizationDirection; bool _produceScheduler = false; bool _shieldingTask = false; From 9a414442171ac9b0b7babc4e777435f60241b42f Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Fri, 19 Jul 2024 17:01:01 +0200 Subject: [PATCH 03/21] finding MSECs done, in progress: deflating the MSECs --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- .../helper/internal/SoundGameViHelper.cpp | 44 ++++++++++++++++--- .../rpatl/helper/internal/SoundGameViHelper.h | 8 ++-- 3 files changed, 44 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 1a346333b..3b824341f 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -63,7 +63,7 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { - storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, statesOfCoalition, goal.direction()); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, goal.direction()); // Initialize the x vector and solution vector result. // TODO Fabian: maybe relevant states (later) diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index a3817540b..198550e6f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -14,7 +14,7 @@ namespace storm { namespace internal { template - SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) { + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) { // Intentionally left empty. } @@ -34,7 +34,6 @@ namespace storm { // Get precision for convergence check. ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); - STORM_LOG_DEBUG("hello" << "world"); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x1L = xL; @@ -97,14 +96,48 @@ namespace storm { _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); + // restricting the none optimal minimizer choices + storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); + + // storage::SparseMatrix restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions); + STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); + // TODO Fabian: find_MSECs() & deflate() + storm::storage::MaximalEndComponentDecomposition MECD = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); + + STORM_LOG_DEBUG("MECD: \n" << MECD); + // deflate(MECD,restrictedTransMatrix, xNewU()); + } + + template + void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU) + { + /* auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); + auto mec_it = MECD.begin(); + + + for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + ValueType optChoice; + if (!_minimizerStates[state]) { // check if current state is maximizer state + // getting the optimal minimizer choice for the given state + optChoice = *std::min_element(choice_it, choice_it + rowGroupSize); + + for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + if (*choice_it > optChoice) { + result->set(rowGroupIndices[state] + choice, 0); + } + } + // reducing the xNew() (choiceValues) vector for minimizer states + choiceValues[state] = optChoice; + } + } */ } template void SoundGameViHelper::reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result) { - // result BitVec should be initialized with 1s outside the function - // restrict rows + // result BitVec should be initialized with 1s outside the method auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); auto choice_it = choiceValues.begin(); @@ -137,8 +170,6 @@ namespace storm { } } choiceValues.resize(this->_transitionMatrix.getRowGroupCount()); - STORM_LOG_DEBUG("reduced BitVec: " << *result); - STORM_LOG_DEBUG("reduced x Vector: " << choiceValues); } @@ -177,6 +208,7 @@ namespace storm { _produceScheduler = value; } + template bool SoundGameViHelper::isProduceSchedulerSet() const { return _produceScheduler; diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index 21ec6b464..f140eb734 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -4,6 +4,7 @@ #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/Multiplier.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" namespace storm { class Environment; @@ -19,7 +20,7 @@ namespace storm { template class SoundGameViHelper { public: - SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection); + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection); void prepareSolversAndMultipliers(const Environment& env); @@ -73,9 +74,9 @@ namespace storm { */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); + void deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU); + void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result); - // - // für alle minimizer states -> reduce zu optimal actions /*! * Checks whether the curently computed value achieves the desired precision @@ -111,6 +112,7 @@ namespace storm { std::vector& getProducedOptimalChoices(); storm::storage::SparseMatrix _transitionMatrix; + storm::storage::SparseMatrix _backwardTransitions; storm::storage::BitVector _statesOfCoalition; std::vector _x, _x1L, _x2L, _x1U, _x2U; std::unique_ptr> _multiplier; From 2de38edbff72e97d222e4c76549117bc08321648 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Thu, 25 Jul 2024 15:35:50 +0200 Subject: [PATCH 04/21] basic implementation done --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 2 +- .../helper/internal/SoundGameViHelper.cpp | 63 ++++++++++--------- .../rpatl/helper/internal/SoundGameViHelper.h | 4 +- 3 files changed, 39 insertions(+), 30 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 3b824341f..29d41b45c 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -63,7 +63,7 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { - storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, goal.direction()); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, goal.direction()); // Initialize the x vector and solution vector result. // TODO Fabian: maybe relevant states (later) diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 198550e6f..d035f6fd7 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -14,7 +14,7 @@ namespace storm { namespace internal { template - SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _optimizationDirection(optimizationDirection) { + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _psiStates(psiStates), _optimizationDirection(optimizationDirection) { // Intentionally left empty. } @@ -98,40 +98,47 @@ namespace storm { // restricting the none optimal minimizer choices storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); + _multiplierRestricted = storm::solver::MultiplierFactory().create(env, restrictedTransMatrix); - // storage::SparseMatrix restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions); - STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); + // storage::SparseMatrix restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions); + // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); - // TODO Fabian: find_MSECs() & deflate() + // find_MSECs() & deflate() storm::storage::MaximalEndComponentDecomposition MECD = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); - STORM_LOG_DEBUG("MECD: \n" << MECD); - // deflate(MECD,restrictedTransMatrix, xNewU()); + // STORM_LOG_DEBUG("MECD: \n" << MECD); + deflate(MECD,restrictedTransMatrix, xNewU()); } template - void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU) - { - /* auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); - auto mec_it = MECD.begin(); - - - for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { - uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; - ValueType optChoice; - if (!_minimizerStates[state]) { // check if current state is maximizer state - // getting the optimal minimizer choice for the given state - optChoice = *std::min_element(choice_it, choice_it + rowGroupSize); - - for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - if (*choice_it > optChoice) { - result->set(rowGroupIndices[state] + choice, 0); + void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU) { + auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); + + // iterating over all MSECs + for (auto smec_it : MECD) { + ValueType bestExit = 0; + for (uint state = 0; state < rowGroupIndices.size() - 1; state++) { + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + if (!_minimizerStates[state] && smec_it.containsState(state)) { // check if current state is maximizer state + // getting the optimal minimizer choice for the given state + + for (uint choice = 0; choice < rowGroupSize; choice++) { + if (!smec_it.containsChoice(state, choice + rowGroupIndices[state])) { + ValueType choiceValue = 0; + _multiplierRestricted->multiplyRow(choice + rowGroupIndices[state], xU, choiceValue); + if (choiceValue > bestExit) + bestExit = choiceValue; + } } } - // reducing the xNew() (choiceValues) vector for minimizer states - choiceValues[state] = optChoice; } - } */ + auto stateSet = smec_it.getStateSet(); + for (auto smec_state : stateSet) + { + if (!_psiStates[smec_state]) + xU[smec_state] = std::min(xU[smec_state], bestExit); + } + } } template @@ -178,9 +185,9 @@ namespace storm { 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 = xOldL().begin(); - auto x1Ite = xOldL().end(); - auto x2It = xNewL().begin(); + 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. diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index f140eb734..5fecd8d87 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -20,7 +20,7 @@ namespace storm { template class SoundGameViHelper { public: - SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, OptimizationDirection const& optimizationDirection); + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection); void prepareSolversAndMultipliers(const Environment& env); @@ -114,8 +114,10 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::SparseMatrix _backwardTransitions; storm::storage::BitVector _statesOfCoalition; + storm::storage::BitVector _psiStates; std::vector _x, _x1L, _x2L, _x1U, _x2U; std::unique_ptr> _multiplier; + std::unique_ptr> _multiplierRestricted; OptimizationDirection _optimizationDirection; bool _produceScheduler = false; From de9a5646b0e9c6fe45d5d6b07b9c5e7d67cdba6b Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Fri, 26 Jul 2024 09:41:42 +0200 Subject: [PATCH 05/21] small performance fix in deflate() --- .../helper/internal/SoundGameViHelper.cpp | 30 ++++++++----------- 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index d035f6fd7..10de545e3 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -80,6 +80,7 @@ namespace storm { storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)}; // under approximation + if (!_multiplier) { prepareSolversAndMultipliers(env); } @@ -100,28 +101,26 @@ namespace storm { storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); _multiplierRestricted = storm::solver::MultiplierFactory().create(env, restrictedTransMatrix); - // storage::SparseMatrix restrictedBackMatrix = this->_backwardTransitions.restrictRows(reducedMinimizerActions); // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); // find_MSECs() & deflate() - storm::storage::MaximalEndComponentDecomposition MECD = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); + storm::storage::MaximalEndComponentDecomposition MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); // STORM_LOG_DEBUG("MECD: \n" << MECD); - deflate(MECD,restrictedTransMatrix, xNewU()); + deflate(MSEC,restrictedTransMatrix, xNewU()); } template - void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU) { + void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MSEC, storage::SparseMatrix const restrictedMatrix, std::vector& xU) { auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); // iterating over all MSECs - for (auto smec_it : MECD) { + for (auto smec_it : MSEC) { ValueType bestExit = 0; - for (uint state = 0; state < rowGroupIndices.size() - 1; state++) { + auto stateSet = smec_it.getStateSet(); + for (uint state : stateSet) { uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; - if (!_minimizerStates[state] && smec_it.containsState(state)) { // check if current state is maximizer state - // getting the optimal minimizer choice for the given state - + if (!_minimizerStates[state]) { // check if current state is maximizer state for (uint choice = 0; choice < rowGroupSize; choice++) { if (!smec_it.containsChoice(state, choice + rowGroupIndices[state])) { ValueType choiceValue = 0; @@ -132,11 +131,10 @@ namespace storm { } } } - auto stateSet = smec_it.getStateSet(); - for (auto smec_state : stateSet) - { - if (!_psiStates[smec_state]) - xU[smec_state] = std::min(xU[smec_state], bestExit); + // deflating the states of the current MSEC + for (uint state : stateSet) { + if (!_psiStates[state]) + xU[state] = std::min(xU[state], bestExit); } } } @@ -149,10 +147,6 @@ namespace storm { auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); auto choice_it = choiceValues.begin(); - STORM_LOG_DEBUG("MinStates " << _minimizerStates); - STORM_LOG_DEBUG("init choiceVal " << choiceValues); - - for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; ValueType optChoice; From 877067cdcca13bd6204b21cddbb7821b30d985eb Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Fri, 26 Jul 2024 10:29:46 +0200 Subject: [PATCH 06/21] SparseSmgRpatlHelper.cpp added return value --- src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp | 3 +++ .../modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp | 1 - 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 29d41b45c..566120827 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -64,6 +64,8 @@ namespace storm { SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, goal.direction()); + std::unique_ptr> scheduler; + storm::storage::BitVector relevantStates(psiStates.size(), true); // Initialize the x vector and solution vector result. // TODO Fabian: maybe relevant states (later) @@ -93,6 +95,7 @@ namespace storm { std::vector constrainedChoiceValues; viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); + return SMGSparseModelCheckingHelperReturnType(std::move(xU), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); assert(false); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 10de545e3..5a7109cac 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -28,7 +28,6 @@ namespace storm { template void SoundGameViHelper::performValueIteration(Environment const& env, std::vector& xL, std::vector& xU, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues) { - // new pair (x_old, x_new) for over_approximation() prepareSolversAndMultipliers(env); // Get precision for convergence check. From 986d1183aa91485f0d3aa592177b51aa289a48d4 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Fri, 9 Aug 2024 11:04:18 +0200 Subject: [PATCH 07/21] bug fixes and optimizations --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 2 + .../rpatl/helper/SparseSmgRpatlHelper.cpp | 16 ++-- .../helper/internal/SoundGameViHelper.cpp | 91 ++++++++++++------- .../rpatl/helper/internal/SoundGameViHelper.h | 5 +- src/storm/storage/MaximalEndComponent.cpp | 16 +++- src/storm/storage/MaximalEndComponent.h | 11 +++ 6 files changed, 96 insertions(+), 45 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index cb110be26..30001ce75 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -142,6 +142,7 @@ namespace storm { ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilitiesSound(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); @@ -151,6 +152,7 @@ namespace storm { if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } + //STORM_LOG_DEBUG(result); return result; } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 566120827..e3dc2d8ee 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -83,11 +83,13 @@ namespace storm { storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); // assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f assert(xU.size() == probGreater0.size()); - for (size_t i = 0; i < xL.size(); i++) // TODO Fabian: do this more efficient - { - if (probGreater0[i]) - xU[i] = 1; - } + auto xU_begin = xU.begin(); + std::for_each(xU.begin(), xU.end(), [&probGreater0, &xU_begin](ValueType &it) + { + if (probGreater0[&it - &(*xU_begin)]) + it = 1; + }); + STORM_LOG_DEBUG("xU " << xU); std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); @@ -95,9 +97,9 @@ namespace storm { std::vector constrainedChoiceValues; viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); - return SMGSparseModelCheckingHelperReturnType(std::move(xU), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); - assert(false); + STORM_LOG_DEBUG(xU); + return SMGSparseModelCheckingHelperReturnType(std::move(xU), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } template diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 5a7109cac..732127ce9 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -84,62 +84,82 @@ namespace storm { prepareSolversAndMultipliers(env); } _x1IsCurrent = !_x1IsCurrent; + std::vector choiceValuesL = std::vector(this->_transitionMatrix.getRowCount(), storm::utility::zero()); - std::vector choiceValues = xNewL(); - choiceValues.resize(this->_transitionMatrix.getRowCount()); - - _multiplier->multiply(env, xOldL(), nullptr, choiceValues); - reduceChoiceValues(choiceValues, &reducedMinimizerActions); - xNewL() = choiceValues; + _multiplier->multiply(env, xOldL(), nullptr, choiceValuesL); + reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL()); // over_approximation - _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); + std::vector choiceValuesU = std::vector(this->_transitionMatrix.getRowCount(), storm::utility::zero()); + + _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); + reduceChoiceValues(choiceValuesU, nullptr, xNewU()); + + //_multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); // restricting the none optimal minimizer choices storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); - _multiplierRestricted = storm::solver::MultiplierFactory().create(env, restrictedTransMatrix); // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); - // find_MSECs() & deflate() + // find_MSECs() storm::storage::MaximalEndComponentDecomposition MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); - // STORM_LOG_DEBUG("MECD: \n" << MECD); - deflate(MSEC,restrictedTransMatrix, xNewU()); + // STORM_LOG_DEBUG("MECD: \n" << MSEC); + + // reducing the choiceValuesU + size_t i = 0; + auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { + bool ret = !(reducedMinimizerActions[i]); + i++; + return ret; + }); + choiceValuesU.erase(new_end, choiceValuesU.end()); + + // deflating the MSECs + deflate(MSEC, restrictedTransMatrix, xNewU(), choiceValuesU); } template - void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MSEC, storage::SparseMatrix const restrictedMatrix, std::vector& xU) { + void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MSEC, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues) { auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); + auto choice_begin = choiceValues.begin(); // iterating over all MSECs for (auto smec_it : MSEC) { ValueType bestExit = 0; + if (smec_it.isErgodic(restrictedMatrix)) continue; // TODO Fabian: ?? isErgodic undefined ref auto stateSet = smec_it.getStateSet(); for (uint state : stateSet) { - uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; - if (!_minimizerStates[state]) { // check if current state is maximizer state - for (uint choice = 0; choice < rowGroupSize; choice++) { - if (!smec_it.containsChoice(state, choice + rowGroupIndices[state])) { - ValueType choiceValue = 0; - _multiplierRestricted->multiplyRow(choice + rowGroupIndices[state], xU, choiceValue); - if (choiceValue > bestExit) - bestExit = choiceValue; - } - } - } + if (_minimizerStates[state]) continue; + uint rowGroupIndex = rowGroupIndices[state]; + auto exitingCompare = [&state, &smec_it, &choice_begin](const ValueType &lhs, const ValueType &rhs) + { + bool lhsExiting = !smec_it.containsChoice(state, (&lhs - &(*choice_begin))); + bool rhsExiting = !smec_it.containsChoice(state, (&rhs - &(*choice_begin))); + if( lhsExiting && !rhsExiting) return false; + if(!lhsExiting && rhsExiting) return true; + if(!lhsExiting && !rhsExiting) return false; + return lhs < rhs; + }; + uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndex; + + auto choice_it = choice_begin + rowGroupIndex; + ValueType newBestExit = *std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare); + if (newBestExit > bestExit) + bestExit = newBestExit; } // deflating the states of the current MSEC for (uint state : stateSet) { - if (!_psiStates[state]) - xU[state] = std::min(xU[state], bestExit); + if (_psiStates[state]) continue; + xU[state] = std::min(xU[state], bestExit); } } } template - void SoundGameViHelper::reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result) + void SoundGameViHelper::reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result, std::vector& x) { // result BitVec should be initialized with 1s outside the method @@ -153,23 +173,26 @@ namespace storm { // getting the optimal minimizer choice for the given state optChoice = *std::min_element(choice_it, choice_it + rowGroupSize); - for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { - if (*choice_it > optChoice) { - result->set(rowGroupIndices[state] + choice, 0); + if (result != nullptr) { + for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) { + if (*choice_it > optChoice) { + result->set(rowGroupIndices[state] + choice, 0); + } } } - // reducing the xNew() (choiceValues) vector for minimizer states - choiceValues[state] = optChoice; + else + choice_it += rowGroupSize; + // reducing the xNew() vector for minimizer states + x[state] = optChoice; } else { optChoice = *std::max_element(choice_it, choice_it + rowGroupSize); - // reducing the xNew() (choiceValues) vector for maximizer states - choiceValues[state] = optChoice; + // reducing the xNew() vector for maximizer states + x[state] = optChoice; choice_it += rowGroupSize; } } - choiceValues.resize(this->_transitionMatrix.getRowGroupCount()); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index 5fecd8d87..f738958ca 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -74,9 +74,9 @@ namespace storm { */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - void deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU); + void deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues); - void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result); + void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result, std::vector& x); /*! * Checks whether the curently computed value achieves the desired precision @@ -117,7 +117,6 @@ namespace storm { storm::storage::BitVector _psiStates; std::vector _x, _x1L, _x2L, _x1U, _x2U; std::unique_ptr> _multiplier; - std::unique_ptr> _multiplierRestricted; OptimizationDirection _optimizationDirection; bool _produceScheduler = false; diff --git a/src/storm/storage/MaximalEndComponent.cpp b/src/storm/storage/MaximalEndComponent.cpp index aa7453277..d4f51e089 100644 --- a/src/storm/storage/MaximalEndComponent.cpp +++ b/src/storm/storage/MaximalEndComponent.cpp @@ -4,7 +4,6 @@ namespace storm { namespace storage { - std::ostream& operator<<(std::ostream& out, storm::storage::FlatSet const& block); MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() { @@ -100,6 +99,18 @@ namespace storm { return stateChoicePair->second.find(choice) != stateChoicePair->second.end(); } + template + bool MaximalEndComponent::isErgodic(storm::storage::SparseMatrix transitionMatrix) const { + auto rowGroupIndices = transitionMatrix.getRowGroupIndices(); + for (auto state : this->getStateSet()) + { + if (getChoicesForState(state).size() == (rowGroupIndices[state + 1] - rowGroupIndices[state])) continue; + return false; + } + return true; + } + + MaximalEndComponent::set_type MaximalEndComponent::getStateSet() const { set_type states; states.reserve(stateToChoicesMapping.size()); @@ -136,5 +147,8 @@ namespace storm { MaximalEndComponent::const_iterator MaximalEndComponent::end() const { return stateToChoicesMapping.end(); } + + template bool MaximalEndComponent::isErgodic(storm::storage::SparseMatrix transitionMatrix) const; + template bool MaximalEndComponent::isErgodic(storm::storage::SparseMatrix transitionMatrix) const; } } diff --git a/src/storm/storage/MaximalEndComponent.h b/src/storm/storage/MaximalEndComponent.h index a1d5b37c2..66c1d1c4a 100644 --- a/src/storm/storage/MaximalEndComponent.h +++ b/src/storm/storage/MaximalEndComponent.h @@ -5,6 +5,7 @@ #include "storm/storage/sparse/StateType.h" #include "storm/storage/BoostTypes.h" +#include "storm/storage/SparseMatrix.h" namespace storm { namespace storage { @@ -20,6 +21,7 @@ namespace storm { typedef std::unordered_map map_type; typedef map_type::iterator iterator; typedef map_type::const_iterator const_iterator; + /*! * Creates an empty MEC. @@ -124,6 +126,15 @@ namespace storm { * @return True if the given choice is contained in the MEC. */ bool containsChoice(uint_fast64_t state, uint_fast64_t choice) const; + + /*! + * Retrieves wether the MEC is ergodic or not i.e. wether the MEC is exitable or not + * + * @param transitionMatrix the given transition matrix + * @return True if the MEC is ergodic + */ + template + bool isErgodic(storm::storage::SparseMatrix transitionMatrix) const; /*! * Retrieves the set of states contained in the MEC. From 1e40b9e5a3ca642b0ba5c092e6b1088392171d80 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 20 Aug 2024 11:27:43 +0200 Subject: [PATCH 08/21] SmgRpatlModelCheckerTest.cpp: added test for deflate method of SoundGameViHelper.cpp --- .../examples/testfiles/smg/example_smg.nm | 28 ++++ .../helper/internal/SoundGameViHelper.cpp | 5 +- .../rpatl/helper/internal/SoundGameViHelper.h | 11 +- src/storm/storage/MaximalEndComponent.h | 2 +- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 153 ++++++++++++++++++ 5 files changed, 189 insertions(+), 10 deletions(-) create mode 100644 resources/examples/testfiles/smg/example_smg.nm diff --git a/resources/examples/testfiles/smg/example_smg.nm b/resources/examples/testfiles/smg/example_smg.nm new file mode 100644 index 000000000..0050b1028 --- /dev/null +++ b/resources/examples/testfiles/smg/example_smg.nm @@ -0,0 +1,28 @@ +smg + +const double p = 2/3; + +player maxP + [q_action1], [q_action2] +endplayer + +player minP + [p_action1] +endplayer + +player sinkstates + state_space +endplayer + + +module state_space + s : [0..3]; + + [p_action1] s=0 -> (s'=1); + + [q_action1] s=1 -> (s'=0); + [q_action2] s=1 -> (1-p) : (s'=1) + (p/2) : (s'=2) + (p/2) : (s'=3); + + [] s=2 -> true; + [] s=3 -> true; +endmodule diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 732127ce9..e305c3be7 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -96,8 +96,6 @@ namespace storm { _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); reduceChoiceValues(choiceValuesU, nullptr, xNewU()); - //_multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition); - // restricting the none optimal minimizer choices storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); @@ -124,12 +122,11 @@ namespace storm { template void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MSEC, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues) { auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); - auto choice_begin = choiceValues.begin(); // iterating over all MSECs for (auto smec_it : MSEC) { ValueType bestExit = 0; - if (smec_it.isErgodic(restrictedMatrix)) continue; // TODO Fabian: ?? isErgodic undefined ref + if (smec_it.isErgodic(restrictedMatrix)) continue; auto stateSet = smec_it.getStateSet(); for (uint state : stateSet) { if (_minimizerStates[state]) continue; diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index f738958ca..d8a0d7907 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -68,16 +68,18 @@ namespace storm { */ void fillChoiceValuesVector(std::vector& choiceValues, storm::storage::BitVector psiStates, std::vector::index_type> rowGroupIndices); + void deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues); + + 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 */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - void deflate(storm::storage::MaximalEndComponentDecomposition const MECD, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues); - - void reduceChoiceValues(std::vector& choiceValues, storm::storage::BitVector* result, std::vector& x); - /*! * Checks whether the curently computed value achieves the desired precision */ @@ -116,7 +118,6 @@ namespace storm { storm::storage::BitVector _statesOfCoalition; storm::storage::BitVector _psiStates; std::vector _x, _x1L, _x2L, _x1U, _x2U; - std::unique_ptr> _multiplier; OptimizationDirection _optimizationDirection; bool _produceScheduler = false; diff --git a/src/storm/storage/MaximalEndComponent.h b/src/storm/storage/MaximalEndComponent.h index 66c1d1c4a..448159804 100644 --- a/src/storm/storage/MaximalEndComponent.h +++ b/src/storm/storage/MaximalEndComponent.h @@ -128,7 +128,7 @@ namespace storm { bool containsChoice(uint_fast64_t state, uint_fast64_t choice) const; /*! - * Retrieves wether the MEC is ergodic or not i.e. wether the MEC is exitable or not + * Retrieves whether the MEC is ergodic or not i.e. wether the MEC is exitable or not * * @param transitionMatrix the given transition matrix * @return True if the MEC is ergodic diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 79217c614..d634ec6b2 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -17,6 +17,11 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/logic/Formulas.h" #include "storm/exceptions/UncheckedRequirementException.h" +#include "storm/solver/Multiplier.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/utility/graph.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" +#include "storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h" namespace { @@ -114,6 +119,7 @@ namespace { std::vector> getTasks(std::vector> const& formulas) const { std::vector> result; for (auto const& f : formulas) { + std::cout << *f << std::endl; result.emplace_back(*f); } return result; @@ -345,5 +351,152 @@ namespace { EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + TYPED_TEST(SmgRpatlModelCheckerTest, Deflate) { + typedef double ValueType; + std::string formulasString = " <> Pmax=? [F (s=2)]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/example_smg.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + auto transitionMatrix = model->getTransitionMatrix(); + + + auto formulas = std::move(modelFormulas.second); + + storm::logic::GameFormula const& gameFormula = formulas[0]->asGameFormula(); + + storm::modelchecker::CheckTask checkTask(gameFormula); + + storm::storage::BitVector statesOfCoalition = model->computeStatesOfCoalition(gameFormula.getCoalition()); + statesOfCoalition.complement(); + + // TODO Fabian: get optimization direction + + storm::storage::BitVector psiStates = checker->check(this->env(), gameFormula.getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asStateFormula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + storm::storage::BitVector phiStates(model->getNumberOfStates(), true); + + storm::storage::SparseMatrix backwardTransitions = model->getBackwardTransitions(); + storm::OptimizationDirection optimizationDirection = storm::OptimizationDirection::Maximize; + auto minimizerStates = optimizationDirection == storm::OptimizationDirection::Maximize ? statesOfCoalition : ~statesOfCoalition; + + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, optimizationDirection); + viHelper.prepareSolversAndMultipliers(this->env()); + + std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + for (size_t i = 0; i < xL.size(); i++) + { + if (psiStates[i]) + xL[i] = 1; + } + + std::vector xU = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); + auto xU_begin = xU.begin(); + std::for_each(xU.begin(), xU.end(), [&probGreater0, &xU_begin](ValueType &it) + { + if (probGreater0[&it - &(*xU_begin)]) + it = 1; + }); + + // performValueIteration + std::vector _x1L = xL; + std::vector _x2L = _x1L; + + std::vector _x1U = xU; + std::vector _x2U = _x1U; + + // perform first iteration step + storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)}; + std::vector choiceValuesL = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x2L, nullptr, choiceValuesL); + + viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x1L); + + + // over approximation + std::vector choiceValuesU = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x2U, nullptr, choiceValuesU); + viHelper.reduceChoiceValues(choiceValuesU, nullptr, _x1U); + + storm::storage::SparseMatrix restrictedTransMatrix = transitionMatrix.restrictRows(reducedMinimizerActions); + + storm::storage::MaximalEndComponentDecomposition MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, backwardTransitions); + + // reducing the choiceValuesU + size_t i = 0; + auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { + bool ret = !(reducedMinimizerActions[i]); + i++; + return ret; + }); + choiceValuesU.erase(new_end, choiceValuesU.end()); + + // deflating the MSECs + viHelper.deflate(MSEC, restrictedTransMatrix, _x1U, choiceValuesU); + + xL = _x1L; + xU = _x1U; + + EXPECT_NEAR(this->parseNumber("0"), xL[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.333333"), xL[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xL[3], this->precision()); + + EXPECT_NEAR(this->parseNumber("0.666666"), xU[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.666666"), xU[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + + // second iteration step + + reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)}; + choiceValuesL = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x1L, nullptr, choiceValuesL); + + viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x2L); + + + // over approximation + choiceValuesU = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); + + viHelper._multiplier->multiply(this->env(), _x1U, nullptr, choiceValuesU); + viHelper.reduceChoiceValues(choiceValuesU, nullptr, _x2U); + + restrictedTransMatrix = transitionMatrix.restrictRows(reducedMinimizerActions); + + MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, backwardTransitions); + + // reducing the choiceValuesU + i = 0; + new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { + bool ret = !(reducedMinimizerActions[i]); + i++; + return ret; + }); + choiceValuesU.erase(new_end, choiceValuesU.end()); + + // deflating the MSECs + viHelper.deflate(MSEC, restrictedTransMatrix, _x2U, choiceValuesU); + + xL = _x2L; + xU = _x2U; + + EXPECT_NEAR(this->parseNumber("0.333333"), xL[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.444444"), xL[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xL[3], this->precision()); + + EXPECT_NEAR(this->parseNumber("0.555555"), xU[0], this->precision()); + EXPECT_NEAR(this->parseNumber("0.555555"), xU[1], this->precision()); + EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); + EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + + } + // TODO: create more test cases (files) } From 3b0eeb1e882472c489d8919158c01f1e04495252 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 20 Aug 2024 13:23:06 +0200 Subject: [PATCH 09/21] SmgRpatlModelCheckerTest.cpp: google tests for MSECs --- .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 134 ++++++++++++++++++ 1 file changed, 134 insertions(+) diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index d634ec6b2..d4f0c8694 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -426,6 +426,73 @@ namespace { storm::storage::MaximalEndComponentDecomposition MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, backwardTransitions); + // testing MSEC + // ===================================================== + ASSERT_TRUE(MSEC.size() == 3); + storm::storage::MaximalEndComponent const& mec1 = MSEC[0]; + if (mec1.containsState(0)) { + ASSERT_TRUE(mec1.containsState(1)); + ASSERT_FALSE(mec1.containsState(2)); + ASSERT_FALSE(mec1.containsState(3)); + } + else if (mec1.containsState(2)) { + ASSERT_FALSE(mec1.containsState(0)); + ASSERT_FALSE(mec1.containsState(1)); + ASSERT_FALSE(mec1.containsState(3)); + } + else if (mec1.containsState(3)) { + ASSERT_FALSE(mec1.containsState(0)); + ASSERT_FALSE(mec1.containsState(1)); + ASSERT_FALSE(mec1.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + + storm::storage::MaximalEndComponent const& mec2 = MSEC[1]; + if (mec2.containsState(0)) { + ASSERT_TRUE(mec2.containsState(1)); + ASSERT_FALSE(mec2.containsState(2)); + ASSERT_FALSE(mec2.containsState(3)); + } + else if (mec2.containsState(2)) { + ASSERT_FALSE(mec2.containsState(0)); + ASSERT_FALSE(mec2.containsState(1)); + ASSERT_FALSE(mec2.containsState(3)); + } + else if (mec2.containsState(3)) { + ASSERT_FALSE(mec2.containsState(0)); + ASSERT_FALSE(mec2.containsState(1)); + ASSERT_FALSE(mec2.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + + storm::storage::MaximalEndComponent const& mec3 = MSEC[2]; + if (mec3.containsState(0)) { + ASSERT_TRUE(mec3.containsState(1)); + ASSERT_FALSE(mec3.containsState(2)); + ASSERT_FALSE(mec3.containsState(3)); + } + else if (mec3.containsState(2)) { + ASSERT_FALSE(mec3.containsState(0)); + ASSERT_FALSE(mec3.containsState(1)); + ASSERT_FALSE(mec3.containsState(3)); + } + else if (mec3.containsState(3)) { + ASSERT_FALSE(mec3.containsState(0)); + ASSERT_FALSE(mec3.containsState(1)); + ASSERT_FALSE(mec3.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + // ===================================================== + // reducing the choiceValuesU size_t i = 0; auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { @@ -471,6 +538,73 @@ namespace { MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, backwardTransitions); + // testing MSEC + // ===================================================== + ASSERT_TRUE(MSEC.size() == 3); + storm::storage::MaximalEndComponent const& mec4 = MSEC[0]; + if (mec4.containsState(0)) { + ASSERT_TRUE(mec4.containsState(1)); + ASSERT_FALSE(mec4.containsState(2)); + ASSERT_FALSE(mec4.containsState(3)); + } + else if (mec4.containsState(2)) { + ASSERT_FALSE(mec4.containsState(0)); + ASSERT_FALSE(mec4.containsState(1)); + ASSERT_FALSE(mec4.containsState(3)); + } + else if (mec4.containsState(3)) { + ASSERT_FALSE(mec4.containsState(0)); + ASSERT_FALSE(mec4.containsState(1)); + ASSERT_FALSE(mec4.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + + storm::storage::MaximalEndComponent const& mec5 = MSEC[1]; + if (mec5.containsState(0)) { + ASSERT_TRUE(mec5.containsState(1)); + ASSERT_FALSE(mec5.containsState(2)); + ASSERT_FALSE(mec5.containsState(3)); + } + else if (mec5.containsState(2)) { + ASSERT_FALSE(mec5.containsState(0)); + ASSERT_FALSE(mec5.containsState(1)); + ASSERT_FALSE(mec5.containsState(3)); + } + else if (mec5.containsState(3)) { + ASSERT_FALSE(mec5.containsState(0)); + ASSERT_FALSE(mec5.containsState(1)); + ASSERT_FALSE(mec5.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + + storm::storage::MaximalEndComponent const& mec6 = MSEC[2]; + if (mec6.containsState(0)) { + ASSERT_TRUE(mec6.containsState(1)); + ASSERT_FALSE(mec6.containsState(2)); + ASSERT_FALSE(mec6.containsState(3)); + } + else if (mec6.containsState(2)) { + ASSERT_FALSE(mec6.containsState(0)); + ASSERT_FALSE(mec6.containsState(1)); + ASSERT_FALSE(mec6.containsState(3)); + } + else if (mec6.containsState(3)) { + ASSERT_FALSE(mec6.containsState(0)); + ASSERT_FALSE(mec6.containsState(1)); + ASSERT_FALSE(mec6.containsState(2)); + } + else { + // This case must never happen + ASSERT_TRUE(false); + } + // ===================================================== + // reducing the choiceValuesU i = 0; new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { From 81c0dbc50fa016163fa19f45f2eb13d90fc41a6c Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 20 Aug 2024 13:37:22 +0200 Subject: [PATCH 10/21] removed all std::cout --- .../modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index d4f0c8694..cd37d9875 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -119,7 +119,6 @@ namespace { std::vector> getTasks(std::vector> const& formulas) const { std::vector> result; for (auto const& f : formulas) { - std::cout << *f << std::endl; result.emplace_back(*f); } return result; @@ -412,7 +411,6 @@ namespace { std::vector choiceValuesL = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); viHelper._multiplier->multiply(this->env(), _x2L, nullptr, choiceValuesL); - viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x1L); @@ -518,13 +516,11 @@ namespace { EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); - // second iteration step - + // perform second iteration step reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)}; choiceValuesL = std::vector(transitionMatrix.getRowCount(), storm::utility::zero()); viHelper._multiplier->multiply(this->env(), _x1L, nullptr, choiceValuesL); - viHelper.reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, _x2L); From 470fd302aa82bb9d3c68374a3d222451f3f00e88 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Wed, 21 Aug 2024 10:34:31 +0200 Subject: [PATCH 11/21] getting optimization direction via CheckTask --- resources/examples/testfiles/smg/example_smg.nm | 4 ++++ .../rpatl/smg/SmgRpatlModelCheckerTest.cpp | 11 +++++++---- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/resources/examples/testfiles/smg/example_smg.nm b/resources/examples/testfiles/smg/example_smg.nm index 0050b1028..875070051 100644 --- a/resources/examples/testfiles/smg/example_smg.nm +++ b/resources/examples/testfiles/smg/example_smg.nm @@ -1,3 +1,7 @@ +// taken from Julia Eisentraut "Value iteration for simple stochastic games: Stopping criterion +// and learning algorithm" - Fig. 1 + + smg const double p = 2/3; diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index cd37d9875..765d08135 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -361,9 +361,7 @@ namespace { std::unique_ptr result; auto transitionMatrix = model->getTransitionMatrix(); - auto formulas = std::move(modelFormulas.second); - storm::logic::GameFormula const& gameFormula = formulas[0]->asGameFormula(); storm::modelchecker::CheckTask checkTask(gameFormula); @@ -371,13 +369,12 @@ namespace { storm::storage::BitVector statesOfCoalition = model->computeStatesOfCoalition(gameFormula.getCoalition()); statesOfCoalition.complement(); - // TODO Fabian: get optimization direction storm::storage::BitVector psiStates = checker->check(this->env(), gameFormula.getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asStateFormula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector phiStates(model->getNumberOfStates(), true); storm::storage::SparseMatrix backwardTransitions = model->getBackwardTransitions(); - storm::OptimizationDirection optimizationDirection = storm::OptimizationDirection::Maximize; + storm::OptimizationDirection optimizationDirection = gameFormula.getSubformula().asOperatorFormula().getOptimalityType(); auto minimizerStates = optimizationDirection == storm::OptimizationDirection::Maximize ? statesOfCoalition : ~statesOfCoalition; storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, optimizationDirection); @@ -506,6 +503,8 @@ namespace { xL = _x1L; xU = _x1U; + // testing x vectors + // ===================================================== EXPECT_NEAR(this->parseNumber("0"), xL[0], this->precision()); EXPECT_NEAR(this->parseNumber("0.333333"), xL[1], this->precision()); EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); @@ -515,6 +514,7 @@ namespace { EXPECT_NEAR(this->parseNumber("0.666666"), xU[1], this->precision()); EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + // ===================================================== // perform second iteration step reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)}; @@ -616,6 +616,8 @@ namespace { xL = _x2L; xU = _x2U; + // testing x vectors + // ===================================================== EXPECT_NEAR(this->parseNumber("0.333333"), xL[0], this->precision()); EXPECT_NEAR(this->parseNumber("0.444444"), xL[1], this->precision()); EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); @@ -625,6 +627,7 @@ namespace { EXPECT_NEAR(this->parseNumber("0.555555"), xU[1], this->precision()); EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + // ===================================================== } From 5107b5904cf6590ed6f6b6590d5de4914786ac61 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 1 Oct 2024 12:04:49 +0200 Subject: [PATCH 12/21] optimization: searching for MSECs only if policy changed --- .../helper/internal/SoundGameViHelper.cpp | 85 +++++++++++++------ .../rpatl/helper/internal/SoundGameViHelper.h | 14 ++- 2 files changed, 71 insertions(+), 28 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index e305c3be7..41dc61b50 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -14,7 +14,7 @@ namespace storm { namespace internal { template - SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _psiStates(psiStates), _optimizationDirection(optimizationDirection) { + SoundGameViHelper::SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector b, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection) : _transitionMatrix(transitionMatrix), _backwardTransitions(backwardTransitions), _statesOfCoalition(statesOfCoalition), _psiStates(psiStates), _optimizationDirection(optimizationDirection), _b(b) { // Intentionally left empty. } @@ -24,6 +24,8 @@ namespace storm { _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); _x1IsCurrent = false; _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; + _oldPolicy = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); + _timing = std::vector(5, 0); } template @@ -37,6 +39,8 @@ namespace storm { //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x1L = xL; _x2L = _x1L; + _x1Test = _x1L; + _x2Test = _x1L; _x1U = xU; _x2U = _x1U; @@ -65,8 +69,8 @@ namespace storm { xL = xNewL(); xU = xNewU(); - STORM_LOG_DEBUG("result xL: " << xL); - STORM_LOG_DEBUG("result xU: " << xU); + // for profiling + STORM_PRINT(_timing[0] << ", " << _timing[1] << ", " << _timing[2] << ", " << _timing[3] << ", " << _timing[4] << std::endl); if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. @@ -79,7 +83,7 @@ namespace storm { storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)}; // under approximation - + auto start = std::chrono::steady_clock::now(); if (!_multiplier) { prepareSolversAndMultipliers(env); } @@ -89,23 +93,42 @@ namespace storm { _multiplier->multiply(env, xOldL(), nullptr, choiceValuesL); reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL()); - // over_approximation + // just for debugging + _multiplier->multiplyAndReduce(env, _optimizationDirection, xOldTest(), nullptr, xNewTest(), nullptr, &_statesOfCoalition); + + // over_approximation std::vector choiceValuesU = std::vector(this->_transitionMatrix.getRowCount(), storm::utility::zero()); _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); reduceChoiceValues(choiceValuesU, nullptr, xNewU()); - // restricting the none optimal minimizer choices - storage::SparseMatrix restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions); + auto finish = std::chrono::steady_clock::now(); + double elapsed_seconds = std::chrono::duration_cast< + std::chrono::duration>(finish - start).count(); + _timing[0] += elapsed_seconds; - // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); + if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed + start = std::chrono::steady_clock::now(); - // find_MSECs() - storm::storage::MaximalEndComponentDecomposition MSEC = storm::storage::MaximalEndComponentDecomposition(restrictedTransMatrix, _backwardTransitions); + // restricting the none optimal minimizer choices + _restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions); - // STORM_LOG_DEBUG("MECD: \n" << MSEC); + finish = std::chrono::steady_clock::now(); + elapsed_seconds = std::chrono::duration_cast>(finish - start).count(); + _timing[1] += elapsed_seconds; + // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); + start = std::chrono::steady_clock::now(); + // find_MSECs() + _MSECs = storm::storage::MaximalEndComponentDecomposition(_restrictedTransitions, _restrictedTransitions.transpose(true)); + + finish = std::chrono::steady_clock::now(); + elapsed_seconds = std::chrono::duration_cast>(finish - start).count(); + _timing[2] += elapsed_seconds; + } + + start = std::chrono::steady_clock::now(); // reducing the choiceValuesU size_t i = 0; auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { @@ -114,9 +137,19 @@ namespace storm { return ret; }); choiceValuesU.erase(new_end, choiceValuesU.end()); + finish = std::chrono::steady_clock::now(); + elapsed_seconds = std::chrono::duration_cast< + std::chrono::duration>(finish - start).count(); + _timing[3] += elapsed_seconds; + _oldPolicy = reducedMinimizerActions; // deflating the MSECs - deflate(MSEC, restrictedTransMatrix, xNewU(), choiceValuesU); + start = std::chrono::steady_clock::now(); + deflate(_MSECs, _restrictedTransitions, xNewU(), choiceValuesU); + finish = std::chrono::steady_clock::now(); + elapsed_seconds = std::chrono::duration_cast< + std::chrono::duration>(finish - start).count(); + _timing[4] += elapsed_seconds; } template @@ -177,8 +210,9 @@ namespace storm { } } } - else + else { choice_it += rowGroupSize; + } // reducing the xNew() vector for minimizer states x[state] = optChoice; } @@ -201,22 +235,11 @@ namespace storm { 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) { + for (; 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) { + if (diff > threshold) { return false; } } @@ -338,6 +361,16 @@ namespace storm { return _x1IsCurrent ? _x2U : _x1U; } + template + std::vector& SoundGameViHelper::xOldTest() { + return _x1IsCurrent ? _x2Test : _x1Test; + } + + template + std::vector& SoundGameViHelper::xNewTest() { + return _x1IsCurrent ? _x1Test : _x2Test; + } + template class SoundGameViHelper; #ifdef STORM_HAVE_CARL template class SoundGameViHelper; diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index d8a0d7907..ad78bee56 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -20,7 +20,7 @@ namespace storm { template class SoundGameViHelper { public: - SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection); + SoundGameViHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector b, storm::storage::BitVector statesOfCoalition, storm::storage::BitVector psiStates, OptimizationDirection const& optimizationDirection); void prepareSolversAndMultipliers(const Environment& env); @@ -97,6 +97,10 @@ namespace storm { std::vector& xOldU(); std::vector const& xOldU() const; + std::vector& xNewTest(); + + std::vector& xOldTest(); + bool _x1IsCurrent; storm::storage::BitVector _minimizerStates; @@ -115,14 +119,20 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::SparseMatrix _backwardTransitions; + storm::storage::SparseMatrix _restrictedTransitions; + storm::storage::BitVector _oldPolicy; storm::storage::BitVector _statesOfCoalition; storm::storage::BitVector _psiStates; - std::vector _x, _x1L, _x2L, _x1U, _x2U; + std::vector _x, _x1L, _x2L, _x1U, _x2U, _x1Test, _x2Test, _b; OptimizationDirection _optimizationDirection; + storm::storage::MaximalEndComponentDecomposition _MSECs; + bool _produceScheduler = false; bool _shieldingTask = false; boost::optional> _producedOptimalChoices; + + std::vector _timing; }; } } From 26094b08ce4393775e27bcd57fc39bc594b6531b Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 1 Oct 2024 12:07:24 +0200 Subject: [PATCH 13/21] WIP Sound LRA for games --- .../internal/SparseSmgLraHelper.cpp | 271 ++++++++++++++++++ .../internal/SparseSmgLraHelper.h | 154 ++++++++++ .../rpatl/SparseSmgRpatlModelChecker.cpp | 8 +- 3 files changed, 431 insertions(+), 2 deletions(-) create mode 100644 src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp create mode 100644 src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h 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; } From 621e9f679405ddc16b1d7f769bc47e0ac8a7949e Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 1 Oct 2024 12:09:17 +0200 Subject: [PATCH 14/21] optimization: WIP relevant states for game VI --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 56 +++++++++++++------ 1 file changed, 38 insertions(+), 18 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index e3dc2d8ee..88f2bd1a2 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -22,8 +22,7 @@ namespace storm { // Relevant states are those states which are phiStates and not PsiStates. storm::storage::BitVector relevantStates = phiStates & ~psiStates; - - // Initialize the x vector and solution vector result. + // Initialize the x vector and solution vector result. std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); @@ -62,44 +61,65 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { + STORM_LOG_DEBUG("statesOfCoalition: " << statesOfCoalition << std::endl); + + storm::storage::BitVector prob1 = storm::utility::graph::performProb1(backwardTransitions, phiStates, psiStates); + storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); + STORM_LOG_DEBUG("probGreater0: " << probGreater0 << std::endl); + + - storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, goal.direction()); std::unique_ptr> scheduler; - storm::storage::BitVector relevantStates(psiStates.size(), true); + storm::storage::BitVector relevantStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); // TODO Fabian + + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); // Initialize the x vector and solution vector result. - // TODO Fabian: maybe relevant states (later) - std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + std::vector xL = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + auto xL_begin = xL.begin(); + std::for_each(xL.begin(), xL.end(), [&prob1, &xL_begin](ValueType &it) + { + if (prob1[&it - &(*xL_begin)]) + it = 1; + }); // std::transform(xL.begin(), xL.end(), psiStates.begin(), xL, [](double& a) { a *= 3; }) // TODO Fabian // assigning 1s to the xL vector for all Goal states - assert(xL.size() == psiStates.size()); - for (size_t i = 0; i < xL.size(); i++) - { - if (psiStates[i]) - xL[i] = 1; - } - STORM_LOG_DEBUG("xL " << xL); std::vector xU = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); // assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f - assert(xU.size() == probGreater0.size()); auto xU_begin = xU.begin(); std::for_each(xU.begin(), xU.end(), [&probGreater0, &xU_begin](ValueType &it) { if (probGreater0[&it - &(*xU_begin)]) it = 1; }); - - STORM_LOG_DEBUG("xU " << xU); + /*size_t i = 0; + auto new_end = std::remove_if(xU.begin(), xU.end(), [&relevantStates, &i](const auto& item) { + bool ret = !(relevantStates[i]); + i++; + return ret; + }); + xU.erase(new_end, xU.end()); + xU.resize(relevantStates.getNumberOfSetBits()); */ std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); + + // STORM_LOG_DEBUG(transitionMatrix); + STORM_LOG_DEBUG("b: " << b); + storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); + clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); // std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); // TODO Fabian: do I need this? std::vector constrainedChoiceValues; + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, b, statesOfCoalition, psiStates, goal.direction()); + viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); + storm::utility::vector::setVectorValues(result, relevantStates, xU); + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + STORM_LOG_DEBUG(xU); - return SMGSparseModelCheckingHelperReturnType(std::move(xU), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); + return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } template From 8f187f46f12ae95ee50b31a725766361af0cd236 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Wed, 9 Oct 2024 21:10:52 +0200 Subject: [PATCH 15/21] debug: Sound Game VI now fully debugged (fixed Find_MSEC), WIP: produce scheduler --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 1 - .../rpatl/helper/SparseSmgRpatlHelper.cpp | 50 +++++------ .../helper/internal/SoundGameViHelper.cpp | 90 ++++++++----------- .../rpatl/helper/internal/SoundGameViHelper.h | 6 +- 4 files changed, 63 insertions(+), 84 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 6cd0a5560..9239f0578 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -154,7 +154,6 @@ namespace storm { if (checkTask.isProduceSchedulersSet() && ret.scheduler) { result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); } - //STORM_LOG_DEBUG(result); return result; } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 88f2bd1a2..31dc8cea7 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -61,29 +61,30 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { - STORM_LOG_DEBUG("statesOfCoalition: " << statesOfCoalition << std::endl); - storm::storage::BitVector prob1 = storm::utility::graph::performProb1(backwardTransitions, phiStates, psiStates); storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); - STORM_LOG_DEBUG("probGreater0: " << probGreater0 << std::endl); - - - std::unique_ptr> scheduler; - storm::storage::BitVector relevantStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); // TODO Fabian + storm::storage::BitVector relevantStates = phiStates; storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); // Initialize the x vector and solution vector result. - std::vector xL = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); + std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + // assigning 1s to the xL vector for all Goal states auto xL_begin = xL.begin(); - std::for_each(xL.begin(), xL.end(), [&prob1, &xL_begin](ValueType &it) + std::for_each(xL.begin(), xL.end(), [&psiStates, &xL_begin](ValueType &it) { - if (prob1[&it - &(*xL_begin)]) + if (psiStates[&it - &(*xL_begin)]) it = 1; }); - // std::transform(xL.begin(), xL.end(), psiStates.begin(), xL, [](double& a) { a *= 3; }) // TODO Fabian - // assigning 1s to the xL vector for all Goal states + size_t i = 0; + auto new_end = std::remove_if(xL.begin(), xL.end(), [&relevantStates, &i](const auto& item) { + bool ret = !(relevantStates[i]); + i++; + return ret; + }); + xL.erase(new_end, xL.end()); + xL.resize(relevantStates.getNumberOfSetBits()); std::vector xU = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f auto xU_begin = xU.begin(); @@ -92,33 +93,32 @@ namespace storm { if (probGreater0[&it - &(*xU_begin)]) it = 1; }); - /*size_t i = 0; - auto new_end = std::remove_if(xU.begin(), xU.end(), [&relevantStates, &i](const auto& item) { + i = 0; + auto new_end_U = std::remove_if(xU.begin(), xU.end(), [&relevantStates, &i](const auto& item) { bool ret = !(relevantStates[i]); i++; return ret; }); - xU.erase(new_end, xU.end()); - xU.resize(relevantStates.getNumberOfSetBits()); */ + xU.erase(new_end_U, xU.end()); + xU.resize(relevantStates.getNumberOfSetBits()); + + storm::storage::BitVector clippedPsiStates(relevantStates.getNumberOfSetBits()); + clippedPsiStates.setClippedStatesOfCoalition(relevantStates, psiStates); - std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates); + std::vector result = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - // STORM_LOG_DEBUG(transitionMatrix); - STORM_LOG_DEBUG("b: " << b); storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits()); clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); - // std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); // TODO Fabian: do I need this? - std::vector constrainedChoiceValues; + std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); - storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, b, statesOfCoalition, psiStates, goal.direction()); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, clippedPsiStates, goal.direction()); viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); - storm::utility::vector::setVectorValues(result, relevantStates, xU); - storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + storm::utility::vector::setVectorValues(result, relevantStates, xL); - STORM_LOG_DEBUG(xU); return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 41dc61b50..4cea25c18 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -20,7 +20,6 @@ namespace storm { template void SoundGameViHelper::prepareSolversAndMultipliers(const Environment& env) { - STORM_LOG_DEBUG("\n" << _transitionMatrix); _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); _x1IsCurrent = false; _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; @@ -39,13 +38,11 @@ namespace storm { //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); _x1L = xL; _x2L = _x1L; - _x1Test = _x1L; - _x2Test = _x1L; _x1U = xU; _x2U = _x1U; - if (this->isProduceSchedulerSet()) { + if (this->isProduceSchedulerSet()) { // TODO Fabian scheduler !!! if (!this->_producedOptimalChoices.is_initialized()) { this->_producedOptimalChoices.emplace(); } @@ -53,12 +50,19 @@ namespace storm { } uint64_t iter = 0; - constrainedChoiceValues = std::vector(xL.size(), storm::utility::zero()); // ?? + constrainedChoiceValues = std::vector(xL.size(), storm::utility::zero()); while (iter < maxIter) { performIterationStep(env, dir); if (checkConvergence(precision)) { - //_multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); // TODO Fabian: ??? + // one last iteration for shield + _multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); + storm::storage::BitVector psiStates = _psiStates; + auto xL_begin = xNewL().begin(); + std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it){ + if (psiStates[&it - &(*xL_begin)]) + it = 1; + }); break; } if (storm::utility::resources::isTerminate()) { @@ -69,13 +73,10 @@ namespace storm { xL = xNewL(); xU = xNewU(); - // for profiling - STORM_PRINT(_timing[0] << ", " << _timing[1] << ", " << _timing[2] << ", " << _timing[3] << ", " << _timing[4] << std::endl); - - if (isProduceSchedulerSet()) { + /* if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. performIterationStep(env, dir, &_producedOptimalChoices.get()); - } + } */ } template @@ -92,21 +93,25 @@ namespace storm { _multiplier->multiply(env, xOldL(), nullptr, choiceValuesL); reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL()); - - - // just for debugging - _multiplier->multiplyAndReduce(env, _optimizationDirection, xOldTest(), nullptr, xNewTest(), nullptr, &_statesOfCoalition); + storm::storage::BitVector psiStates = _psiStates; + auto xL_begin = xNewL().begin(); + std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it) + { + if (psiStates[&it - &(*xL_begin)]) + it = 1; + }); // over_approximation std::vector choiceValuesU = std::vector(this->_transitionMatrix.getRowCount(), storm::utility::zero()); _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); reduceChoiceValues(choiceValuesU, nullptr, xNewU()); - - auto finish = std::chrono::steady_clock::now(); - double elapsed_seconds = std::chrono::duration_cast< - std::chrono::duration>(finish - start).count(); - _timing[0] += elapsed_seconds; + auto xU_begin = xNewU().begin(); + std::for_each(xNewU().begin(), xNewU().end(), [&psiStates, &xU_begin](ValueType &it) + { + if (psiStates[&it - &(*xU_begin)]) + it = 1; + }); if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed start = std::chrono::steady_clock::now(); @@ -114,21 +119,10 @@ namespace storm { // restricting the none optimal minimizer choices _restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions); - finish = std::chrono::steady_clock::now(); - elapsed_seconds = std::chrono::duration_cast>(finish - start).count(); - _timing[1] += elapsed_seconds; - - // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix); - start = std::chrono::steady_clock::now(); // find_MSECs() _MSECs = storm::storage::MaximalEndComponentDecomposition(_restrictedTransitions, _restrictedTransitions.transpose(true)); - - finish = std::chrono::steady_clock::now(); - elapsed_seconds = std::chrono::duration_cast>(finish - start).count(); - _timing[2] += elapsed_seconds; } - start = std::chrono::steady_clock::now(); // reducing the choiceValuesU size_t i = 0; auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { @@ -137,31 +131,28 @@ namespace storm { return ret; }); choiceValuesU.erase(new_end, choiceValuesU.end()); - finish = std::chrono::steady_clock::now(); - elapsed_seconds = std::chrono::duration_cast< - std::chrono::duration>(finish - start).count(); - _timing[3] += elapsed_seconds; + _oldPolicy = reducedMinimizerActions; // deflating the MSECs - start = std::chrono::steady_clock::now(); deflate(_MSECs, _restrictedTransitions, xNewU(), choiceValuesU); - finish = std::chrono::steady_clock::now(); - elapsed_seconds = std::chrono::duration_cast< - std::chrono::duration>(finish - start).count(); - _timing[4] += elapsed_seconds; } template void SoundGameViHelper::deflate(storm::storage::MaximalEndComponentDecomposition const MSEC, storage::SparseMatrix const restrictedMatrix, std::vector& xU, std::vector choiceValues) { + auto rowGroupIndices = restrictedMatrix.getRowGroupIndices(); auto choice_begin = choiceValues.begin(); // iterating over all MSECs for (auto smec_it : MSEC) { ValueType bestExit = 0; - if (smec_it.isErgodic(restrictedMatrix)) continue; + // if (smec_it.isErgodic(restrictedMatrix)) continue; auto stateSet = smec_it.getStateSet(); for (uint state : stateSet) { + if (_psiStates[state]) { + bestExit = 1; + break; + } if (_minimizerStates[state]) continue; uint rowGroupIndex = rowGroupIndices[state]; auto exitingCompare = [&state, &smec_it, &choice_begin](const ValueType &lhs, const ValueType &rhs) @@ -176,13 +167,16 @@ namespace storm { uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndex; auto choice_it = choice_begin + rowGroupIndex; - ValueType newBestExit = *std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare); + auto it = std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare); + ValueType newBestExit = 0; + if (!smec_it.containsChoice(state, it - choice_begin)) { + newBestExit = *it; + } if (newBestExit > bestExit) bestExit = newBestExit; } // deflating the states of the current MSEC for (uint state : stateSet) { - if (_psiStates[state]) continue; xU[state] = std::min(xU[state], bestExit); } } @@ -361,16 +355,6 @@ namespace storm { return _x1IsCurrent ? _x2U : _x1U; } - template - std::vector& SoundGameViHelper::xOldTest() { - return _x1IsCurrent ? _x2Test : _x1Test; - } - - template - std::vector& SoundGameViHelper::xNewTest() { - return _x1IsCurrent ? _x1Test : _x2Test; - } - template class SoundGameViHelper; #ifdef STORM_HAVE_CARL template class SoundGameViHelper; diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h index ad78bee56..45d583b7b 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h @@ -97,10 +97,6 @@ namespace storm { std::vector& xOldU(); std::vector const& xOldU() const; - std::vector& xNewTest(); - - std::vector& xOldTest(); - bool _x1IsCurrent; storm::storage::BitVector _minimizerStates; @@ -123,7 +119,7 @@ namespace storm { storm::storage::BitVector _oldPolicy; storm::storage::BitVector _statesOfCoalition; storm::storage::BitVector _psiStates; - std::vector _x, _x1L, _x2L, _x1U, _x2U, _x1Test, _x2Test, _b; + std::vector _x, _x1L, _x2L, _x1U, _x2U, _b; OptimizationDirection _optimizationDirection; storm::storage::MaximalEndComponentDecomposition _MSECs; From bb72102e501e54277ed9c3c5ef0b4b9529af7b59 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Fri, 11 Oct 2024 16:49:31 +0200 Subject: [PATCH 16/21] produceShield: small fix, produceScheduler: implemented --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 15 +++++++++++++-- .../rpatl/helper/SparseSmgRpatlHelper.h | 2 +- .../helper/internal/SoundGameViHelper.cpp | 19 ++++++++++++------- 3 files changed, 26 insertions(+), 10 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 31dc8cea7..ddf04ea90 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -114,16 +114,24 @@ namespace storm { storm::modelchecker::helper::internal::SoundGameViHelper viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, clippedPsiStates, goal.direction()); + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } + viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); storm::utility::vector::setVectorValues(result, relevantStates, xL); + if (produceScheduler) { + scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); + } + return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); } template - storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates) { + storm::storage::Scheduler SparseSmgRpatlHelper::expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates, bool sound) { storm::storage::Scheduler completeScheduler(psiStates.size()); uint_fast64_t maybeStatesCounter = 0; uint schedulerSize = psiStates.size(); @@ -131,6 +139,9 @@ namespace storm { // psiStates already fulfill formulae so we can set an arbitrary action if(psiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); + if (sound) { + maybeStatesCounter++; + } // ~phiStates do not fulfill formulae so we can set an arbitrary action } else if(notPhiStates.get(stateCounter)) { completeScheduler.setChoice(0, stateCounter); @@ -149,7 +160,7 @@ namespace storm { storm::storage::BitVector notPsiStates = ~psiStates; statesOfCoalition.complement(); - auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); + auto result = computeUntilProbabilitiesSound(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); for (auto& element : result.values) { element = storm::utility::one() - element; } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h index 741d5961d..c0216d23f 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.h @@ -41,7 +41,7 @@ namespace storm { static SMGSparseModelCheckingHelperReturnType computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound); static SMGSparseModelCheckingHelperReturnType computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound, bool computeBoundedGlobally = false); private: - static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates); + static storm::storage::Scheduler expandScheduler(storm::storage::Scheduler scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates, bool sound = false); static void expandChoiceValues(std::vector const& rowGroupIndices, storm::storage::BitVector const& relevantStates, std::vector const& constrainedChoiceValues, std::vector& choiceValues); }; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index 4cea25c18..e42179764 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -50,7 +50,7 @@ namespace storm { } uint64_t iter = 0; - constrainedChoiceValues = std::vector(xL.size(), storm::utility::zero()); + constrainedChoiceValues = std::vector(_transitionMatrix.getRowCount(), storm::utility::zero()); while (iter < maxIter) { performIterationStep(env, dir); @@ -73,10 +73,18 @@ namespace storm { xL = xNewL(); xU = xNewU(); - /* if (isProduceSchedulerSet()) { + if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. - performIterationStep(env, dir, &_producedOptimalChoices.get()); - } */ + _x1IsCurrent = !_x1IsCurrent; + _multiplier->multiplyAndReduce(env, dir, xOldL(), nullptr, xNewL(), &_producedOptimalChoices.get(), &_statesOfCoalition); + storm::storage::BitVector psiStates = _psiStates; + auto xL_begin = xNewL().begin(); + std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it) + { + if (psiStates[&it - &(*xL_begin)]) + it = 1; + }); + } } template @@ -84,7 +92,6 @@ namespace storm { storm::storage::BitVector reducedMinimizerActions = {storm::storage::BitVector(this->_transitionMatrix.getRowCount(), true)}; // under approximation - auto start = std::chrono::steady_clock::now(); if (!_multiplier) { prepareSolversAndMultipliers(env); } @@ -114,8 +121,6 @@ namespace storm { }); if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed - start = std::chrono::steady_clock::now(); - // restricting the none optimal minimizer choices _restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions); From 5453d910c315428969717f94b484784e84851c4f Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Mon, 21 Oct 2024 16:29:21 +0200 Subject: [PATCH 17/21] reach/safety fully implemented --- .../rpatl/SparseSmgRpatlModelChecker.cpp | 48 ++++++++++++++++--- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 43 ++++++++++++----- .../helper/internal/SoundGameViHelper.cpp | 2 +- 3 files changed, 73 insertions(+), 20 deletions(-) diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index 9239f0578..7fa177d2c 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp @@ -143,7 +143,28 @@ namespace storm { ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilitiesSound(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + if (env.solver().isForceSoundness()) { + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilitiesSound( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), + checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); + + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if(checkTask.isShieldingTask()) { + storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true); + auto shield = tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), allStatesBv, ~statesOfCoalition); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; + } + + auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper::computeUntilProbabilities( + env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), + this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), + checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint()); STORM_LOG_DEBUG(ret.values); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { @@ -241,12 +262,28 @@ 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::internal::SparseSmgLraHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); - storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); - auto values = helper.computeLongRunAverageRewardsSound(env, rewardModel.get()); + 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()); + 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); + result->asExplicitQuantitativeCheckResult().setShield(std::move(shield)); + } + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); + } + return result; + } + + storm::modelchecker::helper::SparseNondeterministicGameInfiniteHorizonHelper helper(this->getModel().getTransitionMatrix(), statesOfCoalition); + auto values = helper.computeLongRunAverageRewards(env, rewardModel.get()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); 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); @@ -255,7 +292,6 @@ namespace storm { if (checkTask.isProduceSchedulersSet()) { result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler())); } - */ return result; } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index ddf04ea90..e2a349a50 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -61,13 +61,10 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) { - storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates); std::unique_ptr> scheduler; storm::storage::BitVector relevantStates = phiStates; - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); - // Initialize the x vector and solution vector result. std::vector xL = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); // assigning 1s to the xL vector for all Goal states @@ -112,19 +109,24 @@ namespace storm { clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); std::vector constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); - storm::modelchecker::helper::internal::SoundGameViHelper viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, clippedPsiStates, goal.direction()); + if (!relevantStates.empty()) { + storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); + storm::modelchecker::helper::internal::SoundGameViHelper viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, + clippedPsiStates, goal.direction()); - if (produceScheduler) { - viHelper.setProduceScheduler(true); - } + if (produceScheduler) { + viHelper.setProduceScheduler(true); + } - viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); + viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues); - viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); - storm::utility::vector::setVectorValues(result, relevantStates, xL); + viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices()); + storm::utility::vector::setVectorValues(result, relevantStates, xL); - if (produceScheduler) { - scheduler = std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates)); + if (produceScheduler) { + scheduler = + std::make_unique>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates, true)); + } } return SMGSparseModelCheckingHelperReturnType(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues)); @@ -160,7 +162,22 @@ namespace storm { storm::storage::BitVector notPsiStates = ~psiStates; statesOfCoalition.complement(); - auto result = computeUntilProbabilitiesSound(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint); + if (env.solver().isForceSoundness()) { + auto result = computeUntilProbabilitiesSound(env, std::move(goal), transitionMatrix, backwardTransitions, + storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, + qualitative, statesOfCoalition, produceScheduler, hint); + for (auto& element : result.values) { + element = storm::utility::one() - element; + } + for (auto& element : result.choiceValues) { + element = storm::utility::one() - element; + } + return result; + } + + auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, + storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, + qualitative, statesOfCoalition, produceScheduler, hint); for (auto& element : result.values) { element = storm::utility::one() - element; } diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp index e42179764..a91fc03b6 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp @@ -42,7 +42,7 @@ namespace storm { _x1U = xU; _x2U = _x1U; - if (this->isProduceSchedulerSet()) { // TODO Fabian scheduler !!! + if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { this->_producedOptimalChoices.emplace(); } From c8acbc6834835a5e63440b786b5b99e650b1ef63 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Mon, 21 Oct 2024 16:30:09 +0200 Subject: [PATCH 18/21] WIP: LRA fully implemented, scheduler and shield still to be debugged --- .../internal/SparseSmgLraHelper.cpp | 196 ++++++++++++++---- .../internal/SparseSmgLraHelper.h | 20 +- 2 files changed, 169 insertions(+), 47 deletions(-) diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp index 92df53597..307f4d889 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp @@ -29,9 +29,9 @@ namespace storm { template std::vector SparseSmgLraHelper::computeLongRunAverageRewardsSound(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel) { - STORM_LOG_DEBUG("Transition Matrix:\n" << _transitionMatrix); + // STORM_LOG_DEBUG("Transition Matrix:\n" << _transitionMatrix); std::vector result; - std::vector stateRewardsGetter; + std::vector stateRewardsGetter = std::vector(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); if (rewardModel.hasStateRewards()) { stateRewardsGetter = rewardModel.getStateRewardVector(); } @@ -45,60 +45,104 @@ namespace storm { } else { actionRewardsGetter = [] (uint64_t) { return storm::utility::zero(); }; } - STORM_LOG_DEBUG("rewards: " << rewardModel.getStateRewardVector()); + std::vector b = getBVector(stateRewardsGetter, actionRewardsGetter); + + // If requested, allocate memory for the choices made + if (this->_produceScheduler) { + if (!this->_producedOptimalChoices.is_initialized()) { + _producedOptimalChoices.emplace(); + } + _producedOptimalChoices->resize(_transitionMatrix.getRowGroupCount()); + } + prepareMultiplier(env, rewardModel); - performValueIteration(env, rewardModel, stateRewardsGetter, actionRewardsGetter, result); + performValueIteration(env, rewardModel, b, 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 SparseSmgLraHelper::getBVector(std::vector const& stateRewardsGetter, ValueGetter const& actionRewardsGetter) { + std::vector b = std::vector(_transitionMatrix.getRowCount()); + size_t globalChoiceCount = 0; + auto rowGroupIndices = _transitionMatrix.getRowGroupIndices(); + for (size_t state = 0; state < _transitionMatrix.getRowGroupCount(); state++) { + size_t rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state]; + for (size_t choice = 0; choice < rowGroupSize; choice++, globalChoiceCount++) + { + b[globalChoiceCount] = stateRewardsGetter[state] + actionRewardsGetter(globalChoiceCount); + } + } + return b; + } + + template + void SparseSmgLraHelper::performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& b, 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()); + 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()); do { - _x1IsCurrent = !_x1IsCurrent; + size_t iteration_count = 0; // 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]; - } + _multiplier->multiplyAndReduce(env, _optimizationDirection, xNew(), &b, xNew(), &choicesForStrategies, &_statesOfCoalition); + if (iteration_count % 5 == 0) { // only every 5th iteration 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); + if (fixedMaxStrat != _fixedMaxStrat) { + storm::storage::SparseMatrix restrictedMaxMatrix = _transitionMatrix.restrictRows(fixedMaxStrat); + + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MaxSolver(restrictedMaxMatrix); + MaxSolver.setOptimizationDirection(OptimizationDirection::Minimize); + _resultForMax = MaxSolver.computeLongRunAverageRewards(envMinMax, rewardModel); + STORM_LOG_DEBUG("resultMax: " << _resultForMax); + _fixedMaxStrat = fixedMaxStrat; + + for (size_t i = 0; i < xNewL().size(); i++) { + xNewL()[i] = std::max(xNewL()[i], _resultForMax[i]); + } + } - for (size_t i = 0; i < xNewL().size(); i++) - { - xNewL()[i] = std::max(xOldL()[i], resultForMax[i]); - } + if (fixedMinStrat != _fixedMinStrat) { + storm::storage::SparseMatrix restrictedMinMatrix = _transitionMatrix.restrictRows(fixedMinStrat); - storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MinSolver(restrictedMinMatrix); - MinSolver.setOptimizationDirection(OptimizationDirection::Maximize); - std::vector resultForMin = MinSolver.computeLongRunAverageRewards(env, rewardModel); + storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper MinSolver(restrictedMinMatrix); + MinSolver.setOptimizationDirection(OptimizationDirection::Maximize); + _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(xOldU()[i], resultForMin[i]); + for (size_t i = 0; i < xNewU().size(); i++) { + xNewU()[i] = std::min(xNewU()[i], _resultForMin[i]); + } + } } STORM_LOG_DEBUG("xL " << xNewL()); STORM_LOG_DEBUG("xU " << xNewU()); } while (!checkConvergence(precision)); - result = xNewU(); + + if (_produceScheduler) { + _multiplier->multiplyAndReduce(env, _optimizationDirection, xNew(), &b, xNew(), &_producedOptimalChoices.get(), &_statesOfCoalition); + } + + if (_produceChoiceValues) { + if (!this->_choiceValues.is_initialized()) { + this->_choiceValues.emplace(); + } + this->_choiceValues->resize(this->_transitionMatrix.getRowCount()); + _choiceValues = calcChoiceValues(envMinMax, rewardModel); + } + result = xNewL(); } @@ -108,7 +152,7 @@ namespace storm { auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices(); STORM_LOG_DEBUG("choices " << choices); - for(uint state = 0; state < rowGroupIndices.size() - 1; state++) { + for(uint state = 0; state < _transitionMatrix.getRowGroupCount(); state++) { if ((_minimizerStates[state] && strategy == MinMaxStrategy::MaxStrategy) || (!_minimizerStates[state] && strategy == MinMaxStrategy::MinStrategy)) continue; @@ -122,6 +166,75 @@ namespace storm { return restrictBy; } + template + std::vector SparseSmgLraHelper::calcChoiceValues(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel) { + std::vector choiceValues(_transitionMatrix.getRowCount()); + + 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; + } + + template + std::vector SparseSmgLraHelper::getChoiceValues() const { + STORM_LOG_ASSERT(_produceChoiceValues, "Trying to get the computed choice values although this was not requested."); + STORM_LOG_ASSERT(this->_choiceValues.is_initialized(), "Trying to get the computed choice values but none were available. Was there a computation call before?"); + return this->_choiceValues.get(); + } + + template + 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; + } + + template + 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(); + } template void SparseSmgLraHelper::prepareMultiplier(const Environment& env, storm::models::sparse::StandardRewardModel const& rewardModel) @@ -134,6 +247,12 @@ namespace storm { _x1 = _x1L; _x2 = _x1; + _fixedMaxStrat = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); + _fixedMinStrat = storm::storage::BitVector(_transitionMatrix.getRowCount(), false); + + _resultForMin = std::vector(_transitionMatrix.getRowGroupCount()); + _resultForMax = std::vector(_transitionMatrix.getRowGroupCount()); + _x1U = std::vector(_transitionMatrix.getRowGroupCount(), std::numeric_limits::infinity()); _x2U = _x1U; } @@ -146,22 +265,9 @@ namespace storm { 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) { + for (; 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) { + if (diff > threshold) { return false; } } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h index f4bb609e0..d9be65770 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h @@ -24,7 +24,7 @@ namespace storm { template class SparseSmgLraHelper { public: - /// Function mapping from indices to values + // Function mapping from indices to values typedef std::function ValueGetter; SparseSmgLraHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const statesOfCoalition); @@ -42,7 +42,11 @@ namespace storm { */ 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; + storm::storage::Scheduler extractScheduler() const; + + std::vector const& getProducedOptimalChoices() const; void prepareMultiplier(const Environment& env, storm::models::sparse::StandardRewardModel const& rewardModel); @@ -91,6 +95,10 @@ namespace storm { storm::storage::BitVector getStrategyFixedBitVec(std::vector const& choices, MinMaxStrategy strategy); + std::vector getBVector(std::vector const& stateRewardsGetter, ValueGetter const& actionRewardsGetter); + + std::vector calcChoiceValues(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel); + /*! * Must be called between two calls of performIterationStep. */ @@ -128,9 +136,14 @@ namespace storm { storm::storage::BitVector const _statesOfCoalition; ValueType _strategyVIPrecision; - storm::storage::BitVector _relevantStates; storm::storage::BitVector _minimizerStates; + + storm::storage::BitVector _fixedMinStrat; + storm::storage::BitVector _fixedMaxStrat; + std::vector _resultForMax; + std::vector _resultForMin; + boost::optional> _valueThreshold; storm::solver::OptimizationDirection _optimizationDirection; bool _produceScheduler; @@ -147,6 +160,9 @@ namespace storm { std::unique_ptr> _Solver; std::unique_ptr> _DetIsSolver; std::unique_ptr _IsSolverEnv; + + boost::optional> _producedOptimalChoices; + boost::optional> _choiceValues; }; } } From 8846a976f28bb2fd76860aa1bc5015be94e74bd4 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 29 Oct 2024 09:05:25 +0100 Subject: [PATCH 19/21] Game LRA Sound algorithm fully debugged --- .../internal/SparseSmgLraHelper.cpp | 129 +++++------------- .../internal/SparseSmgLraHelper.h | 61 +-------- .../rpatl/SparseSmgRpatlModelChecker.cpp | 4 +- .../helper/internal/SoundGameViHelper.cpp | 7 +- 4 files changed, 44 insertions(+), 157 deletions(-) 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); } From 54f36dd36980ab5bcefa90284554e820a85d418b Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 29 Oct 2024 09:32:27 +0100 Subject: [PATCH 20/21] SparseSmgLraHelper: cleaned up --- .../internal/SparseSmgLraHelper.cpp | 19 ++++++++----------- .../internal/SparseSmgLraHelper.h | 9 +-------- 2 files changed, 9 insertions(+), 19 deletions(-) diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp index ffeacaf3d..6b8f63739 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.cpp @@ -17,6 +17,8 @@ #include "modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" #include "storm/exceptions/UnmetRequirementException.h" +#define SOLVE_MDP 50 + namespace storm { namespace modelchecker { namespace helper { @@ -55,7 +57,7 @@ namespace storm { } prepareMultiplier(env, rewardModel); - performValueIteration(env, rewardModel, _b, actionRewardsGetter, result); + performValueIteration(env, rewardModel, _b, result); return result; } @@ -76,7 +78,7 @@ namespace storm { } template - void SparseSmgLraHelper::performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& b, ValueGetter const& actionValueGetter, std::vector& result, std::vector* choices, std::vector* choiceValues) + void SparseSmgLraHelper::performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& b, std::vector& result) { std::vector choicesForStrategies = std::vector(_transitionMatrix.getRowGroupCount(), 0); auto precision = storm::utility::convertNumber(env.solver().lra().getPrecision()); @@ -90,28 +92,24 @@ namespace storm { _multiplier->multiplyAndReduce(env, _optimizationDirection, xNew(), &b, xNew(), &choicesForStrategies, &_statesOfCoalition); - 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); + if (iteration_count % SOLVE_MDP == 0) { // only every 50th iteration + storm::storage::BitVector fixedMaxStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MaxStrategy); + storm::storage::BitVector fixedMinStrat = getStrategyFixedBitVec(choicesForStrategies, MinMaxStrategy::MinStrategy); - // compute bounds + // 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); _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) { @@ -126,7 +124,6 @@ namespace storm { for (size_t i = 0; i < xNewU().size(); i++) { xNewU()[i] = std::min(xNewU()[i], _resultForMin[i]); } - STORM_LOG_DEBUG("xU " << xNewU()[0]); } } diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h index 5fb8bf205..4a6537945 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/SparseSmgLraHelper.h @@ -29,7 +29,7 @@ namespace storm { SparseSmgLraHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const statesOfCoalition); - 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 performValueIteration(Environment const& env, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const& b, std::vector& result); std::vector getChoiceValues() const; @@ -57,13 +57,6 @@ namespace storm { bool checkConvergence(ValueType threshold) const; - 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); std::vector getBVector(std::vector const& stateRewardsGetter, ValueGetter const& actionRewardsGetter); From 7e5867252d6298df9d3095d1c4cc0bf304a3af01 Mon Sep 17 00:00:00 2001 From: Fabian Russold Date: Tue, 29 Oct 2024 09:39:48 +0100 Subject: [PATCH 21/21] 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;