From 3b394a965e4d7bec11f60778f1838b4b52470f15 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 18 Jan 2018 11:43:16 +0100 Subject: [PATCH] some qvi optimizations --- .../IterativeMinMaxLinearEquationSolver.cpp | 55 ++++++++++--------- src/storm/storage/SparseMatrix.cpp | 14 +++++ src/storm/storage/SparseMatrix.h | 6 ++ 3 files changed, 49 insertions(+), 26 deletions(-) diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index d79ed2f35..5e7600feb 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -610,7 +610,10 @@ namespace storm { template class QuickValueIterationHelper { public: - QuickValueIterationHelper(std::vector& x, std::vector& y, bool relative, ValueType const& precision) : x(x), y(y), hasLowerBound(false), hasUpperBound(false), minIndex(0), maxIndex(0), relative(relative), precision(precision) { + QuickValueIterationHelper(std::vector& x, std::vector& y, bool relative, ValueType const& precision, uint64_t sizeOfLargestRowGroup) : x(x), y(y), hasLowerBound(false), hasUpperBound(false), minIndex(0), maxIndex(0), relative(relative), precision(precision) { + xTmp.resize(sizeOfLargestRowGroup); + yTmp.resize(sizeOfLargestRowGroup); + restart(); } @@ -623,45 +626,43 @@ namespace storm { firstIndexViolatingConvergence = 0; } - void setLowerBound(ValueType const& value) { + inline void setLowerBound(ValueType const& value) { hasLowerBound = true; lowerBound = value; - // std::cout << "Lower bound set to " << lowerBound << std::endl; } - void setUpperBound(ValueType const& value) { + inline void setUpperBound(ValueType const& value) { hasUpperBound = true; upperBound = value; - // std::cout << "Upper bound set to " << upperBound << std::endl; } template - bool better(ValueType const& val1, ValueType const& val2) { + inline bool better(ValueType const& val1, ValueType const& val2) { return maximize(dir) ? val1 > val2 : val1 < val2; } template - ValueType& getPrimaryBound() { + inline ValueType& getPrimaryBound() { return maximize(dir) ? upperBound : lowerBound; } template - bool& hasPrimaryBound() { + inline bool& hasPrimaryBound() { return maximize(dir) ? hasUpperBound : hasLowerBound; } template - ValueType& getSecondaryBound() { + inline ValueType& getSecondaryBound() { return maximize(dir) ? lowerBound : upperBound; } template - uint64_t& getPrimaryIndex() { + inline uint64_t& getPrimaryIndex() { return maximize(dir) ? maxIndex : minIndex; } template - uint64_t& getSecondaryIndex() { + inline uint64_t& getSecondaryIndex() { return maximize(dir) ? minIndex : maxIndex; } @@ -732,9 +733,8 @@ namespace storm { ++row; // Only do more work if there are still rows in this row group if (row != groupEnd) { - xTmp.clear(); - yTmp.clear(); ValueType xi, yi; + uint64_t xyTmpIndex = 0; if (hasPrimaryBound()) { ValueType bestValue = xBest + yBest * getPrimaryBound(); for (;row < groupEnd; ++row) { @@ -745,8 +745,9 @@ namespace storm { if (better(currentValue, bestValue)) { if (yBest < yi) { // We need to store the 'old' best value as it might be relevant for the decision value - xTmp.push_back(std::move(xBest)); - yTmp.push_back(std::move(yBest)); + xTmp[xyTmpIndex] = std::move(xBest); + yTmp[xyTmpIndex] = std::move(yBest); + ++xyTmpIndex; } xBest = std::move(xi); yBest = std::move(yi); @@ -757,8 +758,9 @@ namespace storm { xBest = std::move(xi); yBest = std::move(yi); } else { - xTmp.push_back(std::move(xi)); - yTmp.push_back(std::move(yi)); + xTmp[xyTmpIndex] = std::move(xi); + yTmp[xyTmpIndex] = std::move(yi); + ++xyTmpIndex; } } } @@ -767,24 +769,25 @@ namespace storm { multiplyRow(row, A, b[row], xi, yi); // Update the best choice if (yi > yBest || (yi == yBest && better(xi, xBest))) { - xTmp.push_back(std::move(xBest)); - yTmp.push_back(std::move(yBest)); + xTmp[xyTmpIndex] = std::move(xBest); + yTmp[xyTmpIndex] = std::move(yBest); + ++xyTmpIndex; xBest = std::move(xi); yBest = std::move(yi); } else { - xTmp.push_back(std::move(xi)); - yTmp.push_back(std::move(yi)); + xTmp[xyTmpIndex] = std::move(xi); + yTmp[xyTmpIndex] = std::move(yi); + ++xyTmpIndex; } } } // Update the decision value - for (auto xTmpIt = xTmp.begin(), yTmpIt = yTmp.begin(); xTmpIt != xTmp.end(); ++xTmpIt, ++yTmpIt) { - ValueType deltaY = yBest - (*yTmpIt); + for (uint64_t i = 0; i < xyTmpIndex; ++i) { + ValueType deltaY = yBest - yTmp[i]; if (deltaY > storm::utility::zero()) { - ValueType newDecisionValue = (*xTmpIt - xBest) / deltaY; + ValueType newDecisionValue = (xTmp[i] - xBest) / deltaY; if (!hasDecisionValue || better(newDecisionValue, decisionValue)) { - // std::cout << "Updating decision value in Iteration " << iterations << " to " << newDecisionValue << ", where deltaX = " << xTmp[choice] << " - " << *xIt << " = " << (xTmp[choice] - *xIt) << " and deltaY= " << *yIt << " - " << yTmp[choice] << " = " << deltaY << "." << std::endl; decisionValue = std::move(newDecisionValue); hasDecisionValue = true; } @@ -976,7 +979,7 @@ namespace storm { this->auxiliaryRowGroupVector = std::make_unique>(); } - QuickValueIterationHelper helper(x, *this->auxiliaryRowGroupVector, env.solver().minMax().getRelativeTerminationCriterion(), storm::utility::convertNumber(env.solver().minMax().getPrecision())); + QuickValueIterationHelper helper(x, *this->auxiliaryRowGroupVector, env.solver().minMax().getRelativeTerminationCriterion(), storm::utility::convertNumber(env.solver().minMax().getPrecision()), this->A->getSizeOfLargestRowGroup()); // Get the precision uint64_t restartMaxIterations = env.solver().minMax().getQviRestartMaxIterations(); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 36dd5724e..729b85b46 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -579,6 +579,20 @@ namespace storm { return this->getRowGroupIndices()[group + 1] - this->getRowGroupIndices()[group]; } + template + typename SparseMatrix::index_type SparseMatrix::getSizeOfLargestRowGroup() const { + if (this->hasTrivialRowGrouping()) { + return 1; + } + index_type res = 0; + index_type previousGroupStart = 0; + for (auto const& i : rowGroupIndices.get()) { + res = std::max(res, i - previousGroupStart); + previousGroupStart = i; + } + return res; + } + template std::vector::index_type> const& SparseMatrix::getRowGroupIndices() const { // If there is no current row grouping, we need to create it. diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index e07389e5a..e115db443 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -567,6 +567,11 @@ namespace storm { */ index_type getRowGroupSize(index_type group) const; + /*! + * Returns the size of the largest row group of the matrix + */ + index_type getSizeOfLargestRowGroup() const; + /*! * Returns the grouping of rows of this matrix. * @@ -574,6 +579,7 @@ namespace storm { */ std::vector const& getRowGroupIndices() const; + /*! * Sets the row grouping to the given one. * @note It is assumed that the new row grouping is non-trivial.