From 56061c0bfa67b5c292c625800f169336ec709ce3 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 27 Feb 2018 13:26:53 +0100 Subject: [PATCH] Using multiplier in MDP Model checker helpers --- .../prctl/helper/HybridMdpPrctlHelper.cpp | 17 +++++++------ .../prctl/helper/SparseMdpPrctlHelper.cpp | 25 +++++++++---------- src/storm/solver/Multiplier.cpp | 11 +++++++- src/storm/solver/Multiplier.h | 5 ++-- 4 files changed, 34 insertions(+), 24 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 2e14497d5..8a1ef4c9c 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -21,6 +21,7 @@ #include "storm/modelchecker/results/HybridQuantitativeCheckResult.h" #include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/UncheckedRequirementException.h" @@ -309,8 +310,8 @@ namespace storm { // Translate the symbolic matrix/vector to their explicit representations. std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, model.getNondeterminismVariables(), odd, odd); - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitRepresentation.first)); - solver->repeatedMultiply(env, dir, x, &explicitRepresentation.second, stepBound); + auto multiplier = storm::solver::MultiplierFactory().create(env, explicitRepresentation.first); + multiplier->repeatedMultiplyAndReduce(env, dir, x, &explicitRepresentation.second, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd(), maybeStates, odd, x)); @@ -334,9 +335,9 @@ namespace storm { std::vector x = rewardModel.getStateRewardVector().toVector(odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitMatrix)); - solver->repeatedMultiply(env, dir, x, nullptr, stepBound); - + auto multiplier = storm::solver::MultiplierFactory().create(env, explicitMatrix); + multiplier->repeatedMultiplyAndReduce(env, dir, x, nullptr, stepBound); + // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); } @@ -359,9 +360,9 @@ namespace storm { std::pair, std::vector> explicitRepresentation = transitionMatrix.toMatrixVector(totalRewardVector, model.getNondeterminismVariables(), odd, odd); // Perform the matrix-vector multiplication. - std::unique_ptr> solver = linearEquationSolverFactory.create(env, std::move(explicitRepresentation.first)); - solver->repeatedMultiply(env, dir, x, &explicitRepresentation.second, stepBound); - + auto multiplier = storm::solver::MultiplierFactory().create(env, explicitRepresentation.first); + multiplier->repeatedMultiplyAndReduce(env, dir, x, &explicitRepresentation.second, stepBound); + // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); } diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index adaed4627..a589d3491 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -21,6 +21,7 @@ #include "storm/storage/Scheduler.h" #include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/Multiplier.h" #include "storm/solver/LpSolver.h" #include "storm/settings/SettingsManager.h" @@ -75,9 +76,8 @@ namespace storm { // Create the vector with which to multiply. std::vector subresult(maybeStates.getNumberOfSetBits()); - goal.restrictRelevantValues(maybeStates); - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix)); - solver->repeatedMultiply(env, subresult, &b, stepBound); + auto multiplier = storm::solver::MultiplierFactory().create(env, submatrix); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), subresult, &b, stepBound); // Set the values of the resulting vector accordingly. storm::utility::vector::setVectorValues(result, maybeStates, subresult); @@ -272,8 +272,8 @@ namespace storm { std::vector result(transitionMatrix.getRowGroupCount()); storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one()); - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(env, transitionMatrix); - solver->repeatedMultiply(env, dir, result, nullptr, 1); + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->multiplyAndReduce(env, dir, result, nullptr, result); return result; } @@ -812,9 +812,9 @@ namespace storm { // Initialize result to state rewards of the this->getModel(). std::vector result(rewardModel.getStateRewardVector()); - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, transitionMatrix); - solver->repeatedMultiply(env, result, nullptr, stepCount); - + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, nullptr, stepCount); + return result; } @@ -831,8 +831,8 @@ namespace storm { // Initialize result to the zero vector. std::vector result(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, transitionMatrix); - solver->repeatedMultiply(env, result, &totalRewardVector, stepBound); + auto multiplier = storm::solver::MultiplierFactory().create(env, transitionMatrix); + multiplier->repeatedMultiplyAndReduce(env, goal.direction(), result, &totalRewardVector, stepBound); return result; } @@ -1459,12 +1459,11 @@ namespace storm { std::vector x(mecTransitions.getRowGroupCount(), storm::utility::zero()); std::vector xPrime = x; - auto solver = minMaxLinearEquationSolverFactory.create(env, std::move(mecTransitions)); - solver->setCachingEnabled(true); + auto multiplier = storm::solver::MultiplierFactory().create(env, mecTransitions); ValueType maxDiff, minDiff; while (true) { // Compute the obtained rewards for the next step - solver->repeatedMultiply(env, dir, x, &choiceRewards, 1); + multiplier->multiplyAndReduce(env, dir, x, &choiceRewards, x); // update xPrime and check for convergence // to avoid large (and numerically unstable) x-values, we substract a reference value. diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index d5da8654c..e48b29df2 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -24,6 +24,16 @@ namespace storm { void Multiplier::clearCache() const { cachedVector.reset(); } + + template + void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) { + multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices); + } + + template + void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr) { + multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices); + } template void Multiplier::repeatedMultiply(Environment const& env, std::vector& x, std::vector const* b, uint64_t n) const { @@ -49,7 +59,6 @@ namespace storm { return std::make_unique>(matrix); } } - template class Multiplier; template class MultiplierFactory; diff --git a/src/storm/solver/Multiplier.h b/src/storm/solver/Multiplier.h index 78e8e60ad..4356c583e 100644 --- a/src/storm/solver/Multiplier.h +++ b/src/storm/solver/Multiplier.h @@ -61,6 +61,7 @@ namespace storm { * to the number of rows of A. Can be the same as the x vector. * @param choices If given, the choices made in the reduction process are written to this vector. */ + void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const = 0; /*! @@ -77,6 +78,7 @@ namespace storm { * to the number of rows of A. Can be the same as the x vector. * @param choices If given, the choices made in the reduction process are written to this vector. */ + void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr) const; virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr) const = 0; /*! @@ -97,7 +99,6 @@ namespace storm { * so that the resulting vector has the size of number of row groups of A. * * @param dir The direction for the reduction step. - * @param rowGroupIndices A vector storing the row groups over which to reduce. * @param x The input vector with which to multiply the matrix. Its length must be equal * to the number of columns of A. * @param b If non-null, this vector is added after the multiplication. If given, its length must be equal @@ -106,7 +107,7 @@ namespace storm { * to the number of rows of A. * @param n The number of times to perform the multiplication. */ - void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, uint64_t n) const; + void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n) const; /*! * Multiplies the row with the given index with x and adds the given offset