removed 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<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);
 
@@ -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<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);
+                    viHelper.performValueIteration(env, x, goal.direction(), upperBound);
                 }
 
                 viHelper.fillResultVector(x, relevantStates);

src/storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.cpp

@@ -25,9 +25,8 @@ namespace storm {
                 }
 
                 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) {
+                void BoundedGloballyGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound) {
                     prepareSolversAndMultipliers(env);
-                    _b = b;
 /*
                     _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
 */
@@ -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

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<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, uint64_t upperBound);
+                    void performValueIteration(Environment const& env, std::vector<ValueType>& 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<ValueType> _transitionMatrix;
                     storm::storage::BitVector _statesOfCoalition;
-                    std::vector<ValueType> _x1, _x2, _b;
+                    std::vector<ValueType> _x1, _x2;
                     std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
 
                     bool _produceScheduler = false;