From 70dc9ce7ace11f36e3df7f4e891a8138153f5235 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 17 Oct 2017 13:14:13 +0200
Subject: [PATCH] Bypassing requirements check to make value iteration without
 a lower result bound work

---
 .../SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp  | 10 ++++++++--
 .../pcaa/SparsePcaaWeightVectorChecker.cpp             |  5 ++++-
 .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp |  7 +++++--
 3 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
index e019a0f88..00903898d 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
+++ b/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);
                 
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
index d9e3e95ff..0d02074b0 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
+++ b/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);
                 
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 53d81fbcd..17a38cfe3 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/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));