Merge pull request 'Cleanup SMG RPATL Model Checking' (#34) from smg_cleanup into main

Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/34

src/storm-parsers/parser/FormulaParserGrammar.cpp

@@ -386,9 +386,21 @@ namespace storm {
             }
         }
 
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
+            if (timeBounds && !timeBounds.get().empty()) {
+                std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
+                std::vector<storm::logic::TimeBoundReference> timeBoundReferences;
+                for (auto const& timeBound : timeBounds.get()) {
+                    STORM_LOG_ASSERT(!std::get<0>(timeBound), "Cannot use lower time bounds (or intervals) in globally formulas.");
+                    lowerBounds.push_back(std::get<0>(timeBound));
+                    upperBounds.push_back(std::get<1>(timeBound));
+                    timeBoundReferences.emplace_back(*std::get<2>(timeBound));
+                }
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BoundedGloballyFormula(subformula, lowerBounds, upperBounds, timeBoundReferences));
+            } else {
                 return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula));
             }
+        }
 
         std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
             return std::shared_ptr<storm::logic::Formula const>(new storm::logic::NextFormula(subformula));

src/storm/logic/FragmentSpecification.cpp

@@ -110,6 +110,9 @@ namespace storm {
             rpatl.setGloballyFormulasAllowed(true);
             rpatl.setNextFormulasAllowed(true);
             rpatl.setBoundedGloballyFormulasAllowed(true);
+            rpatl.setBoundedUntilFormulasAllowed(true);
+            rpatl.setStepBoundedUntilFormulasAllowed(true);
+            rpatl.setTimeBoundedUntilFormulasAllowed(true);
 
             return rpatl;
         }

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@@ -39,8 +39,6 @@ namespace storm {
             // Intentionally left empty.
         }
 
-
-
         template<typename SparseSmgModelType>
         bool SparseSmgRpatlModelChecker<SparseSmgModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
             storm::logic::Formula const& formula = checkTask.getFormula();
@@ -57,8 +55,6 @@ namespace storm {
             }
         }
 
-
-
         template<typename SparseSmgModelType>
         std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<SparseSmgModelType>::checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) {
             Environment solverEnv = env;
@@ -97,7 +93,6 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::checkRewardOperatorFormula(Environment const& env, CheckTask<storm::logic::RewardOperatorFormula, ValueType> const& checkTask) {
             storm::logic::RewardOperatorFormula const& formula = checkTask.getFormula();
             std::unique_ptr<CheckResult> result = this->computeRewards(env, formula.getMeasureType(), checkTask.substituteFormula(formula.getSubformula()));
-
             return result;
         }
 
@@ -105,7 +100,6 @@ namespace storm {
 		std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::checkLongRunAverageOperatorFormula(Environment const& env, CheckTask<storm::logic::LongRunAverageOperatorFormula, ValueType> const& checkTask) {
             storm::logic::LongRunAverageOperatorFormula const& formula = checkTask.getFormula();
             std::unique_ptr<CheckResult> result = this->computeLongRunAverageProbabilities(env, checkTask.substituteFormula(formula.getSubformula().asStateFormula()));
-
             return result;
         }
 
@@ -122,6 +116,8 @@ namespace storm {
                 return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula()));
             } else if (formula.isBoundedGloballyFormula()) {
                 return this->computeBoundedGloballyProbabilities(env, checkTask.substituteFormula(formula.asBoundedGloballyFormula()));
+            } else if (formula.isBoundedUntilFormula()) {
+                return this->computeBoundedUntilProbabilities(env, checkTask.substituteFormula(formula.asBoundedUntilFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
         }
@@ -187,6 +183,11 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::computeBoundedGloballyProbabilities(Environment const& env, CheckTask<storm::logic::BoundedGloballyFormula, ValueType> const& checkTask) {
             storm::logic::BoundedGloballyFormula const& pathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            // checks for bounds
+            STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound.");
+            STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete.");
+            STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula upper step bound must be discrete.");
+
             std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
             ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
 
@@ -198,6 +199,28 @@ namespace storm {
             return result;
         }
 
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<ModelType>::computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) {
+            storm::logic::BoundedUntilFormula const& pathFormula = checkTask.getFormula();
+            STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            // checks for bounds
+            STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound.");
+            STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete.");
+            STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula upper step bound must be discrete.");
+
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
+            ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
+            ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
+
+            auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>());
+            std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
+            if(checkTask.isShieldingTask()) {
+                tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition);
+            }
+            return result;
+        }
+
         template<typename SparseSmgModelType>
         std::unique_ptr<CheckResult> SparseSmgRpatlModelChecker<SparseSmgModelType>::computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NYI");
