Some sanity checks regarding linear equation solver requirements

src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@@ -23,6 +23,7 @@
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/FormatUnsupportedBySolverException.h"
+#include "storm/exceptions/UncheckedRequirementException.h"
 
 namespace storm {
     namespace modelchecker {
@@ -490,6 +491,8 @@ namespace storm {
                     bsccEquationSystem = builder.build();
                     
                     {
+                        // 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.");
                         // 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<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(bsccEquationSystem));
@@ -560,6 +563,8 @@ namespace storm {
                     rewardSolution = std::vector<ValueType>(rewardEquationSystemMatrix.getColumnCount(), one);
                     
                     {
+                        // 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.");
                         // 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<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(rewardEquationSystemMatrix));

src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp

@@ -62,6 +62,11 @@ namespace storm {
                         storm::dd::Add<DdType, ValueType> subvector = submatrix * prob1StatesAsColumn;
                         subvector = subvector.sumAbstract(model.getColumnVariables());
 
+                        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.");
+                        
                         // Check whether we need to create an equation system.
                         bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
                         
@@ -246,9 +251,10 @@ namespace storm {
                         storm::dd::Add<DdType, ValueType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables());
 
                         // Check the requirements of a linear equation solver
+                        // We might need to compute upper reward bounds for which the oneStepTargetProbabilities are needed.
+                        boost::optional<storm::dd::Add<DdType, ValueType>> oneStepTargetProbs;
                         auto req = linearEquationSolverFactory.getRequirements(env);
                         req.clearLowerBounds();
-                        boost::optional<storm::dd::Add<DdType, ValueType>> oneStepTargetProbs;
                         if (req.requiresUpperBounds()) {
                             storm::dd::Add<DdType, ValueType> targetStatesAsColumn = targetStates.template toAdd<ValueType>();
                             targetStatesAsColumn = targetStatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs());
@@ -275,9 +281,11 @@ namespace storm {
                         storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(odd, odd);
                         std::vector<ValueType> b = subvector.toVector(odd);
                         
-                        // Create the upper bounds vector if one was requested
+                        // Create the upper bounds vector if one was requested.
                         boost::optional<std::vector<ValueType>> upperBounds;
                         if (oneStepTargetProbs) {
+                            // FIXME: This will fail if we already converted the matrix to the equation problem format.
+                            STORM_LOG_ASSERT(!convertToEquationSystem, "Upper reward bounds required, but the matrix is in the wrong format for the computation.");
                             upperBounds = computeUpperRewardBounds(explicitSubmatrix, b, oneStepTargetProbs->toVector(odd));
                         }
                         

src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp

@@ -273,11 +273,6 @@ namespace storm {
                         // In this case we have to compute the reward values for the remaining states.
                         // We can eliminate the rows and columns from the original transition probability matrix.
                         storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, convertToEquationSystem);
-                        if (convertToEquationSystem) {
-                            // Converting the matrix from the fixpoint notation to the form needed for the equation
-                            // system. That is, we go from x = A*x + b to (I-A)x = b.
-                            submatrix.convertToEquationSystem();
-                        }
                         
                         // Initialize the x vector with the hint (if available) or with 1 for each element.
                         // This is the initial guess for the iterative solvers.
@@ -300,6 +295,12 @@ namespace storm {
                         }
                         STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver.");
                         
+                        // If necessary, convert the matrix from the fixpoint notation to the form needed for the equation system.
+                        if (convertToEquationSystem) {
+                            // go from x = A*x + b to (I-A)x = b.
+                            submatrix.convertToEquationSystem();
+                        }
+
                         // Create the solver.
                         goal.restrictRelevantValues(maybeStates);
                         std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix));