started on computing upper bounds for rewards for interval value iteration

src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@@ -6,6 +6,8 @@
 #include "storm/utility/vector.h"
 #include "storm/utility/graph.h"
 
+#include "storm/storage/StronglyConnectedComponentDecomposition.h"
+
 #include "storm/solver/LinearEquationSolver.h"
 
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
@@ -14,6 +16,7 @@
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/IllegalArgumentException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
 
 namespace storm {
     namespace modelchecker {
@@ -211,6 +214,130 @@ namespace storm {
                                                   targetStates, qualitative, linearEquationSolverFactory, hint);
             }
             
+            template<typename ValueType>
+            class DsMpi {
+            public:
+                DsMpi(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& rewards, std::vector<ValueType> const& oneStepTargetProbabilities) : transitionMatrix(transitionMatrix), originalRewards(rewards), backwardTransitions(transitionMatrix.transpose()), p(transitionMatrix.getRowCount()), w(transitionMatrix.getRowCount()), rewards(rewards), targetProbabilities(oneStepTargetProbabilities) {
+                    // Intentionally left empty.
+                }
+                
+                std::vector<ValueType> computeUpperBounds() {
+                    sweep();
+                    ValueType lambda = computeLambda();
+                    
+                    // Finally compute the upper bounds for the states.
+                    std::vector<ValueType> result(transitionMatrix.getRowCount());
+                    auto one = storm::utility::one<ValueType>();
+                    for (storm::storage::sparse::state_type state = 0; state < result.size(); ++state) {
+                        result[state] = w[state] + (one - p[state]) * lambda;
+                    }
+                    return result;
+                }
+                
+            private:
+                ValueType computeLambda() {
+                    ValueType lambda = storm::utility::convertNumber<ValueType>(0.0);
+                    for (storm::storage::sparse::state_type state = 0; state < targetProbabilities.size(); ++state) {
+                        // Check whether condition (I) or (II) applies.
+                        ValueType sum = storm::utility::zero<ValueType>();
+                        for (auto const& e : transitionMatrix.getRow(state)) {
+                            sum += e.getValue() * p[e.getColumn()];
+                        }
+                        if (p[state] < sum) {
+                            // Condition (I) applies.
+                            ValueType localLambda = sum - p[state];
+                            ValueType nominator = originalRewards[state];
+                            for (auto const& e : transitionMatrix.getRow(state)) {
+                                nominator += e.getValue() * w[e.getColumn()];
+                            }
+                            nominator -= w[state];
+                            localLambda = nominator / localLambda;
+                            lambda = std::max(lambda, localLambda);
+                        } else {
+                            // Here, condition (II) automatically applies and as the resulting local lambda is 0, we
+                            // don't need to consider it.
+                        }
+                    }
+                    return lambda;
+                }
+                
+                void sweep() {
+                    // Create a priority queue that allows for easy retrieval of the currently best state.
+                    auto cmp = [this](storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) {
+                        ValueType pa = p[a];
+                        ValueType pb = p[b];
+                        if (pa > pb) {
+                            return true;
+                        } else if (pa == pb) {
+                            return w[a] < w[b];
+                        }
+                        return false;
+                    };
+                    std::set<storm::storage::sparse::state_type, decltype(cmp)> queue;
+
+                    
+                    storm::storage::BitVector visited(p.size());
+
+                    for (storm::storage::sparse::state_type state = 0; state < targetProbabilities.size(); ++state) {
+                        if (!storm::utility::isZero(targetProbabilities[state])) {
+                            queue.insert(state);
+                        }
+                    }
+                    
+                    while (!queue.empty()) {
+                        // Get first entry in queue.
+                        storm::storage::sparse::state_type currentState = *queue.begin();
+                        queue.erase(queue.begin());
+                        
+                        // Mark state as visited.
+                        visited.set(currentState);
+                        
+                        // Set weight and probability for the state.
+                        w[currentState] = rewards[currentState];
+                        p[currentState] = targetProbabilities[currentState];
+                        
+                        for (auto const& e : backwardTransitions.getRow(currentState)) {
+                            if (visited.get(e.getColumn())) {
+                                continue;
+                            }
+                            
+                            // Delete element from the priority queue if it was in there.
+                            auto it = queue.find(e.getColumn());
+                            if (it != queue.end()) {
+                                queue.erase(it);
+                            }
+                            
+                            // Update reward/probability values.
+                            rewards[e.getColumn()] += e.getValue() * w[currentState];
+                            targetProbabilities[e.getColumn()] += e.getValue() * p[currentState];
+
+                            // (Re-)insert the state with the new rewards/target probabilities.
+                            queue.insert(e.getColumn());
+                        }
+                    }
+                }
+                
+                // References to input data.
+                storm::storage::SparseMatrix<ValueType> const& transitionMatrix;
+                std::vector<ValueType> const& originalRewards;
+                
+                // Derived from input data.
+                storm::storage::SparseMatrix<ValueType> backwardTransitions;
+                
+                // Data that the algorithm uses internally.
+                std::vector<ValueType> p;
+                std::vector<ValueType> w;
+                std::vector<ValueType> rewards;
+                std::vector<ValueType> targetProbabilities;
+            };
+            
+            // This function computes an upper bound on the reachability rewards (see Baier et al, CAV'17).
+            template<typename ValueType>
+            std::vector<ValueType> computeUpperRewardBounds(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& rewards, std::vector<ValueType> const& oneStepTargetProbabilities) {
+                DsMpi<ValueType> dsmpi(transitionMatrix, rewards, oneStepTargetProbabilities);
+                return dsmpi.computeUpperBounds();
+            }
+            
             template<typename ValueType, typename RewardModelType>
             std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, ModelCheckerHint const& hint) {
                 
@@ -264,10 +391,24 @@ namespace storm {
                         
                         // Prepare the right-hand side of the equation system.
                         std::vector<ValueType> b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates);
+
+                        storm::solver::LinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements();
+                        boost::optional<std::vector<ValueType>> upperRewardBounds;
+                        requirements.clearLowerBounds();
+                        if (requirements.requiresUpperBounds()) {
+                            upperRewardBounds = computeUpperRewardBounds(submatrix, b, transitionMatrix.getConstrainedRowSumVector(maybeStates, targetStates));
+                            requirements.clearUpperBounds();
+                        }
+                        STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver.");
                         
-                        // Now solve the resulting equation system.
+                        // Create the solvers and provide
                         std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(submatrix));
                         solver->setLowerBound(storm::utility::zero<ValueType>());