@@ -216,7 +239,6 @@ namespace storm {
             } else if (checkTask.isProduceSchedulersSet()) {
                 result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::make_unique<storm::storage::Scheduler<ValueType>>(helper.extractScheduler()));
             }
-
             return result;
         }
 

src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h

@@ -28,6 +28,7 @@ namespace storm {
 
             // The implemented methods of the AbstractModelChecker interface.
             bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
+
             std::unique_ptr<CheckResult> checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(Environment const& env, CheckTask<storm::logic::ProbabilityOperatorFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> checkRewardOperatorFormula(Environment const& env, CheckTask<storm::logic::RewardOperatorFormula, ValueType> const& checkTask) override;
@@ -40,11 +41,11 @@ namespace storm {
             std::unique_ptr<CheckResult> computeGloballyProbabilities(Environment const& env, CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> computeNextProbabilities(Environment const& env, CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> computeBoundedGloballyProbabilities(Environment const& env, CheckTask<storm::logic::BoundedGloballyFormula, ValueType> const& checkTask) override;
+            std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
 
             std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
             std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
 
-            //void coalitionIndicator(Environment& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask);
         private:
             storm::storage::BitVector statesOfCoalition;
         };

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

@@ -1,3 +1,4 @@
+#include <utility/graph.h>
 #include "SparseSmgRpatlHelper.h"
 
 #include "storm/environment/Environment.h"
@@ -5,9 +6,8 @@
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 #include "storm/utility/vector.h"
-
+#include "storm/utility/graph.h"
 #include "storm/modelchecker/rpatl/helper/internal/GameViHelper.h"
-#include "storm/modelchecker/rpatl/helper/internal/BoundedGloballyGameViHelper.h"
 
 namespace storm {
     namespace modelchecker {
@@ -19,38 +19,43 @@ 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 those states which are phiStates and not PsiStates.
                 storm::storage::BitVector relevantStates = phiStates & ~psiStates;
 
+                // Initialize the x vector and solution vector result.
+                std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
+                std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
                 std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
                 std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
-
-                // Reduce the matrix to relevant states
-                storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
+                std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
 
                 storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits());
                 clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition);
-                clippedStatesOfCoalition.complement();
 
+                if(!relevantStates.empty()) {
+                    // Reduce the matrix to relevant states.
+                    storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
+                    // Create GameViHelper for computations.
                     storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
-                std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
                     if (produceScheduler) {
                         viHelper.setProduceScheduler(true);
                     }
-
                     viHelper.performValueIteration(env, x, b, goal.direction());
                     if(goal.isShieldingTask()) {
                         viHelper.getChoiceValues(env, x, constrainedChoiceValues);
                     }
-                viHelper.fillResultVector(x, relevantStates, psiStates);
+
+                    // Fill up the constrainedChoice Values to full size.
                     viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
 
                     if (produceScheduler) {
                         scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates));
                     }
-                return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
+                }
+                // Fill up the result vector with the values of x for the relevant states, with 1s for psi states (0 is default)
+                storm::utility::vector::setVectorValues(result, relevantStates, x);
+                storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
+                return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
             }
 
             template<typename ValueType>
@@ -75,11 +80,11 @@ namespace storm {
 
             template<typename ValueType>
             SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
-                // the idea is to implement the definition of globally as in the formula:
                 // G psi = not(F(not psi)) = not(true U (not psi))
-                // so the psiStates are flipped, then the true U part is calculated, at the end the result is flipped again
+                // The psiStates are flipped, then the true U part is calculated, at the end the result is flipped again.
                 storm::storage::BitVector notPsiStates = ~psiStates;
                 statesOfCoalition.complement();
+
                 auto result = computeUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint);
                 for (auto& element : result.values) {
                     element = storm::utility::one<ValueType>() - element;
@@ -92,71 +97,119 @@ namespace storm {
 
             template<typename ValueType>
             SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeNextProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
-                // create vector x for result, bitvector allStates with a true for each state and a vector b for the probability to get to state psi
-                std::vector<ValueType> x = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                // Create vector result, bitvector allStates with a true for each state and a vector b for the probability for each state to get to a psi state, choiceValues is to store choices for shielding.
+                std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
                 storm::storage::BitVector allStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true);
                 std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(allStates, psiStates);
-
+                std::vector<ValueType> choiceValues = std::vector<ValueType>(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
                 statesOfCoalition.complement();
 
                 if (produceScheduler) {
                     STORM_LOG_WARN("Next formula does not expect that produceScheduler is set to true.");
                 }
-
-                // create multiplier and execute the calculation for 1 step
+                // Create a multiplier for reduction.
                 auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
-                std::vector<ValueType> choiceValues = std::vector<ValueType>(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
+                multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), result, &statesOfCoalition);
                 if (goal.isShieldingTask()) {
-                    multiplier->multiply(env, x, &b, choiceValues);
-                    multiplier->reduce(env, goal.direction(), choiceValues, transitionMatrix.getRowGroupIndices(), x, &statesOfCoalition);
-                } else {
-                    multiplier->multiplyAndReduce(env, goal.direction(), x, &b, x, nullptr, &statesOfCoalition);
+                    choiceValues = b;
                 }
-                return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(allStates), nullptr, std::move(choiceValues));
+                return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(allStates), nullptr, std::move(choiceValues));
             }
 
             template<typename ValueType>
             SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint,uint64_t lowerBound, uint64_t upperBound) {
+                // G psi = not(F(not psi)) = not(true U (not psi))
+                // The psiStates are flipped, then the true U part is calculated, at the end the result is flipped again.
+                storm::storage::BitVector notPsiStates = ~psiStates;
+                statesOfCoalition.complement();
+
+                auto result = computeBoundedUntilProbabilities(env, std::move(goal), transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), notPsiStates, qualitative, statesOfCoalition, produceScheduler, hint, lowerBound, upperBound, true);
+                for (auto& element : result.values) {
+                    element = storm::utility::one<ValueType>() - element;
+                }
+                for (auto& element : result.choiceValues) {
+                    element = storm::utility::one<ValueType>() - element;
+                }
+                return result;
+            }
+
+            template<typename ValueType>
+            SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeBoundedUntilProbabilities(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,uint64_t lowerBound, uint64_t upperBound, bool computeBoundedGlobally) {
                 auto solverEnv = env;
                 solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false);
 
