Checking requirements of a linear equation solver now depends on whether we want to do multiplication or equation solving. This was necessary to get the correct requirements of a MinMaxSolver that only uses the underlying linear equation solver for multiplication.

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<ValueType> 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.");
 

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<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true));
                 if (lowerBound) {
                     result->solver->setLowerBound(lowerBound.get());

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@@ -175,7 +175,7 @@ namespace storm {
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound);
                 if (lowerBound) {
                     solver->setLowerBound(lowerBound.get());

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<ValueType> 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()) {

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<ValueType>().getNoEndComponentsInMaybeStates());
                 
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir);
+                bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().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<ValueType> 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.");
                 

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -193,11 +193,18 @@ namespace storm {
         }
 
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
-            // Start by copying the requirements of the linear equation solver.
-            MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env));
-
+        MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& assumeNoInitialScheduler) const {
             auto method = getMethod(env, storm::NumberTraits<ValueType>::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

src/storm/solver/IterativeMinMaxLinearEquationSolver.h

@@ -26,7 +26,7 @@ namespace storm {
 
             virtual void clearCache() const override;
             
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const override;
             
         private:
             

src/storm/solver/LinearEquationSolver.cpp

@@ -112,7 +112,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        LinearEquationSolverRequirements LinearEquationSolver<ValueType>::getRequirements(Environment const& env) const {
+        LinearEquationSolverRequirements LinearEquationSolver<ValueType>::getRequirements(Environment const& env, LinearEquationSolverTask const& task) const {
             return LinearEquationSolverRequirements();
         }
         
@@ -155,8 +155,8 @@ namespace storm {
         }
         
         template<typename ValueType>
-        LinearEquationSolverRequirements LinearEquationSolverFactory<ValueType>::getRequirements(Environment const& env) const {
-            return this->create(env)->getRequirements(env);
+        LinearEquationSolverRequirements LinearEquationSolverFactory<ValueType>::getRequirements(Environment const& env, LinearEquationSolverTask const& task) const {
+            return this->create(env)->getRequirements(env, task);
         }
         
         template<typename ValueType>
@@ -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.");

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<typename ValueType>

src/storm/solver/LpMinMaxLinearEquationSolver.cpp

@@ -111,9 +111,9 @@ namespace storm {
         }
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> 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()) {

src/storm/solver/LpMinMaxLinearEquationSolver.h

@@ -21,7 +21,7 @@ namespace storm {
 
             virtual void clearCache() const override;
 
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const override;
             
         private:
             std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;

src/storm/solver/MinMaxLinearEquationSolver.cpp

@@ -136,7 +136,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const&, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const&, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& assumeNoInitialScheduler) const {
             return MinMaxLinearEquationSolverRequirements();
         }
         
@@ -166,11 +166,11 @@ namespace storm {
         }
 
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& assumeNoInitialScheduler) const {
             // Create dummy solver and ask it for requirements.
             std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->create(env);
             solver->setHasUniqueSolution(hasUniqueSolution);
-            return solver->getRequirements(env, direction);
+            return solver->getRequirements(env, direction, assumeNoInitialScheduler);
         }
         
         template<typename ValueType>

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<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> 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<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none, bool const& assumeNoInitialScheduler = false) const;
             void setRequirementsChecked(bool value = true);
             bool isRequirementsCheckedSet() const;
 

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -929,13 +929,15 @@ namespace storm {
         }
         
         template<typename ValueType>
-        LinearEquationSolverRequirements NativeLinearEquationSolver<ValueType>::getRequirements(Environment const& env) const {
+        LinearEquationSolverRequirements NativeLinearEquationSolver<ValueType>::getRequirements(Environment const& env, LinearEquationSolverTask const& task) const {
             LinearEquationSolverRequirements requirements;
-            auto method = getMethod(env, storm::NumberTraits<ValueType>::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<ValueType>::IsExact);
+                if (method == NativeLinearEquationSolverMethod::Power && env.solver().isForceSoundness()) {
+                    requirements.requireBounds();
+                } else if (method == NativeLinearEquationSolverMethod::RationalSearch) {
+                    requirements.requireLowerBounds();
+                }
             }
             return requirements;
         }

src/storm/solver/NativeLinearEquationSolver.h

@@ -37,7 +37,7 @@ namespace storm {
             virtual void multiplyAndReduceGaussSeidel(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* 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;