+                        if (upperRewardBounds) {
+                            solver->setUpperBounds(std::move(upperRewardBounds.get()));
+                        }
+                        
+                        // Now solve the resulting equation system.
                         solver->solveEquations(x, b);
                         
                         // Set values of resulting vector according to result.

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -210,7 +210,9 @@ namespace storm {
                         requirements.clearValidInitialScheduler();
                     }
                     if (type == storm::solver::EquationSystemType::UntilProbabilities) {
-                        requirements.clearGlobalUpperBound();
+                        requirements.clearBounds();
+                    } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) {
+                        requirements.clearLowerBounds();
                     }
                     STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver.");
                 }

src/storm/solver/EigenLinearEquationSolver.cpp

@@ -276,7 +276,7 @@ namespace storm {
                     }
                 }
                 
-                // Make sure that all results conform to the bounds.
+                // Make sure that all results conform to the (global) bounds.
                 storm::utility::vector::clip(x, this->lowerBound, this->upperBound);
                 
                 // Check if the solver converged and issue a warning otherwise.

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -256,7 +256,7 @@ namespace storm {
                 if (!direction || direction.get() == OptimizationDirection::Maximize) {
                     requirements.requireNoEndComponents();
                 }
-                requirements.requireGlobalUpperBound();
+                requirements.requireUpperBounds();
             }
             
             // Then add our requirements on top of that.
@@ -273,7 +273,7 @@ namespace storm {
             }
             
             if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && this->getSettings().getForceSoundness()) {
-                requirements.requireGlobalUpperBound();
+                requirements.requireUpperBounds();
             }
             
             return requirements;

src/storm/solver/LinearEquationSolver.cpp

@@ -131,11 +131,35 @@ namespace storm {
             cachedRowVector.reset();
         }
         