-                // Relevant states are safe states - the psiStates.
-                storm::storage::BitVector relevantStates = psiStates;
-
-                // Initialize the solution vector.
-                std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::one<ValueType>());
+                // boundedUntil formulas look like:
+                // phi U [lowerBound, upperBound] psi
+                // --
+                // We solve this by look at psiStates, finding phiStates which have paths to psiStates in the given step bounds,
+                // then we find all states which have a path to those phiStates in the given lower bound
+                // (which states the paths pass before the lower bound does not matter).
 
-                // Reduce the matrix to relevant states
-                storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
+                // First initialization of relevantStates between the step bounds.
+                storm::storage::BitVector relevantStates = phiStates & ~psiStates;
 
-                std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(submatrix.getRowCount(), storm::utility::zero<ValueType>());
+                // Initializations.
+                std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
+                std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
+                std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates).size(), storm::utility::zero<ValueType>());
+                std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
 
                 storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits());
                 clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition);
-                clippedStatesOfCoalition.complement();
 
-                // Use the bounded globally game vi helper
-                storm::modelchecker::helper::internal::BoundedGloballyGameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
-                std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
+                // If there are no relevantStates or the upperBound is 0, no computation is needed.
+                if(!relevantStates.empty() && upperBound > 0) {
+                    // Reduce the matrix to relevant states. - relevant states are all states.
+                    storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
+                    // Create GameViHelper for computations.
+                    storm::modelchecker::helper::internal::GameViHelper<ValueType> viHelper(submatrix, clippedStatesOfCoalition);
                     if (produceScheduler) {
                         viHelper.setProduceScheduler(true);
                     }
+                    // If the lowerBound = 0, value iteration is done until the upperBound.
+                    if(lowerBound == 0) {
+                        viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, 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);
 
-                // in case of upperBound = 0 the states which are initially "safe" are filled with ones
-                if(upperBound > 0)
-                {
-                    viHelper.performValueIteration(env, x, goal.direction(), upperBound, constrainedChoiceValues);
-                }
-                viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
+                        // 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>());
+                        storm::utility::vector::setVectorValues(subResult, relevantStates, x);
+                        storm::utility::vector::setVectorValues(subResult, psiStates, storm::utility::one<ValueType>());
 
-                viHelper.fillResultVector(x, relevantStates);
-                viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
+                        // The newPsiStates are those states which can reach the psiStates in the steps between the bounds - the !=0 values in subResult.
+                        storm::storage::BitVector newPsiStates(subResult.size(), false);
+                        storm::utility::vector::setNonzeroIndices(subResult, newPsiStates);
+
+                        // The relevantStates for the second part of the computation are all states.
+                        relevantStates = storm::storage::BitVector(phiStates.size(), true);
+                        submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
+
+                        // Update the viHelper for the (full-size) submatrix and statesOfCoalition.
+                        viHelper.updateTransitionMatrix(submatrix);
+                        viHelper.updateStatesOfCoaltion(statesOfCoalition);
 
+                        // Reset constrainedChoiceValues and b to 0-vector in the correct dimension.
+                        constrainedChoiceValues = std::vector<ValueType>(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero<ValueType>());
+                        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);
+                        x = subResult;
+                    }
+                    viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
                     if (produceScheduler) {
                         scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), relevantStates, ~relevantStates));
                     }
