From 4c514cecdd143f0888c47c991e0eeeaa9d659fe9 Mon Sep 17 00:00:00 2001 From: sp Date: Tue, 5 Nov 2024 14:19:36 +0100 Subject: [PATCH] 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; + }; + } + } + } +}