diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 4e000dab5..bdf030f31 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -92,7 +92,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); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir, true); requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); @@ -382,7 +382,7 @@ namespace storm { std::vector x(numberOfSspStates); // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir, true); requirements.clearBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); @@ -595,7 +595,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); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir, true); requirements.clearLowerBounds(); STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver."); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index f8255bded..44bf2eb7a 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.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); + auto req = result->solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, true); 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/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index c0d25eeef..370b51da6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -175,7 +175,7 @@ namespace storm { std::unique_ptr> solver = solverFactory.create(env, ecQuotient->matrix); solver->setTrackScheduler(true); solver->setHasUniqueSolution(true); - auto req = solver->getRequirements(env); + auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, true); boost::optional lowerBound = this->computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound); if (lowerBound) { solver->setLowerBound(lowerBound.get()); diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 30fa8ad13..c38b32c91 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); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir, true); storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements; SolverRequirementsData solverRequirementsData; bool extendMaybeStates = false; @@ -513,7 +513,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); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir, true); 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 d347c1b24..1316eff78 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -147,7 +147,7 @@ namespace storm { minMaxSolver->setOptimizationDirection(dir); minMaxSolver->setCachingEnabled(true); minMaxSolver->setTrackScheduler(true); - auto req = minMaxSolver->getRequirements(env, dir); + auto req = minMaxSolver->getRequirements(env, dir, false); if (lowerBound) { minMaxSolver->setLowerBound(lowerBound.get()); req.clearLowerBounds(); @@ -432,7 +432,8 @@ namespace storm { || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); // Check for requirements of the solver. - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir); + bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint().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. @@ -1295,7 +1296,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()); + storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, goal.direction(), true); 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 03b512915..371dfab34 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -193,11 +193,18 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction) const { - // Start by copying the requirements of the linear equation solver. - MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env)); - + MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& assumeNoInitialScheduler) 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 || method == MinMaxMethod::RationalSearch) { + if (!this->hasInitialScheduler() && assumeNoInitialScheduler) { + linEqTask = LinearEquationSolverTask::Multiply; + } + } + MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env, linEqTask)); + if (method == MinMaxMethod::ValueIteration) { if (env.solver().isForceSoundness()) { // Interval iteration requires a unique solution and lower+upper bounds diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index df01754f4..f29fa0318 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) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const override; private: diff --git a/src/storm/solver/LinearEquationSolver.cpp b/src/storm/solver/LinearEquationSolver.cpp index 8ee143cf1..faf4951d2 100644 --- a/src/storm/solver/LinearEquationSolver.cpp +++ b/src/storm/solver/LinearEquationSolver.cpp @@ -112,7 +112,7 @@ namespace storm { } template - LinearEquationSolverRequirements LinearEquationSolver::getRequirements(Environment const& env) const { + LinearEquationSolverRequirements LinearEquationSolver::getRequirements(Environment const& env, LinearEquationSolverTask const& task) const { return LinearEquationSolverRequirements(); } @@ -155,8 +155,8 @@ namespace storm { } template - LinearEquationSolverRequirements LinearEquationSolverFactory::getRequirements(Environment const& env) const { - return this->create(env)->getRequirements(env); + LinearEquationSolverRequirements LinearEquationSolverFactory::getRequirements(Environment const& env, LinearEquationSolverTask const& task) const { + return this->create(env)->getRequirements(env, task); } template @@ -210,7 +210,7 @@ namespace storm { EquationSolverType type = env.solver().getLinearEquationSolverType(); // Adjust the solver type if none was specified and we want sound computations - if (env.solver().isForceSoundness() && task != LinearEquationSolverTask::Multiply, type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination) { + if (env.solver().isForceSoundness() && task != LinearEquationSolverTask::Multiply && type != EquationSolverType::Native && type != EquationSolverType::Eigen && type != EquationSolverType::Elimination) { if (env.solver().isLinearEquationSolverTypeSetFromDefaultValue()) { type = EquationSolverType::Native; STORM_LOG_INFO("Selecting '" + toString(type) + "' as the linear equation solver to guarantee sound results. If you want to override this, please explicitly specify a different solver."); diff --git a/src/storm/solver/LinearEquationSolver.h b/src/storm/solver/LinearEquationSolver.h index 6b45ec491..b4b49d627 100644 --- a/src/storm/solver/LinearEquationSolver.h +++ b/src/storm/solver/LinearEquationSolver.h @@ -132,7 +132,7 @@ namespace storm { * Retrieves the requirements of the solver under the current settings. Note that these requirements only * apply to solving linear equations and not to the matrix vector multiplications. */ - virtual LinearEquationSolverRequirements getRequirements(Environment const& env) const; + virtual LinearEquationSolverRequirements getRequirements(Environment const& env, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const; /*! * Sets whether some of the generated data during solver calls should be cached. @@ -217,7 +217,7 @@ namespace storm { * Retrieves the requirements of the solver if it was created with the current settings. Note that these * requirements only apply to solving linear equations and not to the matrix vector multiplications. */ - LinearEquationSolverRequirements getRequirements(Environment const& env) const; + LinearEquationSolverRequirements getRequirements(Environment const& env, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const; }; template diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index e7d92fe45..80668c4fc 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -111,9 +111,9 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver::getRequirements(Environment const& env, boost::optional const& direction, bool const& assumeNoInitialScheduler) const { - MinMaxLinearEquationSolverRequirements requirements; + MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env, LinearEquationSolverTask::Multiply)); // In case we need to retrieve a scheduler, the solution has to be unique if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) { diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h index 6d92b611b..df20e120f 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) const override; + virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const override; private: std::unique_ptr> lpSolverFactory; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 08b6c15d8..a061c451d 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -136,7 +136,7 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver::getRequirements(Environment const&, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver::getRequirements(Environment const&, boost::optional const& direction, bool const& assumeNoInitialScheduler) const { return MinMaxLinearEquationSolverRequirements(); } @@ -166,11 +166,11 @@ namespace storm { } template - MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional const& direction) const { + MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional const& direction, bool const& assumeNoInitialScheduler) const { // Create dummy solver and ask it for requirements. std::unique_ptr> solver = this->create(env); solver->setHasUniqueSolution(hasUniqueSolution); - return solver->getRequirements(env, direction); + return solver->getRequirements(env, direction, assumeNoInitialScheduler); } template diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index c2b30eeda..cb442e0f4 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) const; + virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = 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) const; + MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, boost::optional const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const; void setRequirementsChecked(bool value = true); bool isRequirementsCheckedSet() const; diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 387935970..c9974a700 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -929,13 +929,15 @@ namespace storm { } template - LinearEquationSolverRequirements NativeLinearEquationSolver::getRequirements(Environment const& env) const { + LinearEquationSolverRequirements NativeLinearEquationSolver::getRequirements(Environment const& env, LinearEquationSolverTask const& task) const { LinearEquationSolverRequirements requirements; - auto method = getMethod(env, storm::NumberTraits::IsExact); - if (method == NativeLinearEquationSolverMethod::Power && env.solver().isForceSoundness()) { - requirements.requireBounds(); - } else if (method == NativeLinearEquationSolverMethod::RationalSearch) { - requirements.requireLowerBounds(); + if (task != LinearEquationSolverTask::Multiply) { + auto method = getMethod(env, storm::NumberTraits::IsExact); + if (method == NativeLinearEquationSolverMethod::Power && env.solver().isForceSoundness()) { + requirements.requireBounds(); + } else if (method == NativeLinearEquationSolverMethod::RationalSearch) { + requirements.requireLowerBounds(); + } } return requirements; } diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h index 0fb4970e4..136c8f68f 100644 --- a/src/storm/solver/NativeLinearEquationSolver.h +++ b/src/storm/solver/NativeLinearEquationSolver.h @@ -37,7 +37,7 @@ namespace storm { virtual void multiplyAndReduceGaussSeidel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr) const override; virtual LinearEquationSolverProblemFormat getEquationProblemFormat(storm::Environment const& env) const override; - virtual LinearEquationSolverRequirements getRequirements(storm::Environment const& env) const override; + virtual LinearEquationSolverRequirements getRequirements(Environment const& env, LinearEquationSolverTask const& task = LinearEquationSolverTask::Unspecified) const override; virtual void clearCache() const override;