-
-                return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(x), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
+                    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.
+                if(!computeBoundedGlobally){
+                    storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
+                }
+                return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
             }
 
             template class SparseSmgRpatlHelper<double>;

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

@@ -38,10 +38,10 @@ namespace storm {
                 static SMGSparseModelCheckingHelperReturnType<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
                 static SMGSparseModelCheckingHelperReturnType<ValueType> computeNextProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint);
                 static SMGSparseModelCheckingHelperReturnType<ValueType> computeBoundedGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint, uint64_t lowerBound, uint64_t upperBound);
+                static SMGSparseModelCheckingHelperReturnType<ValueType> computeBoundedUntilProbabilities(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, uint64_t lowerBound, uint64_t upperBound, bool computeBoundedGlobally = false);
             private:
                 static storm::storage::Scheduler<ValueType> expandScheduler(storm::storage::Scheduler<ValueType> scheduler, storm::storage::BitVector psiStates, storm::storage::BitVector notPhiStates);
                 static void expandChoiceValues(std::vector<uint_fast64_t> const& rowGroupIndices, storm::storage::BitVector const& relevantStates, std::vector<ValueType> const& constrainedChoiceValues, std::vector<ValueType>& choiceValues);
-
             };
         }
     }

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

@@ -1,132 +0,0 @@
-#include "BoundedGloballyGameViHelper.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 <typename ValueType>
-                BoundedGloballyGameViHelper<ValueType>::BoundedGloballyGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
-                }
-
-                template <typename ValueType>
-                void BoundedGloballyGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
-                    _multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
-                }
-
-                template <typename ValueType>
-                void BoundedGloballyGameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues) {
-                    prepareSolversAndMultipliers(env);
-                    _x = x;
-
-                    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, nullptr, constrainedChoiceValues);
-                        }
-                        performIterationStep(env, dir);
-                    }
-
-                    x = _x;
-                }
-
-                template <typename ValueType>
-                void BoundedGloballyGameViHelper<ValueType>::performIterationStep(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, nullptr, _x, nullptr, &_statesOfCoalition);
-                    } else {
-                        // Also keep track of the choices made.
-                        _multiplier->multiplyAndReduce(env, dir, _x, nullptr, _x, choices, &_statesOfCoalition);
-                    }
-                }
-
-                template <typename ValueType>
-                void BoundedGloballyGameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector psiStates)
-                {
-                    std::vector<ValueType> filledVector = std::vector<ValueType>(psiStates.size(), storm::utility::zero<ValueType>());
-                    uint bitIndex = 0;
-                    for(uint i = 0; i < filledVector.size(); i++) {
-                        if (psiStates.get(i)) {
-                            filledVector.at(i) = result.at(bitIndex);
-                            bitIndex++;
-                        }
-                    }
-                    result = filledVector;
-                }
-
-                template <typename ValueType>
-                void BoundedGloballyGameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) {
-                    std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>());
-                    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 <typename ValueType>
-                void BoundedGloballyGameViHelper<ValueType>::setProduceScheduler(bool value) {
-                    _produceScheduler = value;
-                }
-
-                template <typename ValueType>
-                bool BoundedGloballyGameViHelper<ValueType>::isProduceSchedulerSet() const {
-                    return _produceScheduler;
-                }
-
-                template <typename ValueType>
-                std::vector<uint64_t> const& BoundedGloballyGameViHelper<ValueType>::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 <typename ValueType>
-                std::vector<uint64_t>& BoundedGloballyGameViHelper<ValueType>::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 <typename ValueType>
-                storm::storage::Scheduler<ValueType> BoundedGloballyGameViHelper<ValueType>::extractScheduler() const{
-                    auto const& optimalChoices = getProducedOptimalChoices();
-                    storm::storage::Scheduler<ValueType> scheduler(optimalChoices.size());
-                    for (uint64_t state = 0; state < optimalChoices.size(); ++state) {
-                        scheduler.setChoice(optimalChoices[state], state);
-                    }
-                    return scheduler;
-                }
-
-                template class BoundedGloballyGameViHelper<double>;
-#ifdef STORM_HAVE_CARL
-                template class BoundedGloballyGameViHelper<storm::RationalNumber>;
-#endif
-            }
-        }
-    }
-}

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

