From 64861445feb3673ea03359701612ff49ab884106 Mon Sep 17 00:00:00 2001 From: Lukas Posch <lukas.posch@student.tugraz.at> Date: Tue, 9 Mar 2021 12:59:47 +0100 Subject: [PATCH] bug fix bounded globally --- .../rpatl/helper/SparseSmgRpatlHelper.cpp | 17 ++++++----- .../internal/BoundedGloballyGameViHelper.cpp | 30 ++++++++++++++----- .../internal/BoundedGloballyGameViHelper.h | 4 +-- 3 files changed, 34 insertions(+), 17 deletions(-) diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 7fb39bf1d..7571a0862 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -111,14 +111,15 @@ namespace storm { auto solverEnv = env; solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false); - // Initialize the solution vector. - std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero<ValueType>()); - // Relevant states are safe states - the psiStates. storm::storage::BitVector relevantStates = psiStates; - std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); + // Initialize the solution vector. + //std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero<ValueType>()); + std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::one<ValueType>()); + //std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); + std::vector<ValueType> b = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>()); // Reduce the matrix to relevant states storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); @@ -142,10 +143,12 @@ namespace storm { STORM_LOG_DEBUG("upperBound = " << upperBound); // in case of 'G<1' or 'G<=0' the states with are initially 'safe' are filled with ones - if(upperBound == 0) + if(upperBound > 0) { - x = std::vector<ValueType>(relevantStates.size(), storm::utility::one<ValueType>()); - } else { +/* x = std::vector<ValueType>(relevantStates.size(), storm::utility::one<ValueType>()); + } else {*/ + STORM_LOG_DEBUG("b = " << b); + STORM_LOG_DEBUG("x = " << x); viHelper.performValueIteration(env, x, b, goal.direction(), upperBound); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index 177301730..f4bfbabb2 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -19,16 +19,25 @@ namespace storm { template <typename ValueType> void BoundedGloballyGameViHelper<ValueType>::prepareSolversAndMultipliersReachability(const Environment& env) { _multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix); +/* _x1IsCurrent = false; +*/ } template <typename ValueType> void BoundedGloballyGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { prepareSolversAndMultipliersReachability(env); _b = b; +/* _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>()); +*/ + _x1 = x; _x2 = _x1; +/* STORM_LOG_DEBUG("_b = " << _b); + STORM_LOG_DEBUG("_x1 = " << _x1); + STORM_LOG_DEBUG("_x2 = " << _x2);*/ + if (this->isProduceSchedulerSet()) { if (!this->_producedOptimalChoices.is_initialized()) { this->_producedOptimalChoices.emplace(); @@ -37,15 +46,20 @@ namespace storm { } for (uint64_t iter = 0; iter < upperBound; iter++) { - performIterationStep(env, dir); +/* STORM_LOG_DEBUG("After iteration " << iter << ":"); + STORM_LOG_DEBUG("_x1 = " << _x1); + STORM_LOG_DEBUG("_x2 = " << _x2);*/ /* if (storm::utility::resources::isTerminate()) { break; }*/ } +/* x = xNew(); +*/ + x = _x1; /* if (isProduceSchedulerSet()) { // We will be doing one more iteration step and track scheduler choices this time. @@ -58,18 +72,18 @@ namespace storm { if (!_multiplier) { prepareSolversAndMultipliersReachability(env); } - _x1IsCurrent = !_x1IsCurrent; +/* _x1IsCurrent = !_x1IsCurrent;*/ // multiplyandreducegaussseidel // Ax + b if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), nullptr, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, nullptr, &_statesOfCoalition); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, choices, &_statesOfCoalition); } - // compare applyPointwise +/* // compare applyPointwise storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { if(storm::solver::maximize(dir)) { if(a > b) return a; @@ -78,7 +92,7 @@ namespace storm { if(a > b) return a; else return b; } - }); + });*/ } template <typename ValueType> @@ -129,7 +143,7 @@ namespace storm { return scheduler; } - template <typename ValueType> +/* template <typename ValueType> std::vector<ValueType>& BoundedGloballyGameViHelper<ValueType>::xNew() { return _x1IsCurrent ? _x1 : _x2; } @@ -147,7 +161,7 @@ namespace storm { template <typename ValueType> std::vector<ValueType> const& BoundedGloballyGameViHelper<ValueType>::xOld() const { return _x1IsCurrent ? _x2 : _x1; - } + }*/ template class BoundedGloballyGameViHelper<double>; #ifdef STORM_HAVE_CARL diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index 413dfb56a..1553d369f 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -45,12 +45,12 @@ namespace storm { private: void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr); - std::vector<ValueType>& xNew(); +/* std::vector<ValueType>& xNew(); std::vector<ValueType> const& xNew() const; std::vector<ValueType>& xOld(); std::vector<ValueType> const& xOld() const; - bool _x1IsCurrent; + bool _x1IsCurrent;*/ /*! * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.