Respected that the solution is unique when doing value iteration

src/storm/solver/AbstractEquationSolver.cpp

@@ -168,6 +168,16 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        void AbstractEquationSolver<ValueType>::createUpperBoundsVector(std::vector<ValueType>& upperBoundsVector) const {
+            STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s).");
+            if (this->hasUpperBound(BoundType::Global)) {
+                upperBoundsVector.assign(upperBoundsVector.size(), this->getUpperBound());
+            } else {
+                upperBoundsVector.assign(this->getUpperBounds().begin(), this->getUpperBounds().end());
+            }
+        }
+        
         template<typename ValueType>
         void AbstractEquationSolver<ValueType>::createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector, uint64_t length) const {
             STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s).");
@@ -179,17 +189,7 @@ namespace storm {
                     upperBoundsVector = std::make_unique<std::vector<ValueType>>(length, this->getUpperBound());
                 }
             } else {
-                if (this->hasUpperBound(BoundType::Global)) {
-                    for (auto& e : *upperBoundsVector) {
-                        e = this->getUpperBound();
-                    }
-                } else {
-                    auto upperBoundsIt = this->getUpperBounds().begin();
-                    for (auto& e : *upperBoundsVector) {
-                        e = *upperBoundsIt;
-                        ++upperBoundsIt;
-                    }
-                }
+                createUpperBoundsVector(*upperBoundsVector);
             }
         }
         

src/storm/solver/AbstractEquationSolver.h

@@ -160,6 +160,7 @@ namespace storm {
             TerminationCondition<ValueType> const& getTerminationCondition() const;
             std::unique_ptr<TerminationCondition<ValueType>> const& getTerminationConditionPointer() const;
             
+            void createUpperBoundsVector(std::vector<ValueType>& upperBoundsVector) const;
             void createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector, uint64_t length) const;
             void createLowerBoundsVector(std::vector<ValueType>& lowerBoundsVector) const;
 

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -367,9 +367,8 @@ namespace storm {
                 auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
             }
             
-            // By default, the guarantee that we can provide is that our solution is always less-or-equal than the
-            // actual solution.
-            SolverGuarantee guarantee = SolverGuarantee::LessOrEqual;
+            // By default, we can not provide any guarantee
+            SolverGuarantee guarantee = SolverGuarantee::None;
             
             if (this->hasInitialScheduler()) {
                 // Resolve the nondeterminism according to the initial scheduler.
@@ -391,14 +390,21 @@ namespace storm {
                 }
                 submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector);
                 
-                // If we were given an initial scheduler and are in fact minimizing, our current solution becomes
-                // always greater-or-equal than the actual solution.
-                if (dir == storm::OptimizationDirection::Minimize) {
+                // If we were given an initial scheduler and are maximizing (minimizing), our current solution becomes
+                // always less-or-equal (greater-or-equal) than the actual solution.
+                if (dir == storm::OptimizationDirection::Maximize) {
+                    guarantee = SolverGuarantee::LessOrEqual;
+                } else {
+                    guarantee = SolverGuarantee::GreaterOrEqual;
+                }
+            } else if (!this->hasUniqueSolution()) {
+                if (dir == storm::OptimizationDirection::Maximize) {
+                    this->createLowerBoundsVector(x);
+                    guarantee = SolverGuarantee::LessOrEqual;
+                } else {
+                    this->createUpperBoundsVector(x);
                     guarantee = SolverGuarantee::GreaterOrEqual;
                 }
-            } else {
-                // If no initial scheduler is given, we start from the lower bound.
-                this->createLowerBoundsVector(x);
             }
 
             std::vector<ValueType>* newX = auxiliaryRowGroupVector.get();

src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -280,11 +280,15 @@ namespace storm {
             // Set up the environment.
             storm::dd::Add<DdType, ValueType> localX;
             
-            // If we were given an initial scheduler, we take its solution as the starting point.
-            if (this->hasInitialScheduler()) {
-                localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b);
+            if (this->hasUniqueSolution()) {
+                localX = x;
             } else {
-                localX = this->getLowerBoundsVector();
+                // If we were given an initial scheduler, we take its solution as the starting point.
+                if (this->hasInitialScheduler()) {
+                    localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b);
+                } else {
+                    localX = this->getLowerBoundsVector();
+                }
             }
             
             ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->settings.getMaximalNumberOfIterations());