diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index c27d7114e..a199b3781 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -152,7 +152,7 @@ namespace storm { // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). auto req = solverFactory->getRequirements(env, true, boost::none, true); req.clearBounds(); - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); solverFactory->setRequirementsChecked(true); } @@ -191,11 +191,11 @@ namespace storm { // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). auto req = solverFactory->getRequirements(env, true, boost::none, true); req.clearLowerBounds(); - if (req.requiresUpperBounds()) { + if (req.upperBounds()) { solvingRequiresUpperRewardBounds = true; req.clearUpperBounds(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); solverFactory->setRequirementsChecked(true); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 931693450..7e50785d0 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -492,7 +492,8 @@ namespace storm { { // Check solver requirements storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; - STORM_LOG_THROW(linearEquationSolverFactory.getRequirements(env).empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the linear equation solver could not be matched."); + auto requirements = linearEquationSolverFactory.getRequirements(env); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); // Check whether we have the right input format for the solver. STORM_LOG_THROW(linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem, storm::exceptions::FormatUnsupportedBySolverException, "The selected solver does not support the required format."); std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(bsccEquationSystem)); @@ -565,7 +566,8 @@ namespace storm { { storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; // Check solver requirements - STORM_LOG_THROW(linearEquationSolverFactory.getRequirements(env).empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the linear equation solver could not be matched."); + auto requirements = linearEquationSolverFactory.getRequirements(env); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); // Check whether we have the right input format for the solver. STORM_LOG_THROW(linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem, storm::exceptions::FormatUnsupportedBySolverException, "The selected solver does not support the required format."); std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(rewardEquationSystemMatrix)); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 164310b20..8eb688d55 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -287,7 +287,7 @@ namespace storm { storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); requirements.clearBounds(); - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); if (numberOfProbabilisticChoices > 0) { solver = minMaxLinearEquationSolverFactory.create(env, probMatrix); @@ -449,7 +449,7 @@ namespace storm { storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); requirements.clearBounds(); - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(env, aProbabilistic); solver->setHasUniqueSolution(); @@ -757,7 +757,7 @@ namespace storm { storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); requirements.clearBounds(); - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(env, sspMatrix); solver->setHasUniqueSolution(); @@ -971,7 +971,7 @@ namespace storm { storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); requirements.clearLowerBounds(); - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); auto solver = minMaxLinearEquationSolverFactory.create(env, std::move(aProbabilistic)); solver->setLowerBound(storm::utility::zero()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp index cc748983d..f5137b0a7 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp @@ -295,7 +295,7 @@ namespace storm { cachedData.linEqSolver->setUpperBound(*obj.upperResultBound); req.clearUpperBounds(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); cachedData.linEqSolver->solveEquations(env, x, cachedData.bLinEq); auto resultIt = result.begin(); for (auto const& state : epochModel.epochInStates) { @@ -331,7 +331,7 @@ namespace storm { cachedData.minMaxSolver->setUpperBound(upperBound.get()); req.clearUpperBounds(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); cachedData.minMaxSolver->setRequirementsChecked(true); cachedData.minMaxSolver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp index 211a12cc4..d43db0d5c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp @@ -314,7 +314,7 @@ namespace storm { result->solver->setUpperBound(upperBound.get()); req.clearUpperBounds(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the MinMaxSolver was not met."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); result->solver->setRequirementsChecked(true); result->solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 9a8b39c4e..3dd8e8988 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -180,14 +180,14 @@ namespace storm { solver->setHasUniqueSolution(true); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize); - setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), weightVector, objectivesWithNoUpperTimeBound, ecQuotient->matrix, ecQuotient->rowsWithSumLessOne, ecQuotient->auxChoiceValues); + setBoundsToSolver(*solver, req.lowerBounds(), req.upperBounds(), weightVector, objectivesWithNoUpperTimeBound, ecQuotient->matrix, ecQuotient->rowsWithSumLessOne, ecQuotient->auxChoiceValues); if (solver->hasLowerBound()) { req.clearLowerBounds(); } if (solver->hasUpperBound()) { req.clearUpperBounds(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); solver->setRequirementsChecked(true); // Use the (0...0) vector as initial guess for the solution. @@ -266,15 +266,14 @@ namespace storm { solver->clearBounds(); storm::storage::BitVector submatrixRowsWithSumLessOne = deterministicMatrix.getRowFilter(maybeStates, maybeStates) % maybeStates; submatrixRowsWithSumLessOne.complement(); - this->setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b); + this->setBoundsToSolver(*solver, req.lowerBounds(), req.upperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b); if (solver->hasLowerBound()) { req.clearLowerBounds(); } if (solver->hasUpperBound()) { req.clearUpperBounds(); } - - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); solver->solveEquations(env, x, b); // Set the result for this objective accordingly storm::utility::vector::setVectorValues(objectiveResults[objIndex], maybeStates, x); diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index b90aa25be..659a17cab 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -72,7 +72,7 @@ namespace storm { auto req = linearEquationSolverFactory.getRequirements(env); req.clearLowerBounds(); req.clearUpperBounds(); - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the linear equation solver could not be matched."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); // Check whether we need to create an equation system. bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; @@ -285,14 +285,14 @@ namespace storm { storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; auto req = linearEquationSolverFactory.getRequirements(env); req.clearLowerBounds(); - if (req.requiresUpperBounds()) { + if (req.upperBounds()) { storm::dd::Add targetStatesAsColumn = targetStates.template toAdd(); targetStatesAsColumn = targetStatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs()); oneStepTargetProbs = submatrix * targetStatesAsColumn; oneStepTargetProbs = oneStepTargetProbs->sumAbstract(model.getColumnVariables()); req.clearUpperBounds(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the linear equation solver could not be matched."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); // Check whether we need to create an equation system. bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 90fbd61d0..cca377b9d 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -155,18 +155,18 @@ namespace storm { SolverRequirementsData solverRequirementsData; bool extendMaybeStates = false; - if (!clearedRequirements.empty()) { - if (clearedRequirements.requiresNoEndComponents()) { + if (clearedRequirements.hasEnabledRequirement()) { + if (clearedRequirements.noEndComponents()) { STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); extendMaybeStates = true; clearedRequirements.clearNoEndComponents(); } - if (clearedRequirements.requiresValidInitialScheduler()) { + if (clearedRequirements.validInitialScheduler()) { STORM_LOG_DEBUG("Scheduling valid scheduler computation, because the solver requires it."); clearedRequirements.clearValidInitialScheduler(); } clearedRequirements.clearBounds(); - STORM_LOG_THROW(clearedRequirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + STORM_LOG_THROW(!clearedRequirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + clearedRequirements.getEnabledRequirementsAsString() + " not checked."); } storm::dd::Bdd extendedMaybeStates = maybeStates; @@ -228,7 +228,7 @@ namespace storm { explicitRepresentation = submatrix.toMatrixVector(subvector, model.getNondeterminismVariables(), odd, odd); conversionWatch.stop(); - if (requirements.requiresValidInitialScheduler()) { + if (requirements.validInitialScheduler()) { solverRequirementsData.initialScheduler = computeValidInitialSchedulerForUntilProbabilities(explicitRepresentation.first, explicitRepresentation.second); } } @@ -251,7 +251,7 @@ namespace storm { solver->solveEquations(env, dir, x, explicitRepresentation.second); // If we included some target and non-filter states in the ODD, we need to expand the result from the solver. - if (requirements.requiresNoEndComponents() && solverRequirementsData.ecInformation) { + if (requirements.noEndComponents() && solverRequirementsData.ecInformation) { std::vector extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits()); solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x); x = std::move(extendedVector); @@ -549,24 +549,24 @@ namespace storm { storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; bool extendMaybeStates = false; - if (!clearedRequirements.empty()) { - if (clearedRequirements.requiresNoEndComponents()) { + if (clearedRequirements.hasEnabledRequirement()) { + if (clearedRequirements.noEndComponents()) { STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); extendMaybeStates = true; clearedRequirements.clearNoEndComponents(); } - if (clearedRequirements.requiresValidInitialScheduler()) { + if (clearedRequirements.validInitialScheduler()) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); extendMaybeStates = true; clearedRequirements.clearValidInitialScheduler(); } clearedRequirements.clearLowerBounds(); - if (clearedRequirements.requiresUpperBounds()) { + if (clearedRequirements.upperBounds()) { STORM_LOG_DEBUG("Computing upper bounds, because the solver requires it."); extendMaybeStates = true; clearedRequirements.clearUpperBounds(); } - STORM_LOG_THROW(clearedRequirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + STORM_LOG_THROW(!clearedRequirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + clearedRequirements.getEnabledRequirementsAsString() + " not checked."); } // Compute the set of maybe states that we are required to keep in the translation to explicit. @@ -611,17 +611,17 @@ namespace storm { storm::storage::BitVector targetStates = computeTargetStatesForReachabilityRewardsFromExplicitRepresentation(explicitRepresentation.first); solverRequirementsData.properMaybeStates = ~targetStates; - if (requirements.requiresNoEndComponents()) { - eliminateEndComponentsAndTargetStatesReachabilityRewards(explicitRepresentation, solverRequirementsData, targetStates, requirements.requiresUpperBounds()); + if (requirements.noEndComponents()) { + eliminateEndComponentsAndTargetStatesReachabilityRewards(explicitRepresentation, solverRequirementsData, targetStates, requirements.upperBounds()); // The solution becomes unique after end components have been eliminated. uniqueSolution = true; } else { - if (requirements.requiresValidInitialScheduler()) { + if (requirements.validInitialScheduler()) { // Compute a valid initial scheduler. solverRequirementsData.initialScheduler = computeValidInitialSchedulerForReachabilityRewards(explicitRepresentation.first, solverRequirementsData.properMaybeStates, targetStates); } - if (requirements.requiresUpperBounds()) { + if (requirements.upperBounds()) { solverRequirementsData.oneStepTargetProbabilities = computeOneStepTargetProbabilitiesFromExtendedExplicitRepresentation(explicitRepresentation.first, solverRequirementsData.properMaybeStates, targetStates); } @@ -641,7 +641,7 @@ namespace storm { solver->setHasUniqueSolution(uniqueSolution); // If the solver requires upper bounds, compute them now. - if (requirements.requiresUpperBounds()) { + if (requirements.upperBounds()) { setUpperRewardBounds(*solver, dir, explicitRepresentation.first, explicitRepresentation.second, solverRequirementsData.oneStepTargetProbabilities.get()); } @@ -657,7 +657,7 @@ namespace storm { solver->solveEquations(env, dir, x, explicitRepresentation.second); // If we eliminated end components, we need to extend the solution vector. - if (requirements.requiresNoEndComponents() && solverRequirementsData.ecInformation) { + if (requirements.noEndComponents() && solverRequirementsData.ecInformation) { std::vector extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits()); solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x); x = std::move(extendedVector); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 9e0da7157..03d3fb1a0 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -128,7 +128,7 @@ namespace storm { linEqSolver->setUpperBound(upperBound.get()); req.clearUpperBounds(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); } // Prepare the right hand side of the equation system @@ -487,11 +487,11 @@ namespace storm { storm::solver::LinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env); boost::optional> upperRewardBounds; requirements.clearLowerBounds(); - if (requirements.requiresUpperBounds()) { + if (requirements.upperBounds()) { upperRewardBounds = computeUpperRewardBounds(submatrix, b, transitionMatrix.getConstrainedRowSumVector(maybeStates, rew0States)); requirements.clearUpperBounds(); } - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver."); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); // If necessary, convert the matrix from the fixpoint notation to the form needed for the equation system. if (convertToEquationSystem) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 2acc4f299..0609db7ee 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -158,7 +158,7 @@ namespace storm { minMaxSolver->setUpperBound(upperBound.get()); req.clearUpperBounds(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); minMaxSolver->setRequirementsChecked(); } else { auto choicesTmp = minMaxSolver->getSchedulerChoices(); @@ -437,10 +437,9 @@ namespace storm { bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint(); storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir, hasSchedulerHint); - if (!requirements.empty()) { - + if (requirements.hasEnabledRequirement()) { // If the solver still requires no end-components, we have to eliminate them later. - if (requirements.requiresNoEndComponents()) { + if (requirements.noEndComponents()) { STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique."); STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it."); result.eliminateEndComponents = true; @@ -450,7 +449,7 @@ namespace storm { } // If the solver requires an initial scheduler, compute one now. - if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { + if (requirements.validInitialScheduler()) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); result.schedulerHint = computeValidSchedulerHint(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates); requirements.clearValidInitialScheduler(); @@ -462,11 +461,11 @@ namespace storm { } else if (type == SolutionType::ExpectedRewards) { requirements.clearLowerBounds(); } - if (requirements.requiresUpperBounds()) { + if (requirements.upperBounds()) { result.computeUpperBounds = true; requirements.clearUpperBounds(); } - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver."); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); } else { STORM_LOG_DEBUG("Solver has no requirements."); } @@ -1343,7 +1342,8 @@ namespace storm { storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, goal.direction()); requirements.clearBounds(); - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); + std::vector sspResult(numberOfSspStates); goal.restrictRelevantValues(statesNotContainedInAnyMec); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 506396a54..d5c9fea6e 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -75,20 +75,20 @@ namespace storm { // Check requirements of solver. storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(env, dir); boost::optional> initialScheduler; - if (!requirements.empty()) { - if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { + if (requirements.hasEnabledRequirement()) { + if (requirements.validInitialScheduler()) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); initialScheduler = computeValidSchedulerHint(EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability1); requirements.clearValidInitialScheduler(); } requirements.clearBounds(); - if (requirements.requiresNoEndComponents()) { + if (requirements.noEndComponents()) { // Check whether there are end components if (storm::utility::graph::performProb0E(model, transitionMatrix.notZero(), maybeStates, !maybeStates && model.getReachableStates()).isZero()) { requirements.clearNoEndComponents(); } } - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver."); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); } if (initialScheduler) { solver->setInitialScheduler(initialScheduler.get()); @@ -246,20 +246,20 @@ namespace storm { // Check requirements of solver. storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(env, dir); boost::optional> initialScheduler; - if (!requirements.empty()) { - if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) { + if (requirements.hasEnabledRequirement()) { + if (requirements.validInitialScheduler()) { STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it."); initialScheduler = computeValidSchedulerHint(EquationSystemType::ExpectedRewards, model, transitionMatrix, maybeStates, targetStates); requirements.clearValidInitialScheduler(); } requirements.clearLowerBounds(); - if (requirements.requiresNoEndComponents()) { + if (requirements.noEndComponents()) { // Check whether there are end components if (storm::utility::graph::performProb0E(model, transitionMatrixBdd, maybeStates, !maybeStates && model.getReachableStates()).isZero()) { requirements.clearNoEndComponents(); } } - STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Could not establish requirements of solver."); + STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); } if (initialScheduler) { solver->setInitialScheduler(initialScheduler.get()); diff --git a/src/storm/solver/LinearEquationSolverRequirements.cpp b/src/storm/solver/LinearEquationSolverRequirements.cpp index 90662c6f9..445e776d7 100644 --- a/src/storm/solver/LinearEquationSolverRequirements.cpp +++ b/src/storm/solver/LinearEquationSolverRequirements.cpp @@ -3,52 +3,78 @@ namespace storm { namespace solver { - LinearEquationSolverRequirements::LinearEquationSolverRequirements() : lowerBounds(false), upperBounds(false) { + LinearEquationSolverRequirements::LinearEquationSolverRequirements() { // Intentionally left empty. } - LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireLowerBounds() { - lowerBounds = true; + LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireLowerBounds(bool critical) { + lowerBoundsRequirement.enable(critical); return *this; } - LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireUpperBounds() { - upperBounds = true; + LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireUpperBounds(bool critical) { + upperBoundsRequirement.enable(critical); return *this; } - LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireBounds() { - requireLowerBounds(); - requireUpperBounds(); + LinearEquationSolverRequirements& LinearEquationSolverRequirements::requireBounds(bool critical) { + requireLowerBounds(critical); + requireUpperBounds(critical); return *this; } - bool LinearEquationSolverRequirements::requiresLowerBounds() const { - return lowerBounds; + SolverRequirement const& LinearEquationSolverRequirements::lowerBounds() const { + return lowerBoundsRequirement; } - bool LinearEquationSolverRequirements::requiresUpperBounds() const { - return upperBounds; + SolverRequirement const& LinearEquationSolverRequirements::upperBounds() const { + return upperBoundsRequirement; } - bool LinearEquationSolverRequirements::requires(Element const& element) const { + SolverRequirement const& LinearEquationSolverRequirements::get(Element const& element) const { switch (element) { - case Element::LowerBounds: return lowerBounds; break; - case Element::UpperBounds: return upperBounds; break; + case Element::LowerBounds: return lowerBounds(); break; + case Element::UpperBounds: return upperBounds(); break; } } void LinearEquationSolverRequirements::clearLowerBounds() { - lowerBounds = false; + lowerBoundsRequirement.clear(); } void LinearEquationSolverRequirements::clearUpperBounds() { - upperBounds = false; + upperBoundsRequirement.clear(); } - bool LinearEquationSolverRequirements::empty() const { - return !lowerBounds && !upperBounds; + bool LinearEquationSolverRequirements::hasEnabledRequirement() const { + return lowerBoundsRequirement || upperBoundsRequirement; } + bool LinearEquationSolverRequirements::hasEnabledCriticalRequirement() const { + return lowerBoundsRequirement.isCritical() || upperBoundsRequirement.isCritical(); + } + + + std::string LinearEquationSolverRequirements::getEnabledRequirementsAsString() const { + std::string res = "["; + bool first = true; + if (lowerBounds()) { + if (!first) { res += ", "; } else {first = false;} + res += "lowerBounds"; + if (lowerBounds().isCritical()) { + res += "(mandatory)"; + } + } + if (upperBounds()) { + if (!first) { res += ", "; } else {first = false;} + res += "upperBounds"; + if (upperBounds().isCritical()) { + res += "(mandatory)"; + } + } + res += "]"; + return res; + } + } } diff --git a/src/storm/solver/LinearEquationSolverRequirements.h b/src/storm/solver/LinearEquationSolverRequirements.h index 8f5a126a7..a7e23d248 100644 --- a/src/storm/solver/LinearEquationSolverRequirements.h +++ b/src/storm/solver/LinearEquationSolverRequirements.h @@ -1,5 +1,9 @@ #pragma once +#include + +#include "storm/solver/SolverRequirement.h" + namespace storm { namespace solver { @@ -14,22 +18,29 @@ namespace storm { LinearEquationSolverRequirements(); - LinearEquationSolverRequirements& requireLowerBounds(); - LinearEquationSolverRequirements& requireUpperBounds(); - LinearEquationSolverRequirements& requireBounds(); + LinearEquationSolverRequirements& requireLowerBounds(bool critical = true); + LinearEquationSolverRequirements& requireUpperBounds(bool critical = true); + LinearEquationSolverRequirements& requireBounds(bool critical = true); - bool requiresLowerBounds() const; - bool requiresUpperBounds() const; - bool requires(Element const& element) const; + SolverRequirement const& lowerBounds() const; + SolverRequirement const& upperBounds() const; + SolverRequirement const& get(Element const& element) const; void clearLowerBounds(); void clearUpperBounds(); - bool empty() const; + bool hasEnabledRequirement() const; + bool hasEnabledCriticalRequirement() const; + + /*! + * Checks whether there are no critical requirements left. + * In case there is a critical requirement left an exception is thrown. + */ + std::string getEnabledRequirementsAsString() const; private: - bool lowerBounds; - bool upperBounds; + SolverRequirement lowerBoundsRequirement; + SolverRequirement upperBoundsRequirement; }; } diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp index 005d57977..e16bbdf54 100644 --- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp @@ -3,76 +3,76 @@ namespace storm { namespace solver { - MinMaxLinearEquationSolverRequirements::MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements) : noEndComponents(false), validInitialScheduler(false), lowerBounds(linearEquationSolverRequirements.requiresLowerBounds()), upperBounds(linearEquationSolverRequirements.requiresUpperBounds()) { + MinMaxLinearEquationSolverRequirements::MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements) : lowerBoundsRequirement(linearEquationSolverRequirements.lowerBounds()), upperBoundsRequirement(linearEquationSolverRequirements.upperBounds()) { // Intentionally left empty. } - MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireNoEndComponents() { - noEndComponents = true; + MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireNoEndComponents(bool critical) { + noEndComponentsRequirement.enable(critical); return *this; } - MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireValidInitialScheduler() { - validInitialScheduler = true; + MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireValidInitialScheduler(bool critical) { + validInitialSchedulerRequirement.enable(critical); return *this; } - MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireLowerBounds() { - lowerBounds = true; + MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireLowerBounds(bool critical) { + lowerBoundsRequirement.enable(critical); return *this; } - MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireUpperBounds() { - upperBounds = true; + MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireUpperBounds(bool critical) { + upperBoundsRequirement.enable(critical); return *this; } - MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireBounds() { - requireLowerBounds(); - requireUpperBounds(); + MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireBounds(bool critical) { + requireLowerBounds(critical); + requireUpperBounds(critical); return *this; } - bool MinMaxLinearEquationSolverRequirements::requiresNoEndComponents() const { - return noEndComponents; + SolverRequirement const& MinMaxLinearEquationSolverRequirements::noEndComponents() const { + return noEndComponentsRequirement; } - bool MinMaxLinearEquationSolverRequirements::requiresValidInitialScheduler() const { - return validInitialScheduler; + SolverRequirement const& MinMaxLinearEquationSolverRequirements::validInitialScheduler() const { + return validInitialSchedulerRequirement; } - bool MinMaxLinearEquationSolverRequirements::requiresLowerBounds() const { - return lowerBounds; + SolverRequirement const& MinMaxLinearEquationSolverRequirements::lowerBounds() const { + return lowerBoundsRequirement; } - bool MinMaxLinearEquationSolverRequirements::requiresUpperBounds() const { - return upperBounds; + SolverRequirement const& MinMaxLinearEquationSolverRequirements::upperBounds() const { + return upperBoundsRequirement; } - bool MinMaxLinearEquationSolverRequirements::requires(Element const& element) const { + SolverRequirement const& MinMaxLinearEquationSolverRequirements::get(Element const& element) const { switch (element) { - case Element::NoEndComponents: return noEndComponents; break; - case Element::ValidInitialScheduler: return validInitialScheduler; break; - case Element::LowerBounds: return lowerBounds; break; - case Element::UpperBounds: return upperBounds; break; + case Element::NoEndComponents: return noEndComponents(); break; + case Element::ValidInitialScheduler: return validInitialScheduler(); break; + case Element::LowerBounds: return lowerBounds(); break; + case Element::UpperBounds: return upperBounds(); break; } } void MinMaxLinearEquationSolverRequirements::clearNoEndComponents() { - noEndComponents = false; - validInitialScheduler = false; + noEndComponentsRequirement.clear(); + validInitialSchedulerRequirement.clear(); } void MinMaxLinearEquationSolverRequirements::clearValidInitialScheduler() { - validInitialScheduler = false; + validInitialSchedulerRequirement.clear(); } void MinMaxLinearEquationSolverRequirements::clearLowerBounds() { - lowerBounds = false; + lowerBoundsRequirement.clear(); } void MinMaxLinearEquationSolverRequirements::clearUpperBounds() { - upperBounds = false; + upperBoundsRequirement.clear(); } void MinMaxLinearEquationSolverRequirements::clearBounds() { @@ -80,8 +80,47 @@ namespace storm { clearUpperBounds(); } - bool MinMaxLinearEquationSolverRequirements::empty() const { - return !noEndComponents && !validInitialScheduler && !lowerBounds && !upperBounds; + bool MinMaxLinearEquationSolverRequirements::hasEnabledRequirement() const { + return noEndComponentsRequirement || validInitialSchedulerRequirement || lowerBoundsRequirement || upperBoundsRequirement; + } + + bool MinMaxLinearEquationSolverRequirements::hasEnabledCriticalRequirement() const { + return noEndComponentsRequirement.isCritical() || validInitialSchedulerRequirement.isCritical() || lowerBoundsRequirement.isCritical() || upperBoundsRequirement.isCritical(); + } + + std::string MinMaxLinearEquationSolverRequirements::getEnabledRequirementsAsString() const { + std::string res = "["; + bool first = true; + if (noEndComponents()) { + if (!first) { res += ", "; } else {first = false;} + res += "NoEndComponents"; + if (noEndComponents().isCritical()) { + res += "(mandatory)"; + } + } + if (validInitialScheduler()) { + if (!first) { res += ", "; } else {first = false;} + res += "validInitialScheduler"; + if (validInitialScheduler().isCritical()) { + res += "(mandatory)"; + } + } + if (lowerBounds()) { + if (!first) { res += ", "; } else {first = false;} + res += "lowerBounds"; + if (lowerBounds().isCritical()) { + res += "(mandatory)"; + } + } + if (upperBounds()) { + if (!first) { res += ", "; } else {first = false;} + res += "upperBounds"; + if (upperBounds().isCritical()) { + res += "(mandatory)"; + } + } + res += "]"; + return res; } } diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.h b/src/storm/solver/MinMaxLinearEquationSolverRequirements.h index 33e3511ad..06ba623c1 100644 --- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.h +++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.h @@ -1,6 +1,9 @@ #pragma once +#include + #include "storm/solver/LinearEquationSolverRequirements.h" +#include "storm/solver/SolverRequirement.h" namespace storm { namespace solver { @@ -20,19 +23,21 @@ namespace storm { UpperBounds }; + // The type of a requirement. + MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements = LinearEquationSolverRequirements()); - MinMaxLinearEquationSolverRequirements& requireNoEndComponents(); - MinMaxLinearEquationSolverRequirements& requireValidInitialScheduler(); - MinMaxLinearEquationSolverRequirements& requireLowerBounds(); - MinMaxLinearEquationSolverRequirements& requireUpperBounds(); - MinMaxLinearEquationSolverRequirements& requireBounds(); + MinMaxLinearEquationSolverRequirements& requireNoEndComponents(bool critical = true); + MinMaxLinearEquationSolverRequirements& requireValidInitialScheduler(bool critical = true); + MinMaxLinearEquationSolverRequirements& requireLowerBounds(bool critical = true); + MinMaxLinearEquationSolverRequirements& requireUpperBounds(bool critical = true); + MinMaxLinearEquationSolverRequirements& requireBounds(bool critical = true); - bool requiresNoEndComponents() const; - bool requiresValidInitialScheduler() const; - bool requiresLowerBounds() const; - bool requiresUpperBounds() const; - bool requires(Element const& element) const; + SolverRequirement const& noEndComponents() const; + SolverRequirement const& validInitialScheduler() const; + SolverRequirement const& lowerBounds() const; + SolverRequirement const& upperBounds() const; + SolverRequirement const& get(Element const& element) const; void clearNoEndComponents(); void clearValidInitialScheduler(); @@ -40,13 +45,19 @@ namespace storm { void clearUpperBounds(); void clearBounds(); - bool empty() const; + bool hasEnabledRequirement() const; + bool hasEnabledCriticalRequirement() const; + + /*! + * Returns a string that enumerates the enabled requirements + */ + std::string getEnabledRequirementsAsString() const; private: - bool noEndComponents; - bool validInitialScheduler; - bool lowerBounds; - bool upperBounds; + SolverRequirement noEndComponentsRequirement; + SolverRequirement validInitialSchedulerRequirement; + SolverRequirement lowerBoundsRequirement; + SolverRequirement upperBoundsRequirement; }; } diff --git a/src/storm/solver/SolverRequirement.cpp b/src/storm/solver/SolverRequirement.cpp new file mode 100644 index 000000000..c898840aa --- /dev/null +++ b/src/storm/solver/SolverRequirement.cpp @@ -0,0 +1,32 @@ +#include "storm/solver/SolverRequirement.h" + +#include + +#include "storm/utility/vector.h" + +namespace storm { + namespace solver { + SolverRequirement::SolverRequirement() : enabled(false), critical(false) { + // Intentionally left empty + } + + SolverRequirement::operator bool() const { + return enabled; + } + + void SolverRequirement::enable(bool critical) { + this->enabled = true; + this->critical = critical; + } + + void SolverRequirement::clear() { + enabled = false; + critical = false; + } + + bool SolverRequirement::isCritical() const { + return this->critical; + } + + } +} diff --git a/src/storm/solver/SolverRequirement.h b/src/storm/solver/SolverRequirement.h new file mode 100644 index 000000000..cfdac2e18 --- /dev/null +++ b/src/storm/solver/SolverRequirement.h @@ -0,0 +1,39 @@ +#pragma once + +namespace storm { + namespace solver { + + class SolverRequirement { + public: + + SolverRequirement(); + SolverRequirement(SolverRequirement const& other) = default; + + /*! + * Returns true if this is a requirement of the considered solver. + */ + operator bool() const; + + /*! + * Enables this requirement. + * @param critical if set, it is assumed that the solver will fail in case this requirement is not met + */ + void enable(bool critical = true); + + /*! + * Clears this requirement. + */ + void clear(); + + /*! + * Returns true if the solver fails in case this requirement is not met. + */ + bool isCritical() const; + + private: + bool enabled; + bool critical; + }; + + } +} diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index c0d7e0460..92692b966 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -8,7 +8,7 @@ #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidEnvironmentException.h" #include "storm/exceptions/UnexpectedException.h" -#include "storm/exceptions/UnmetRequirementException.h" +#include "storm/exceptions/UncheckedRequirementException.h" namespace storm { namespace solver { @@ -184,13 +184,13 @@ namespace storm { this->sccSolver->setInitialScheduler(std::move(choices)); } auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir); - if (req.requiresUpperBounds() && this->hasUpperBound()) { + if (req.upperBounds() && this->hasUpperBound()) { req.clearUpperBounds(); } - if (req.requiresLowerBounds() && this->hasLowerBound()) { + if (req.lowerBounds() && this->hasLowerBound()) { req.clearLowerBounds(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UnmetRequirementException, "Requirements of underlying solver not met."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); this->sccSolver->setRequirementsChecked(true); bool res = this->sccSolver->solveEquations(sccSolverEnvironment, dir, x, b); @@ -252,16 +252,16 @@ namespace storm { // Requirements auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir); - if (req.requiresUpperBounds() && this->hasUpperBound()) { + if (req.upperBounds() && this->hasUpperBound()) { req.clearUpperBounds(); } - if (req.requiresLowerBounds() && this->hasLowerBound()) { + if (req.lowerBounds() && this->hasLowerBound()) { req.clearLowerBounds(); } - if (req.requiresValidInitialScheduler() && this->hasInitialScheduler()) { + if (req.validInitialScheduler() && this->hasInitialScheduler()) { req.clearValidInitialScheduler(); } - STORM_LOG_THROW(req.empty(), storm::exceptions::UnmetRequirementException, "Requirements of underlying solver not met."); + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked."); this->sccSolver->setRequirementsChecked(true); // Invoke scc solver diff --git a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp index 707b6ba4c..725590bc8 100644 --- a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp +++ b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp @@ -152,7 +152,7 @@ namespace { solver->setBounds(this->parseNumber("0"), this->parseNumber("2")); storm::solver::MinMaxLinearEquationSolverRequirements req = solver->getRequirements(this->env()); req.clearBounds(); - ASSERT_TRUE(req.empty()); + ASSERT_FALSE(req.hasEnabledRequirement()); ASSERT_NO_THROW(solver->solveEquations(this->env(), storm::OptimizationDirection::Minimize, x, b)); EXPECT_NEAR(x[0], this->parseNumber("0.5"), this->precision());