@@ -1,76 +0,0 @@
-#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 <typename VT> class Scheduler;
-    }
-
-    namespace modelchecker {
-        namespace helper {
-            namespace internal {
-
-                template <typename ValueType>
-                class BoundedGloballyGameViHelper {
-                public:
-                    BoundedGloballyGameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition);
-
-                    void prepareSolversAndMultipliers(const Environment& env);
-
-                    void performValueIteration(Environment const& env, std::vector<ValueType>& x, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues);
-
-                    /*!
-                     * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates
-                     */
-                    void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector psiStates);
-
-                    /*!
-                     * Fills the choice values vector to the original size with zeros for ~psiState choices.
-                     */
-                    void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
-
-                    /*!
-                     * 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;
-
-                    storm::storage::Scheduler<ValueType> extractScheduler() const;
-
-                private:
-                    void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
-
-                    /*!
-                     * @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<uint64_t> 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<uint64_t>& getProducedOptimalChoices();
-
-                    storm::storage::SparseMatrix<ValueType> _transitionMatrix;
-                    storm::storage::BitVector _statesOfCoalition;
-                    std::vector<ValueType> _x;
-                    std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
-
-                    bool _produceScheduler = false;
-                    boost::optional<std::vector<uint64_t>> _producedOptimalChoices;
-                };
-            }
-        }
-    }
-}

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

@@ -15,22 +15,22 @@ namespace storm {
 
                 template <typename ValueType>
                 GameViHelper<ValueType>::GameViHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector statesOfCoalition) : _transitionMatrix(transitionMatrix), _statesOfCoalition(statesOfCoalition) {
+                    // Intentionally left empty.
                 }
 
                 template <typename ValueType>
                 void GameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
                     _multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
-
                     _x1IsCurrent = false;
                 }
 
                 template <typename ValueType>
                 void GameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir) {
                     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>());
                     _x2 = _x1;
 
@@ -114,34 +114,40 @@ namespace storm {
                 }
 
                 template <typename ValueType>
-                void GameViHelper<ValueType>::fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates) {
-                    std::vector<ValueType> filledVector = std::vector<ValueType>(relevantStates.size(), storm::utility::zero<ValueType>());
-                    uint bitIndex = 0;
-                    for(uint i = 0; i < filledVector.size(); i++) {
-                        if (relevantStates.get(i)) {
-                            filledVector.at(i) = result.at(bitIndex);
-                            bitIndex++;
+                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();
                         }
-                        else if (psiStates.get(i)) {
-                            filledVector.at(i) = 1;
+                        this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
                     }
+                    for (uint64_t iter = 0; iter < upperBound; iter++) {
+                        if(iter == upperBound - 1) {
+                            _multiplier->multiply(env, _x, &_b, constrainedChoiceValues);
                         }
-                    result = filledVector;
+                        performIterationStepUpperBound(env, dir);
                     }
 
-                template <typename ValueType>
-                void GameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) {
-                    std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>());
-                    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;
+                    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);
                     }
-                    choiceValues = allChoices;
                 }
 
                 template <typename ValueType>
@@ -154,6 +160,16 @@ namespace storm {
                     return _produceScheduler;
                 }
 
+                template <typename ValueType>
+                void GameViHelper<ValueType>::updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix) {
+                    _transitionMatrix = newTransitionMatrix;
+                }
+
+                template <typename ValueType>
+                void GameViHelper<ValueType>::updateStatesOfCoaltion(storm::storage::BitVector newStatesOfCoaltion) {
+                    _statesOfCoalition = newStatesOfCoaltion;
+                }
+
                 template <typename ValueType>
                 std::vector<uint64_t> const& GameViHelper<ValueType>::getProducedOptimalChoices() const {
                     STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested.");
@@ -183,6 +199,21 @@ namespace storm {
                     _multiplier->multiply(env, x, &_b, choiceValues);
                 }
 
+                template <typename ValueType>
+                void GameViHelper<ValueType>::fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices) {
+                    std::vector<ValueType> allChoices = std::vector<ValueType>(rowGroupIndices.at(rowGroupIndices.size() - 1), storm::utility::zero<ValueType>());
+                    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 <typename ValueType>
                 std::vector<ValueType>& GameViHelper<ValueType>::xNew() {
                     return _x1IsCurrent ? _x1 : _x2;

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

@@ -23,17 +23,15 @@ 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);
-
                     /*!
-                     * Fills the result vector to the original size with ones for being psiStates, zeros for being not phiStates
+                     * Perform value iteration until convergence
                      */
-                    void fillResultVector(std::vector<ValueType>& result, storm::storage::BitVector relevantStates, storm::storage::BitVector psiStates);
+                    void performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir);
 
                     /*!
-                     * Fills the choice values vector to the original size with zeros for ~psiState choices.
+                     * Perform value iteration until upper bound
                      */
-                    void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
+                    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);
 
                     /*!
                      * Sets whether an optimal scheduler shall be constructed during the computation
@@ -45,12 +43,36 @@ namespace storm {
                      */
                     bool isProduceSchedulerSet() const;
 
+                    /*!
+                     * Changes the transitionMatrix to the given one.
+                     */
+                    void updateTransitionMatrix(storm::storage::SparseMatrix<ValueType> newTransitionMatrix);
+
+                    /*!
+                     * Changes the statesOfCoalition to the given one.
+                     */
+                    void updateStatesOfCoaltion(storm::storage::BitVector newStatesOfCoaltion);
+
                     storm::storage::Scheduler<ValueType> extractScheduler() const;
 
                     void getChoiceValues(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType>& choiceValues);
+
+                    /*!
+                     * Fills the choice values vector to the original size with zeros for ~psiState choices.
+                     */
+                    void fillChoiceValuesVector(std::vector<ValueType>& choiceValues, storm::storage::BitVector psiStates, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices);
+
                 private:
+                    /*!
+                     * Performs one iteration step for value iteration
+                     */
                     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
                      */
@@ -77,7 +99,7 @@ namespace storm {
 
                     storm::storage::SparseMatrix<ValueType> _transitionMatrix;
                     storm::storage::BitVector _statesOfCoalition;
-                    std::vector<ValueType> _x1, _x2, _b;
+                    std::vector<ValueType> _x, _x1, _x2, _b;
                     std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
 
                     bool _produceScheduler = false;