diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 9c009ccee..c8cb685e5 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -150,7 +150,7 @@ namespace storm { upperResultBound = storm::utility::one(); // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). - auto req = solverFactory->getRequirements(env, true); + auto req = solverFactory->getRequirements(env, true, boost::none, true); req.clearBounds(); STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement."); solverFactory->setRequirementsChecked(true); @@ -189,7 +189,7 @@ namespace storm { lowerResultBound = storm::utility::zero(); // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations). - auto req = solverFactory->getRequirements(env, true); + auto req = solverFactory->getRequirements(env, true, boost::none, true); req.clearLowerBounds(); if (req.requiresUpperBounds()) { solvingRequiresUpperRewardBounds = true; diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index ad3db92f0..62672023b 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -104,7 +104,7 @@ namespace storm { // Check for requirements of the solver. // The solution is unique as we assume non-zeno MAs. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir, true); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); @@ -403,7 +403,7 @@ namespace storm { std::vector x(numberOfSspStates); // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir, true); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); @@ -616,7 +616,7 @@ namespace storm { // Check for requirements of the solver. // The solution is unique as we assume non-zeno MAs. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir, true); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); requirements.clearLowerBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp index 8505ab035..211a12cc4 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp @@ -303,7 +303,7 @@ namespace storm { result->solver->setHasUniqueSolution(true); result->solver->setTrackScheduler(true); result->solver->setCachingEnabled(true); - auto req = result->solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, true); + auto req = result->solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, false); boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true)); if (lowerBound) { result->solver->setLowerBound(lowerBound.get()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index bd93a44ef..068d08b63 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -179,7 +179,7 @@ namespace storm { solver->setTrackScheduler(true); solver->setHasUniqueSolution(true); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); - auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, true); + auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize); setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), weightVector, objectivesWithNoUpperTimeBound, ecQuotient->matrix, ecQuotient->rowsWithSumLessOne, ecQuotient->auxChoiceValues); if (solver->hasLowerBound()) { req.clearLowerBounds(); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index ad1903d1c..2e14497d5 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -146,7 +146,7 @@ namespace storm { // If we minimize, we know that the solution to the equation system is unique. bool uniqueSolution = dir == storm::solver::OptimizationDirection::Minimize; // Check for requirements of the solver early so we can adjust the maybe state computation accordingly. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir, true); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; SolverRequirementsData solverRequirementsData; bool extendMaybeStates = false; @@ -517,7 +517,7 @@ namespace storm { // If we maximize, we know that the solution to the equation system is unique. bool uniqueSolution = dir == storm::solver::OptimizationDirection::Maximize; // Check for requirements of the solver this early so we can adapt the maybe states accordingly. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir, true); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; bool extendMaybeStates = false; if (!clearedRequirements.empty()) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 10311c2a2..91ff99c8a 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -433,7 +433,7 @@ namespace storm { // Check for requirements of the solver. bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().hasSchedulerHint(); - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir, !hasSchedulerHint); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir, hasSchedulerHint); if (!requirements.empty()) { // If the solver still requires no end-components, we have to eliminate them later. @@ -1298,7 +1298,7 @@ namespace storm { storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates); // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, goal.direction(), true); + 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."); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 5e7600feb..bb4886094 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -212,12 +212,12 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& assumeNoInitialScheduler) const { + MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& hasInitialScheduler) const { auto method = getMethod(env, storm::NumberTraits::IsExact); // Start by getting the requirements of the linear equation solver. LinearEquationSolverTask linEqTask = LinearEquationSolverTask::Unspecified; - if ((method == MinMaxMethod::ValueIteration && !this->hasInitialScheduler() && assumeNoInitialScheduler) || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::QuickValueIteration) { + if ((method == MinMaxMethod::ValueIteration && !this->hasInitialScheduler() && !hasInitialScheduler) || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::QuickValueIteration) { linEqTask = LinearEquationSolverTask::Multiply; } MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env, linEqTask)); diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index fac4555fc..f8943a57a 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -26,7 +26,7 @@ namespace storm { virtual void clearCache() const override; - virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& hasInitialScheduler = false) const override; private: diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 2067c7949..3add9ad41 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -111,7 +111,7 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& assumeNoInitialScheduler) const { + MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& hasInitialScheduler) const { MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env, LinearEquationSolverTask::Multiply)); diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h index df20e120f..e8a531e67 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.h +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -21,7 +21,7 @@ namespace storm { virtual void clearCache() const override; - virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& hasInitialScheduler = false) const override; private: std::unique_ptr> lpSolverFactory; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 3c76d2f9e..433e02c11 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -137,7 +137,7 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver::getRequirements(Environment const&, boost::optional const& direction, bool const& assumeNoInitialScheduler) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver::getRequirements(Environment const&, boost::optional const& direction, bool const& hasInitialScheduler) const { return MinMaxLinearEquationSolverRequirements(); } @@ -167,11 +167,11 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional const& direction, bool const& assumeNoInitialScheduler) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional const& direction, bool const& hasInitialScheduler) const { // Create dummy solver and ask it for requirements. std::unique_ptr> solver = this->create(env); solver->setHasUniqueSolution(hasUniqueSolution); - return solver->getRequirements(env, direction, assumeNoInitialScheduler); + return solver->getRequirements(env, direction, hasInitialScheduler); } template diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index cb442e0f4..159b3e46e 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -167,7 +167,7 @@ namespace storm { * Retrieves the requirements of this solver for solving equations with the current settings. The requirements * are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const; + virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& hasInitialScheduler = false) const; /*! * Notifies the solver that the requirements for solving equations have been checked. If this has not been @@ -220,7 +220,7 @@ namespace storm { * Retrieves the requirements of the solver that would be created when calling create() right now. The * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type. */ - MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const; + MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, boost::optional const& direction = boost::none, bool const& hasInitialScheduler = false) const; void setRequirementsChecked(bool value = true); bool isRequirementsCheckedSet() const; diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp index 0e285c82e..c90dec99b 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -317,19 +317,6 @@ namespace storm { this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution()); this->sccSolver->setTrackScheduler(this->isTrackSchedulerSet()); - // Requirements - auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir); - if (req.requiresUpperBounds() && this->hasUpperBound()) { - req.clearUpperBounds(); - } - if (req.requiresLowerBounds() && this->hasLowerBound()) { - req.clearLowerBounds(); - } - if (req.requiresValidInitialScheduler() && this->hasInitialScheduler()) { - req.clearValidInitialScheduler(); - } - STORM_LOG_THROW(req.empty(), storm::exceptions::UnmetRequirementException, "Requirements of underlying solver not met."); - // SCC Matrix storm::storage::SparseMatrix sccA = this->A->getSubmatrix(true, sccRowGroups, sccRowGroups); this->sccSolver->setMatrix(std::move(sccA)); @@ -368,6 +355,19 @@ namespace storm { this->sccSolver->setUpperBounds(storm::utility::vector::filterVector(this->getUpperBounds(), sccRowGroups)); } + // Requirements + auto req = this->sccSolver->getRequirements(sccSolverEnvironment, dir); + if (req.requiresUpperBounds() && this->hasUpperBound()) { + req.clearUpperBounds(); + } + if (req.requiresLowerBounds() && this->hasLowerBound()) { + req.clearLowerBounds(); + } + if (req.requiresValidInitialScheduler() && this->hasInitialScheduler()) { + req.clearValidInitialScheduler(); + } + STORM_LOG_THROW(req.empty(), storm::exceptions::UnmetRequirementException, "Requirements of underlying solver not met."); + // Invoke scc solver bool res = this->sccSolver->solveEquations(sccSolverEnvironment, dir, sccX, sccB); //std::cout << "rhs is " << storm::utility::vector::toString(sccB) << std::endl; @@ -403,9 +403,9 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements TopologicalMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& assumeNoInitialScheduler) const { + MinMaxLinearEquationSolverRequirements TopologicalMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& hasInitialScheduler) const { // Return the requirements of the underlying solver - return GeneralMinMaxLinearEquationSolverFactory().getRequirements(getEnvironmentForUnderlyingSolver(env), this->hasUniqueSolution(), direction, assumeNoInitialScheduler); + return GeneralMinMaxLinearEquationSolverFactory().getRequirements(getEnvironmentForUnderlyingSolver(env), this->hasUniqueSolution(), direction, hasInitialScheduler); } template diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h index d1ad36e4a..3ac93955d 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h @@ -25,7 +25,7 @@ namespace storm { virtual void clearCache() const override; virtual void repeatedMultiply(Environment const& env, OptimizationDirection d, std::vector& x, std::vector const* b, uint_fast64_t n = 1) const override; - virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const override ; + virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& hasInitialScheduler = false) const override ; protected: