From 38989315408e9e3394febd61458a55d5090e1578 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 24 Nov 2017 11:27:27 +0100 Subject: [PATCH] Some sanity checks regarding linear equation solver requirements --- .../modelchecker/csl/helper/SparseCtmcCslHelper.cpp | 5 +++++ .../prctl/helper/HybridDtmcPrctlHelper.cpp | 12 ++++++++++-- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 11 ++++++----- 3 files changed, 21 insertions(+), 7 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 1a19fca2c..41b768058 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/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> solver = linearEquationSolverFactory.create(env, std::move(bsccEquationSystem)); @@ -560,6 +563,8 @@ namespace storm { rewardSolution = std::vector(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> solver = linearEquationSolverFactory.create(env, std::move(rewardEquationSystemMatrix)); diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index 189245d0b..280c5aaff 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -62,6 +62,11 @@ namespace storm { storm::dd::Add 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 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> oneStepTargetProbs; auto req = linearEquationSolverFactory.getRequirements(env); req.clearLowerBounds(); - boost::optional> oneStepTargetProbs; if (req.requiresUpperBounds()) { storm::dd::Add targetStatesAsColumn = targetStates.template toAdd(); targetStatesAsColumn = targetStatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs()); @@ -275,9 +281,11 @@ namespace storm { storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); std::vector b = subvector.toVector(odd); - // Create the upper bounds vector if one was requested + // Create the upper bounds vector if one was requested. boost::optional> 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)); } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 13f877bb4..0d0ec5928 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/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 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> solver = storm::solver::configureLinearEquationSolver(env, std::move(goal), linearEquationSolverFactory, std::move(submatrix));