diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 7571a0862..c02f393d0 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -115,11 +115,8 @@ namespace storm { storm::storage::BitVector relevantStates = psiStates; // Initialize the solution vector. - //std::vector x = std::vector(transitionMatrix.getRowGroupCount() - psiStates.getNumberOfSetBits(), storm::utility::zero()); std::vector x = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::one()); - //std::vector b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, relevantStates); - std::vector b = std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()); // Reduce the matrix to relevant states storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false); @@ -134,22 +131,10 @@ namespace storm { viHelper.setProduceScheduler(true); } - // TODO: the lower bounds are not used - if(lowerBound != 0) - { - STORM_LOG_WARN("The use of lower bounds is not implemented for bounded globally formulas."); - } - - STORM_LOG_DEBUG("upperBound = " << upperBound); - - // in case of 'G<1' or 'G<=0' the states with are initially 'safe' are filled with ones + // in case of upperBound = 0 the states which are initially "safe" are filled with ones if(upperBound > 0) { -/* x = std::vector(relevantStates.size(), storm::utility::one()); - } else {*/ - STORM_LOG_DEBUG("b = " << b); - STORM_LOG_DEBUG("x = " << x); - viHelper.performValueIteration(env, x, b, goal.direction(), upperBound); + viHelper.performValueIteration(env, x, goal.direction(), upperBound); } viHelper.fillResultVector(x, relevantStates); diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp index f40387fc0..6e08f8277 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp @@ -25,9 +25,8 @@ namespace storm { } template - void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { + void BoundedGloballyGameViHelper::performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound) { prepareSolversAndMultipliers(env); - _b = b; /* _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); */ @@ -77,10 +76,10 @@ namespace storm { // multiplyandreducegaussseidel // Ax + b if (choices == nullptr) { - _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, nullptr, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, nullptr, &_statesOfCoalition); } else { // Also keep track of the choices made. - _multiplier->multiplyAndReduce(env, dir, _x1, &_b, _x1, choices, &_statesOfCoalition); + _multiplier->multiplyAndReduce(env, dir, _x1, nullptr, _x1, choices, &_statesOfCoalition); } /* // compare applyPointwise diff --git a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h index 62a709f15..512031b49 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h +++ b/src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h @@ -23,7 +23,7 @@ namespace storm { void prepareSolversAndMultipliers(const Environment& env); - void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound); + void performValueIteration(Environment const& env, std::vector& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound); /*! * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates @@ -66,7 +66,7 @@ namespace storm { storm::storage::SparseMatrix _transitionMatrix; storm::storage::BitVector _statesOfCoalition; - std::vector _x1, _x2, _b; + std::vector _x1, _x2; std::unique_ptr> _multiplier; bool _produceScheduler = false;