+        template<typename ValueType>
+        bool LinearEquationSolver<ValueType>::hasLowerBound(BoundType const& type) const {
+            if (type == BoundType::Any) {
+                return static_cast<bool>(lowerBound) || static_cast<bool>(lowerBounds);
+            } else if (type == BoundType::Global) {
+                return static_cast<bool>(lowerBound);
+            } else if (type == BoundType::Local) {
+                return static_cast<bool>(lowerBounds);
+            }
+            return false;
+        }
+        
+        template<typename ValueType>
+        bool LinearEquationSolver<ValueType>::hasUpperBound(BoundType const& type) const {
+            if (type == BoundType::Any) {
+                return static_cast<bool>(upperBound) || static_cast<bool>(upperBounds);
+            } else if (type == BoundType::Global) {
+                return static_cast<bool>(upperBound);
+            } else if (type == BoundType::Local) {
+                return static_cast<bool>(upperBounds);
+            }
+            return false;
+        }
+        
         template<typename ValueType>
         void LinearEquationSolver<ValueType>::setLowerBound(ValueType const& value) {
             lowerBound = value;
         }
-
+        
         template<typename ValueType>
         void LinearEquationSolver<ValueType>::setUpperBound(ValueType const& value) {
             upperBound = value;
@@ -148,23 +172,67 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool LinearEquationSolver<ValueType>::hasLowerBound() const {
-            return static_cast<bool>(lowerBound);
+        ValueType const& LinearEquationSolver<ValueType>::getLowerBound() const {
+            return lowerBound.get();
         }
         
         template<typename ValueType>
-        bool LinearEquationSolver<ValueType>::hasUpperBound() const {
-            return static_cast<bool>(upperBound);
+        ValueType const& LinearEquationSolver<ValueType>::getUpperBound() const {
+            return upperBound.get();
         }
         
         template<typename ValueType>
-        ValueType const& LinearEquationSolver<ValueType>::getLowerBound() const {
-            return lowerBound.get();
+        std::vector<ValueType> const& LinearEquationSolver<ValueType>::getLowerBounds() const {
+            return lowerBounds.get();
         }
         
         template<typename ValueType>
-        ValueType const& LinearEquationSolver<ValueType>::getUpperBound() const {
-            return upperBound.get();
+        std::vector<ValueType> const& LinearEquationSolver<ValueType>::getUpperBounds() const {
+            return upperBounds.get();
+        }
+        
+        template<typename ValueType>
+        void LinearEquationSolver<ValueType>::setLowerBounds(std::vector<ValueType> const& values) {
+            lowerBounds = values;
+        }
+        
+        template<typename ValueType>
+        void LinearEquationSolver<ValueType>::setUpperBounds(std::vector<ValueType> const& values) {
+            upperBounds = values;
+        }
+
+        template<typename ValueType>
+        void LinearEquationSolver<ValueType>::setUpperBounds(std::vector<ValueType>&& values) {
+            upperBounds = std::move(values);
+        }
+
+        template<typename ValueType>
+        void LinearEquationSolver<ValueType>::setBounds(std::vector<ValueType> const& lower, std::vector<ValueType> const& upper) {
+            setLowerBounds(lower);
+            setUpperBounds(upper);
+        }
+        
+        template<typename ValueType>
+        void LinearEquationSolver<ValueType>::createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector) const {
+            if (!upperBoundsVector) {
+                if (this->hasUpperBound(BoundType::Local)) {
+                    upperBoundsVector = std::make_unique<std::vector<ValueType>>(this->getUpperBounds());
+                } else {
+                    upperBoundsVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount(), this->getUpperBound());
+                }
+            } else {
+                if (this->hasUpperBound(BoundType::Local)) {
+                    for (auto& e : *upperBoundsVector) {
+                        e = this->getUpperBound();
+                    }
+                } else {
+                    auto upperBoundsIt = this->getUpperBounds().begin();
+                    for (auto& e : *upperBoundsVector) {
+                        e = *upperBoundsIt;
+                        ++upperBoundsIt;
+                    }
+                }
+            }
         }
         
         template<typename ValueType>

src/storm/solver/LinearEquationSolver.h

@@ -150,6 +150,22 @@ namespace storm {
              */
             virtual void clearCache() const;
             
+            enum class BoundType {
+                Global,
+                Local,
+                Any
+            };
+            
+            /*!
+             * Retrieves whether this solver has a lower bound.
+             */
+            bool hasLowerBound(BoundType const& type = BoundType::Any) const;
+            
+            /*!
+             * Retrieves whether this solver has an upper bound.
+             */
+            bool hasUpperBound(BoundType const& type = BoundType::Any) const;
+            
             /*!
              * Sets a lower bound for the solution that can potentially be used by the solver.
              */
@@ -160,34 +176,56 @@ namespace storm {
              */
             void setUpperBound(ValueType const& value);
 
+            /*!
+             * Sets bounds for the solution that can potentially be used by the solver.
+             */
+            void setBounds(ValueType const& lower, ValueType const& upper);
+            
             /*!
              * Retrieves the lower bound (if there is any).
              */
             ValueType const& getLowerBound() const;
             
             /*!
-             * Retrieves the lower bound (if there is any).
+             * Retrieves the upper bound (if there is any).
              */
             ValueType const& getUpperBound() const;
             
             /*!
-             * Retrieves whether this solver has a lower bound.
+             * Retrieves a vector containing the lower bounds (if there are any).
              */
-            bool hasLowerBound() const;
+            std::vector<ValueType> const& getLowerBounds() const;
+            
+            /*!
+             * Retrieves a vector containing the upper bounds (if there are any).
+             */
+            std::vector<ValueType> const& getUpperBounds() const;
+            
+            /*!
+             * Sets lower bounds for the solution that can potentially be used by the solver.
+             */
+            void setLowerBounds(std::vector<ValueType> const& values);
+            
+            /*!
+             * Sets upper bounds for the solution that can potentially be used by the solver.
+             */
+            void setUpperBounds(std::vector<ValueType> const& values);
 
             /*!
-             * Retrieves whether this solver has an upper bound.
+             * Sets upper bounds for the solution that can potentially be used by the solver.
              */
-            bool hasUpperBound() const;
+            void setUpperBounds(std::vector<ValueType>&& values);
 
             /*!
              * Sets bounds for the solution that can potentially be used by the solver.
              */
-            void setBounds(ValueType const& lower, ValueType const& upper);
-
+            void setBounds(std::vector<ValueType> const& lower, std::vector<ValueType> const& upper);
+            
         protected:
             virtual bool internalSolveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const = 0;
             
+            void createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector) const;
+            
             // auxiliary storage. If set, this vector has getMatrixRowCount() entries.
             mutable std::unique_ptr<std::vector<ValueType>> cachedRowVector;
             
@@ -196,6 +234,12 @@ namespace storm {
 
             // An upper bound if one was set.
             boost::optional<ValueType> upperBound;
+            
+            // Lower bounds if they were set.
+            boost::optional<std::vector<ValueType>> lowerBounds;
+
+            // Lower bounds if they were set.
+            boost::optional<std::vector<ValueType>> upperBounds;
 
         private:
             /*!

src/storm/solver/LinearEquationSolverRequirements.cpp

@@ -3,45 +3,45 @@
 namespace storm {
     namespace solver {
         
-        LinearEquationSolverRequirements::LinearEquationSolverRequirements() : globalLowerBound(false), globalUpperBound(false) {
+        LinearEquationSolverRequirements::LinearEquationSolverRequirements() : lowerBounds(false), upperBounds(false) {
             // Intentionally left empty.
         }
         
-        LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireGlobalLowerBound() {
-            globalLowerBound = true;
+        LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireLowerBounds() {
+            lowerBounds = true;
             return *this;
         }
         
-        LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireGlobalUpperBound() {
-            globalUpperBound = true;
+        LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireUpperBounds() {
+            upperBounds = true;
             return *this;
         }
         
-        bool LinearEquationSolverRequirements::requiresGlobalLowerBound() const {
-            return globalLowerBound;
+        bool LinearEquationSolverRequirements::requiresLowerBounds() const {
+            return lowerBounds;
         }
         
-        bool LinearEquationSolverRequirements::requiresGlobalUpperBound() const {
-            return globalUpperBound;
+        bool LinearEquationSolverRequirements::requiresUpperBounds() const {
+            return upperBounds;
         }
         
         bool LinearEquationSolverRequirements::requires(Element const& element) const {
             switch (element) {
-                case Element::GlobalLowerBound: return globalLowerBound; break;
-                case Element::GlobalUpperBound: return globalUpperBound; break;
+                case Element::LowerBounds: return lowerBounds; break;
+                case Element::UpperBounds: return upperBounds; break;
             }
         }
         
-        void LinearEquationSolverRequirements::clearGlobalLowerBound() {
-            globalLowerBound = false;
+        void LinearEquationSolverRequirements::clearLowerBounds() {
+            lowerBounds = false;
         }
         
-        void LinearEquationSolverRequirements::clearGlobalUpperBound() {
-            globalUpperBound = false;
+        void LinearEquationSolverRequirements::clearUpperBounds() {
+            upperBounds = false;
         }
         
         bool LinearEquationSolverRequirements::empty() const {
-            return !globalLowerBound && !globalUpperBound;
+            return !lowerBounds && !upperBounds;
         }
         
     }

src/storm/solver/LinearEquationSolverRequirements.h

@@ -8,27 +8,27 @@ namespace storm {
             // The different requirements a solver can have.
             enum class Element {
                 // Requirements that are related to bounds for the actual solution.
-                GlobalLowerBound,
-                GlobalUpperBound
+                LowerBounds,
+                UpperBounds
             };
             
             LinearEquationSolverRequirements();
             
-            LinearEquationSolverRequirements& requireGlobalLowerBound();
-            LinearEquationSolverRequirements& requireGlobalUpperBound();
+            LinearEquationSolverRequirements& requireLowerBounds();
+            LinearEquationSolverRequirements& requireUpperBounds();
             
-            bool requiresGlobalLowerBound() const;
-            bool requiresGlobalUpperBound() const;
+            bool requiresLowerBounds() const;
+            bool requiresUpperBounds() const;
             bool requires(Element const& element) const;
             
-            void clearGlobalLowerBound();
-            void clearGlobalUpperBound();
+            void clearLowerBounds();
+            void clearUpperBounds();
             
             bool empty() const;
             
         private:
-            bool globalLowerBound;
-            bool globalUpperBound;
+            bool lowerBounds;
+            bool upperBounds;
         };
         
     }

src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp

@@ -3,7 +3,7 @@
 namespace storm {
     namespace solver {
         
-        MinMaxLinearEquationSolverRequirements::MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements) : noEndComponents(false), validInitialScheduler(false), globalLowerBound(linearEquationSolverRequirements.requiresGlobalLowerBound()), globalUpperBound(linearEquationSolverRequirements.requiresGlobalUpperBound()) {
+        MinMaxLinearEquationSolverRequirements::MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements) : noEndComponents(false), validInitialScheduler(false), lowerBounds(linearEquationSolverRequirements.requiresLowerBounds()), upperBounds(linearEquationSolverRequirements.requiresUpperBounds()) {
             // Intentionally left empty.
         }
         
@@ -17,13 +17,13 @@ namespace storm {
             return *this;
         }
         
-        MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireGlobalLowerBound() {
-            globalLowerBound = true;
+        MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireLowerBounds() {
+            lowerBounds = true;
             return *this;
         }
         
-        MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireGlobalUpperBound() {
-            globalUpperBound = true;
+        MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireUpperBounds() {
+            upperBounds = true;
             return *this;
         }
         
@@ -35,20 +35,20 @@ namespace storm {
             return validInitialScheduler;
         }
         
-        bool MinMaxLinearEquationSolverRequirements::requiresGlobalLowerBound() const {
-            return globalLowerBound;
+        bool MinMaxLinearEquationSolverRequirements::requiresLowerBounds() const {
+            return lowerBounds;
         }
         
-        bool MinMaxLinearEquationSolverRequirements::requiresGlobalUpperBound() const {
-            return globalUpperBound;
+        bool MinMaxLinearEquationSolverRequirements::requiresUpperBounds() const {
+            return upperBounds;
         }
         
         bool MinMaxLinearEquationSolverRequirements::requires(Element const& element) const {
             switch (element) {
                 case Element::NoEndComponents: return noEndComponents; break;
                 case Element::ValidInitialScheduler: return validInitialScheduler; break;
-                case Element::GlobalLowerBound: return globalLowerBound; break;
-                case Element::GlobalUpperBound: return globalUpperBound; break;
+                case Element::LowerBounds: return lowerBounds; break;
+                case Element::UpperBounds: return upperBounds; break;
             }
         }
         
@@ -61,16 +61,21 @@ namespace storm {
             validInitialScheduler = false;
         }
         
-        void MinMaxLinearEquationSolverRequirements::clearGlobalLowerBound() {
-            globalLowerBound = false;
+        void MinMaxLinearEquationSolverRequirements::clearLowerBounds() {
+            lowerBounds = false;
         }
         
-        void MinMaxLinearEquationSolverRequirements::clearGlobalUpperBound() {
-            globalUpperBound = false;
+        void MinMaxLinearEquationSolverRequirements::clearUpperBounds() {
+            upperBounds = false;
+        }
+        
+        void MinMaxLinearEquationSolverRequirements::clearBounds() {
+            clearLowerBounds();
+            clearUpperBounds();
         }
         
         bool MinMaxLinearEquationSolverRequirements::empty() const {
-            return !noEndComponents && !validInitialScheduler && !globalLowerBound && !globalUpperBound;
+            return !noEndComponents && !validInitialScheduler && !lowerBounds && !upperBounds;
         }
         
     }

src/storm/solver/MinMaxLinearEquationSolverRequirements.h

@@ -16,35 +16,36 @@ namespace storm {
                 ValidInitialScheduler,
                 
                 // Requirements that are related to bounds for the actual solution.
-                GlobalLowerBound,
-                GlobalUpperBound
+                LowerBounds,
+                UpperBounds
             };
             
             MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements = LinearEquationSolverRequirements());
             
             MinMaxLinearEquationSolverRequirements& requireNoEndComponents();
             MinMaxLinearEquationSolverRequirements& requireValidInitialScheduler();
-            MinMaxLinearEquationSolverRequirements& requireGlobalLowerBound();
-            MinMaxLinearEquationSolverRequirements& requireGlobalUpperBound();
+            MinMaxLinearEquationSolverRequirements& requireLowerBounds();
+            MinMaxLinearEquationSolverRequirements& requireUpperBounds();
 
             bool requiresNoEndComponents() const;
             bool requiresValidIntialScheduler() const;
-            bool requiresGlobalLowerBound() const;
-            bool requiresGlobalUpperBound() const;
+            bool requiresLowerBounds() const;
+            bool requiresUpperBounds() const;
             bool requires(Element const& element) const;
             
             void clearNoEndComponents();
             void clearValidInitialScheduler();
-            void clearGlobalLowerBound();
-            void clearGlobalUpperBound();
+            void clearLowerBounds();
+            void clearUpperBounds();
+            void clearBounds();
             
             bool empty() const;
             
         private:
             bool noEndComponents;
             bool validInitialScheduler;
-            bool globalLowerBound;
-            bool globalUpperBound;
+            bool lowerBounds;
+            bool upperBounds;
         };
         
     }

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -434,13 +434,7 @@ namespace storm {
             STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (SoundPower)");
             
             std::vector<ValueType>* lowerX = &x;
-            if (!this->cachedRowVector) {
-                this->cachedRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount(), this->getUpperBound());
-            } else {
-                for (auto& e : *this->cachedRowVector) {
-                    e = this->getUpperBound();
-                }
-            }
+            this->createUpperBoundsVector(this->cachedRowVector);
             std::vector<ValueType>* upperX = this->cachedRowVector.get();
             
             bool useGaussSeidelMultiplication = this->getSettings().getPowerMethodMultiplicationStyle() == storm::solver::MultiplicationStyle::GaussSeidel;

src/storm/utility/vector.h

@@ -883,6 +883,36 @@ namespace storm {
                 }
             }
             
+            /*!
+             * Takes the input vector and ensures that all entries conform to the bounds.
+             */
+            template <typename ValueType>
+            void clip(std::vector<ValueType>& x, ValueType const& bound, bool boundFromBelow) {
+                for (auto& entry : x) {
+                    if (boundFromBelow && entry < bound) {
+                        entry = bound;
+                    } else if (!boundFromBelow && entry > bound) {
+                        entry = bound;
+                    }
+                }
+            }
+
+            /*!
+             * Takes the input vector and ensures that all entries conform to the bounds.
+             */
+            template <typename ValueType>
+            void clip(std::vector<ValueType>& x, std::vector<ValueType> const& bounds, bool boundFromBelow) {
+                auto boundsIt = bounds.begin();
+                for (auto& entry : x) {
+                    if (boundFromBelow && entry < *boundsIt) {
+                        entry = *boundsIt;
+                    } else if (!boundFromBelow && entry > *boundsIt) {
+                        entry = *boundsIt;
+                    }
+                    ++boundsIt;
+                }
+            }
+
             /*!
              * Takes the given offset vector and applies the given contraint. That is, it produces another offset vector that contains
              * the relative offsets of the entries given by the constraint.

src/test/storm/solver/EliminationLinearEquationSolverTest.cpp

@@ -21,6 +21,7 @@ TEST(EliminationLinearEquationSolver, Solve) {
     
     storm::storage::SparseMatrix<double> A;
     ASSERT_NO_THROW(A = builder.build());
+    ASSERT_NO_THROW(A.convertToEquationSystem());
     
     std::vector<double> x(3);
     std::vector<double> b = {16, -4, -7};