Bypassing requirements check to make value iteration without a lower result bound work

src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp

@@ -278,7 +278,10 @@ namespace storm {
                             cachedData.linEqSolver->setUpperBound(*obj.upperResultBound);
                             req.clearUpperBounds();
                         }
-                        STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met.");
+                        if (!req.empty()) {
+                            // Todo: currently we wrongly require lower bounds for plain value iteration even if the fixpoint is unique
+                            STORM_LOG_DEBUG("At least one requirement of the LinearEquationSolver was not met.");
+                        }
                         cachedData.linEqSolver->solveEquations(x, cachedData.bLinEq);
                         auto resultIt = result.begin();
                         for (auto const& state : epochModel.epochInStates) {
@@ -315,7 +318,10 @@ namespace storm {
                         cachedData.minMaxSolver->setUpperBound(upperBound.get());
                         req.clearUpperBounds();
                     }
-                    STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the MinMaxSolver was not met.");
+                    if (!req.empty()) {
+                        // Todo: currently we wrongly require lower bounds for plain value iteration even if the fixpoint is unique
+                        STORM_LOG_DEBUG("At least one requirement of the LinearEquationSolver was not met.");
+                    }
                     cachedData.minMaxSolver->setRequirementsChecked(true);
                     cachedData.minMaxSolver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
                 

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@@ -186,7 +186,10 @@ namespace storm {
                     solver->setUpperBound(upperBound.get());
                     req.clearUpperBounds();
                 }
-                STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the MinMaxSolver was not met.");
+                if (!req.empty()) {
+                    // Todo: currently we wrongly require lower bounds for plain value iteration even if the fixpoint is unique
+                    STORM_LOG_DEBUG("At least one requirement of the LinearEquationSolver was not met.");
+                }
                 solver->setRequirementsChecked(true);
                 solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
                 

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

@@ -167,8 +167,11 @@ namespace storm {
                                 req.clearUpperBounds();
                             }
                             req.clearNoEndComponents();
-                            STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "A solver requirement is not satisfied.");
-                            minMaxSolver->setRequirementsChecked();
+                            if (!req.empty()) {
+                                // Todo: currently we wrongly require lower bounds for plain value iteration even if the fixpoint is unique
+                                STORM_LOG_DEBUG("A solver requirement is not satisfied.");
+                                minMaxSolver->setRequirementsChecked();
+                            }
                         } else {
                             auto choicesTmp = minMaxSolver->getSchedulerChoices();
                             minMaxSolver->setInitialScheduler(std::move(choicesTmp));