changed GameViHelper::performValueIteration for computing also value iteration with upper bounds

src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

@@ -1,4 +1,5 @@
 #include <utility/graph.h>
+#include <environment/solver/GameSolverEnvironment.h>
 #include "SparseSmgRpatlHelper.h"
 
 #include "storm/environment/Environment.h"
@@ -15,7 +16,6 @@ namespace storm {
 
             template<typename ValueType>
             SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
-                // TODO add Kwiatkowska original reference
                 auto solverEnv = env;
                 solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false);
 
@@ -40,7 +40,7 @@ namespace storm {
                     if (produceScheduler) {
                         viHelper.setProduceScheduler(true);
                     }
-                    viHelper.performValueIteration(env, x, b, goal.direction());
+                    viHelper.performValueIteration(env, x, b, goal.direction(), constrainedChoiceValues);
                     if(goal.isShieldingTask()) {
                         viHelper.getChoiceValues(env, x, constrainedChoiceValues);
                     }
@@ -172,10 +172,12 @@ namespace storm {
                     }
                     // If the lowerBound = 0, value iteration is done until the upperBound.
                     if(lowerBound == 0) {
-                        viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, constrainedChoiceValues);
+                        solverEnv.solver().game().setMaximalNumberOfIterations(upperBound);
+                        viHelper.performValueIteration(solverEnv, x, b, goal.direction(), constrainedChoiceValues);
                     } else {
                         // The lowerBound != 0, the first computation between the given bound steps is done.
-                        viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound, constrainedChoiceValues);
+                        solverEnv.solver().game().setMaximalNumberOfIterations(upperBound - lowerBound);
+                        viHelper.performValueIteration(solverEnv, x, b, goal.direction(), constrainedChoiceValues);
 
                         // Initialization of subResult, fill it with the result of the first computation and 1s for the psiStates in full range.
                         std::vector<ValueType> subResult = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
@@ -199,7 +201,9 @@ namespace storm {
                         b = std::vector<ValueType>(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero<ValueType>());
 
                         // The second computation is done between step 0 and the lowerBound
-                        viHelper.performValueIterationUpperBound(env, subResult, b, goal.direction(), lowerBound, constrainedChoiceValues);
+                        solverEnv.solver().game().setMaximalNumberOfIterations(lowerBound);
+                        viHelper.performValueIteration(solverEnv, subResult, b, goal.direction(), constrainedChoiceValues);
+
                         x = subResult;
                     }
                     viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
@@ -208,7 +212,11 @@ namespace storm {
                     }
                     storm::utility::vector::setVectorValues(result, relevantStates, x);
                 }
-                // In bounded-globally formulas we not only to reach a psiState on the path but also want to stay in a set of psiStates in the given step bounds.
+                // In bounded until and bounded eventually formula the psiStates have probability 1 to satisfy the formula,
+                // because once reaching a state where psi holds those formulas are satisfied.
+                // In bounded globally formulas we cannot set those states to 1 because it is possible to leave a set of safe states after reaching a psiState
+                // and in globally the formula has to hold in every time step (between the bounds).
+                // e.g. phiState -> phiState -> psiState -> unsafeState
                 if(!computeBoundedGlobally){
                     storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
                 }

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

@@ -25,13 +25,14 @@ namespace storm {
                 }
 
                 template <typename ValueType>
-                void GameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir) {
+                void GameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues) {
                     prepareSolversAndMultipliers(env);
                     // Get precision for convergence check.
                     ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
                     uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
                     _b = b;
-                    _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                    //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                    _x1 = x;
                     _x2 = _x1;
 
                     if (this->isProduceSchedulerSet()) {
@@ -42,17 +43,25 @@ namespace storm {
                     }
 
                     uint64_t iter = 0;
-                    std::vector<ValueType> result = x;
+                    constrainedChoiceValues = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
+
                     while (iter < maxIter) {
-                        ++iter;
+                        if(iter == maxIter - 1) {
+                            _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues);
+                            auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices();
+                            rowGroupIndices.erase(rowGroupIndices.begin());
+                            _multiplier->reduce(env, dir, constrainedChoiceValues, rowGroupIndices, xNew());
+                            break;
+                        }
                         performIterationStep(env, dir);
-
                         if (checkConvergence(precision)) {
+                            _multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues);
                             break;
                         }
                         if (storm::utility::resources::isTerminate()) {
                             break;
                         }
+                        ++iter;
                     }
                     x = xNew();
 
@@ -74,18 +83,11 @@ namespace storm {
                     } else {
                         _multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition);
                     }
-
-                    // compare applyPointwise
-                    storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType {
-                       if(a > b) return a;
-                       else return b;
-                    });
                 }
 
                 template <typename ValueType>
                 bool GameViHelper<ValueType>::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<ValueType>(), "Did not expect a non-positive threshold.");
                     auto x1It = xOld().begin();
@@ -113,43 +115,6 @@ namespace storm {
                     return true;
                 }
 
-                template <typename ValueType>
-                void GameViHelper<ValueType>::performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues) {
-                    prepareSolversAndMultipliers(env);
-                    _x = x;
-                    _b = b;
-
-                    if (this->isProduceSchedulerSet()) {
-                        if (!this->_producedOptimalChoices.is_initialized()) {
-                            this->_producedOptimalChoices.emplace();
-                        }
-                        this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
-                    }
-                    for (uint64_t iter = 0; iter < upperBound; iter++) {
-                        if(iter == upperBound - 1) {
-                            _multiplier->multiply(env, _x, &_b, constrainedChoiceValues);
-                        }
-                        performIterationStepUpperBound(env, dir);
-                    }
-
-                    x = _x;
-                }
-
-                template <typename ValueType>
-                void GameViHelper<ValueType>::performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
-                    if (!_multiplier) {
-                        prepareSolversAndMultipliers(env);
-                    }
-                    // multiplyandreducegaussseidel
-                    // Ax = x'
-                    if (choices == nullptr) {
-                        _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, nullptr, &_statesOfCoalition);
-                    } else {
-                        // Also keep track of the choices made.
-                        _multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, choices, &_statesOfCoalition);
-                    }
-                }
-
                 template <typename ValueType>
                 void GameViHelper<ValueType>::setProduceScheduler(bool value) {
                     _produceScheduler = value;

src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

@@ -26,12 +26,7 @@ namespace storm {
                     /*!
                      * Perform value iteration until convergence
                      */
-                    void performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir);
-
-                    /*!
-                     * Perform value iteration until upper bound
-                     */
-                    void performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues);
+                    void performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues);
 
                     /*!
                      * Sets whether an optimal scheduler shall be constructed during the computation
@@ -68,11 +63,6 @@ namespace storm {
                      */
                     void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
 
-                    /*!
-                     * Performs one iteration step for value iteration with upper bound
-                     */
-                    void performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
-
                     /*!
                      * Checks whether the curently computed value achieves the desired precision
                      */