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));