From b698a7cfcb0ffbe394b12848df9261d106da7396 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 19:15:17 +0100 Subject: [PATCH 1/5] native multiplying now supports optdir overrides --- src/storm/solver/NativeMultiplier.cpp | 34 +++--- src/storm/solver/NativeMultiplier.h | 24 ++-- src/storm/storage/SparseMatrix.cpp | 159 +++++++++++++++++++------- src/storm/storage/SparseMatrix.h | 24 ++-- 4 files changed, 157 insertions(+), 84 deletions(-) diff --git a/src/storm/solver/NativeMultiplier.cpp b/src/storm/solver/NativeMultiplier.cpp index 8b13d07cc..26dad0b22 100644 --- a/src/storm/solver/NativeMultiplier.cpp +++ b/src/storm/solver/NativeMultiplier.cpp @@ -60,9 +60,9 @@ namespace storm { this->matrix.multiplyWithVectorForward(x, x, b); } } - + template - void NativeMultiplier::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) const { + void NativeMultiplier::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, storm::storage::BitVector* dirOverride) const { std::vector* target = &result; if (&x == &result) { if (this->cachedVector) { @@ -73,31 +73,31 @@ namespace storm { target = this->cachedVector.get(); } if (parallelize(env)) { - multAddReduceParallel(dir, rowGroupIndices, x, b, *target, choices); + multAddReduceParallel(dir, rowGroupIndices, x, b, *target, choices, dirOverride); } else { - multAddReduce(dir, rowGroupIndices, x, b, *target, choices); + multAddReduce(dir, rowGroupIndices, x, b, *target, choices, dirOverride); } if (&x == &result) { std::swap(result, *this->cachedVector); } } - + template - void NativeMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, bool backwards) const { + void NativeMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { if (backwards) { - this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices); + this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices, dirOverride); } else { - this->matrix.multiplyAndReduceForward(dir, rowGroupIndices, x, b, x, choices); + this->matrix.multiplyAndReduceForward(dir, rowGroupIndices, x, b, x, choices, dirOverride); } } - + template void NativeMultiplier::multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const { for (auto const& entry : this->matrix.getRow(rowIndex)) { value += entry.getValue() * x[entry.getColumn()]; } } - + template void NativeMultiplier::multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const { for (auto const& entry : this->matrix.getRow(rowIndex)) { @@ -110,12 +110,12 @@ namespace storm { void NativeMultiplier::multAdd(std::vector const& x, std::vector const* b, std::vector& result) const { this->matrix.multiplyWithVector(x, result, b); } - + template - void NativeMultiplier::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { - this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices); + void NativeMultiplier::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices, dirOverride); } - + template void NativeMultiplier::multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const { #ifdef STORM_HAVE_INTELTBB @@ -125,11 +125,11 @@ namespace storm { multAdd(x, b, result); #endif } - + template - void NativeMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + void NativeMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { #ifdef STORM_HAVE_INTELTBB - this->matrix.multiplyAndReduceParallel(dir, rowGroupIndices, x, b, result, choices); + this->matrix.multiplyAndReduceParallel(dir, rowGroupIndices, x, b, result, choices, dirOverride); #else STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version."); multAddReduce(dir, rowGroupIndices, x, b, result, choices); diff --git a/src/storm/solver/NativeMultiplier.h b/src/storm/solver/NativeMultiplier.h index 92424f91c..62ae47d07 100644 --- a/src/storm/solver/NativeMultiplier.h +++ b/src/storm/solver/NativeMultiplier.h @@ -9,33 +9,33 @@ namespace storm { template class SparseMatrix; } - + namespace solver { - + template class NativeMultiplier : public Multiplier { public: NativeMultiplier(storm::storage::SparseMatrix const& matrix); virtual ~NativeMultiplier() = default; - + virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const override; virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const override; - 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 override; - virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) const override; + 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, storm::storage::BitVector* dirOverride = nullptr) const override; + virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const override; virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const override; virtual void multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const override; private: bool parallelize(Environment const& env) const; - + void multAdd(std::vector const& x, std::vector const* b, std::vector& result) const; - - void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; - + + void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; + void multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; - + void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; + }; - + } } diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index d89f7a568..84b8fa306 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1753,17 +1753,25 @@ namespace storm { #endif template - void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { - if (dir == OptimizationDirection::Minimize) { - multiplyAndReduceForward>(rowGroupIndices, vector, summand, result, choices); + void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + if(dirOverride && !dirOverride->empty()) { + if (dir == OptimizationDirection::Minimize) { + multiplyAndReduceForward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); + } else { + multiplyAndReduceForward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); + } } else { - multiplyAndReduceForward>(rowGroupIndices, vector, summand, result, choices); + if (dir == OptimizationDirection::Minimize) { + multiplyAndReduceForward, false>(rowGroupIndices, vector, summand, result, choices); + } else { + multiplyAndReduceForward, false>(rowGroupIndices, vector, summand, result, choices); + } } } template - template - void SparseMatrix::multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { + template + void SparseMatrix::multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { Compare compare; auto elementIt = this->begin(); auto rowGroupIt = rowGroupIndices.begin(); @@ -1782,7 +1790,8 @@ namespace storm { uint64_t selectedChoice; uint64_t currentRow = 0; - for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++choiceIt, ++rowGroupIt) { + uint64_t currentRowGroup = 0; + for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++choiceIt, ++rowGroupIt, ++currentRowGroup) { ValueType currentValue = storm::utility::zero(); // Only multiply and reduce if there is at least one row in the group. @@ -1816,10 +1825,19 @@ namespace storm { oldSelectedChoiceValue = newValue; } - if (compare(newValue, currentValue)) { - currentValue = newValue; - if (choices) { - selectedChoice = currentRow - *rowGroupIt; + if(dirOverridden) { + if (dirOverride->get(currentRowGroup) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *rowGroupIt; + } + } + } else { + if (compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *rowGroupIt; + } } } if (summand) { @@ -1829,8 +1847,14 @@ namespace storm { // Finally write value to target vector. *resultIt = currentValue; - if (choices && compare(currentValue, oldSelectedChoiceValue)) { - *choiceIt = selectedChoice; + if(dirOverridden) { + if (choices && dirOverride->get(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } + } else { + if (choices && compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } } } } @@ -1838,23 +1862,31 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const { + void SparseMatrix::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif template - void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { - if (dir == storm::OptimizationDirection::Minimize) { - multiplyAndReduceBackward>(rowGroupIndices, vector, summand, result, choices); + void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + if(dirOverride && !dirOverride->empty()) { + if (dir == storm::OptimizationDirection::Minimize) { + multiplyAndReduceBackward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); + } else { + multiplyAndReduceBackward, true>(rowGroupIndices, vector, summand, result, choices, dirOverride); + } } else { - multiplyAndReduceBackward>(rowGroupIndices, vector, summand, result, choices); + if (dir == storm::OptimizationDirection::Minimize) { + multiplyAndReduceBackward, false>(rowGroupIndices, vector, summand, result, choices); + } else { + multiplyAndReduceBackward, false>(rowGroupIndices, vector, summand, result, choices); + } } } template - template - void SparseMatrix::multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { + template + void SparseMatrix::multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { Compare compare; auto elementIt = this->end() - 1; auto rowGroupIt = rowGroupIndices.end() - 2; @@ -1873,7 +1905,8 @@ namespace storm { uint64_t selectedChoice; uint64_t currentRow = this->getRowCount() - 1; - for (auto resultIt = result.end() - 1, resultIte = result.begin() - 1; resultIt != resultIte; --resultIt, --choiceIt, --rowGroupIt) { + uint64_t currentRowGroup = this->getRowGroupCount() - 2; + for (auto resultIt = result.end() - 1, resultIte = result.begin() - 1; resultIt != resultIte; --resultIt, --choiceIt, --rowGroupIt, --currentRowGroup) { ValueType currentValue = storm::utility::zero(); // Only multiply and reduce if there is at least one row in the group. @@ -1905,18 +1938,33 @@ namespace storm { oldSelectedChoiceValue = newValue; } - if (compare(newValue, currentValue)) { - currentValue = newValue; - if (choices) { - selectedChoice = currentRow - *rowGroupIt; + if(directionOverridden) { + if (dirOverride->get(currentRowGroup) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *rowGroupIt; + } + } + } else { + if (compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *rowGroupIt; + } } } } // Finally write value to target vector. *resultIt = currentValue; - if (choices && compare(currentValue, oldSelectedChoiceValue)) { - *choiceIt = selectedChoice; + if(directionOverridden) { + if (choices && dirOverride->get(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } + } else { + if (choices && compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } } } } @@ -1924,20 +1972,20 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const { + void SparseMatrix::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif #ifdef STORM_HAVE_INTELTBB - template + template class TbbMultAddReduceFunctor { public: typedef typename storm::storage::SparseMatrix::index_type index_type; typedef typename storm::storage::SparseMatrix::value_type value_type; typedef typename storm::storage::SparseMatrix::const_iterator const_iterator; - TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand, std::vector* choices) : rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices) { + TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, std::vector> const& columnsAndEntries, std::vector const& rowIndications, std::vector const& x, std::vector& result, std::vector const* summand, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices), dirOverride(dirOverride) { // Intentionally left empty. } @@ -1964,7 +2012,8 @@ namespace storm { uint64_t selectedChoice; uint64_t currentRow = *groupIt; - for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) { + uint64_t currentRowGroup = *groupIt; + for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt, ++currentRowGroup) { ValueType currentValue = storm::utility::zero(); // Only multiply and reduce if there is at least one row in the group. @@ -1998,18 +2047,33 @@ namespace storm { oldSelectedChoiceValue = newValue; } - if (compare(newValue, currentValue)) { - currentValue = newValue; - if (choices) { - selectedChoice = currentRow - *groupIt; + if(directionOverridden) { + if (dirOverride.get()->get(currentRowGroup) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *groupIt; + } + } + } else { + if (compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *groupIt; + } } } } // Finally write value to target vector. *resultIt = currentValue; - if (choices && compare(currentValue, oldSelectedChoiceValue)) { - *choiceIt = selectedChoice; + if(directionOverridden) { + if (choices && dirOverride.get()->get(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } + } else { + if (choices && compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } } } } @@ -2024,27 +2088,36 @@ namespace storm { std::vector& result; std::vector const* summand; std::vector* choices; + boost::optional dirOverride = boost::none; }; template - void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { - if (dir == storm::OptimizationDirection::Minimize) { - tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices)); + void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + if(dirOverride && !dirOverride->empty()) { + if (dir == storm::OptimizationDirection::Minimize) { + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor, true>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices, dirOverride)); + } else { + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor, true>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices, dirOverride)); + } } else { - tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices)); + if (dir == storm::OptimizationDirection::Minimize) { + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor, false>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices)); + } else { + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor, false>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices)); + } } } #ifdef STORM_HAVE_CARL template<> - void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { + void SparseMatrix::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } #endif #endif template - void SparseMatrix::multiplyAndReduce(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const { + void SparseMatrix::multiplyAndReduce(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { // If the vector and the result are aliases, we need and temporary vector. std::vector* target; diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index ba25a2819..8346e5554 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -907,19 +907,19 @@ namespace storm { * the 'new' choice has a value strictly better (wrt. to the optimization direction) value. * @return The resulting vector the content of the given result vector. */ - void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const; - - void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; - template - void multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices) const; - - void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; - template - void multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; + void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + + void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + template + void multiplyAndReduceForward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* summand, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + + void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + template + void multiplyAndReduceBackward(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; #ifdef STORM_HAVE_INTELTBB - void multiplyAndReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; - template - void multiplyAndReduceParallel(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices) const; + void multiplyAndReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; + template + void multiplyAndReduceParallel(std::vector const& rowGroupIndices, std::vector const& vector, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) const; #endif /*! From 7063928d2fd6ad771d78c485fcbe7a5fecf64fda Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 19:16:54 +0100 Subject: [PATCH 2/5] refactored gmm opt dir overrides --- src/storm/solver/GmmxxMultiplier.cpp | 130 ++++++++++++++++++--------- src/storm/solver/GmmxxMultiplier.h | 32 +++---- 2 files changed, 107 insertions(+), 55 deletions(-) diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index 66ae1249a..e36ce7e74 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -11,6 +11,7 @@ #include "storm/utility/constants.h" #include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/InternalException.h" #include "storm/utility/macros.h" @@ -87,7 +88,7 @@ namespace storm { } template - void GmmxxMultiplier::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) const { + void GmmxxMultiplier::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, storm::storage::BitVector* dirOverride) const { initialize(); std::vector* target = &result; if (&x == &result) { @@ -99,9 +100,9 @@ namespace storm { target = this->cachedVector.get(); } if (parallelize(env)) { - multAddReduceParallel(dir, rowGroupIndices, x, b, *target, choices); + multAddReduceParallel(dir, rowGroupIndices, x, b, *target, choices, dirOverride); } else { - multAddReduceHelper(dir, rowGroupIndices, x, b, *target, choices, false); + multAddReduceHelper(dir, rowGroupIndices, x, b, *target, choices, dirOverride, false); } if (&x == &result) { std::swap(result, *this->cachedVector); @@ -109,9 +110,9 @@ namespace storm { } template - void GmmxxMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, bool backwards) const { + void GmmxxMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { initialize(); - multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, backwards); + multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, dirOverride, backwards); } template @@ -134,25 +135,42 @@ namespace storm { } template - void GmmxxMultiplier::multAddReduceHelper(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, bool backwards) const { + void GmmxxMultiplier::multAddReduceHelper(OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { + bool isOverridden = (dirOverride && !dirOverride->empty()) ? true : false; if (dir == storm::OptimizationDirection::Minimize) { - if (backwards) { - multAddReduceHelper, true>(rowGroupIndices, x, b, result, choices); + if(isOverridden) { + if (backwards) { + multAddReduceHelper, true, true>(rowGroupIndices, x, b, result, choices, dirOverride); + } else { + multAddReduceHelper, false, true>(rowGroupIndices, x, b, result, choices, dirOverride); + } } else { - multAddReduceHelper, false>(rowGroupIndices, x, b, result, choices); + if (backwards) { + multAddReduceHelper, true, false>(rowGroupIndices, x, b, result, choices); + } else { + multAddReduceHelper, false, false>(rowGroupIndices, x, b, result, choices); + } } } else { - if (backwards) { - multAddReduceHelper, true>(rowGroupIndices, x, b, result, choices); + if(isOverridden) { + if (backwards) { + multAddReduceHelper, true, true>(rowGroupIndices, x, b, result, choices, dirOverride); + } else { + multAddReduceHelper, false, true>(rowGroupIndices, x, b, result, choices, dirOverride); + } } else { - multAddReduceHelper, false>(rowGroupIndices, x, b, result, choices); + if (backwards) { + multAddReduceHelper, true, false>(rowGroupIndices, x, b, result, choices); + } else { + multAddReduceHelper, false, false>(rowGroupIndices, x, b, result, choices); + } } } } template - template - void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + template + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { Compare compare; typedef std::vector VectorType; typedef gmm::csr_matrix MatrixType; @@ -169,11 +187,6 @@ namespace storm { choice_it = backwards ? choices->end() - 1 : choices->begin(); } - boost::optional optimizationDirectionOverride; - if(this->getOptimizationDirectionOverride().is_initialized()) { - optimizationDirectionOverride = this->getOptimizationDirectionOverride(); - } - // Variables for correctly tracking choices (only update if new choice is strictly better). ValueType oldSelectedChoiceValue; uint64_t selectedChoice; @@ -228,12 +241,22 @@ namespace storm { } //std::cout << newValue << ", "; //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits::row(itr), x) << " + " << *add_it << "; "); - if(this->isOverridden(currentRowGroup) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { - currentValue = newValue; - if (choices) { - selectedChoice = currentRow - *row_group_it; + if(!directionOverridden) { + if(compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *row_group_it; + } + choiceforprintout = currentRow - *row_group_it; + } + } else { + if(dirOverride->get(currentRowGroup) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *row_group_it; + } + choiceforprintout = currentRow - *row_group_it; } - choiceforprintout = currentRow - *row_group_it; } // move row-based iterators to the next row if (backwards) { @@ -251,8 +274,14 @@ namespace storm { // Finally write value to target vector. *target_it = currentValue; if(choices) { - if(this->isOverridden(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue) ) { - *choice_it = selectedChoice; + if(!directionOverridden) { + if(compare(currentValue, oldSelectedChoiceValue) ) { + *choice_it = selectedChoice; + } + } else { + if(dirOverride->get(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue) ) { + *choice_it = selectedChoice; + } } } } @@ -274,8 +303,8 @@ namespace storm { } template<> - template - void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + template + void GmmxxMultiplier::multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported for this data type."); } @@ -301,7 +330,7 @@ namespace storm { template class TbbMultAddReduceFunctor { public: - TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, gmm::csr_matrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices) { + TbbMultAddReduceFunctor(std::vector const& rowGroupIndices, gmm::csr_matrix const& matrix, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride = nullptr) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices), dirOverride(dirOverride) { // Intentionally left empty. } @@ -321,6 +350,10 @@ namespace storm { if (choices) { choiceIt = choices->begin() + range.begin(); } + bool dirOverridden = false; + if(dirOverride && !dirOverride.get()->empty()) { + dirOverridden = true; + } auto resultIt = result.begin() + range.begin(); @@ -355,19 +388,35 @@ namespace storm { ValueType newValue = b ? *bIt : storm::utility::zero(); newValue += vect_sp(gmm::linalg_traits::row(itr), x); - if (compare(newValue, currentValue)) { - currentValue = newValue; - if (choices) { - selectedChoice = currentRow - *groupIt; + if(!dirOverridden) { + if (compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *groupIt; + } + } + } else { + if (dirOverride.get()->get(*groupIt) ? compare(currentValue, newValue) : compare(newValue, currentValue)) { + currentValue = newValue; + if (choices) { + selectedChoice = currentRow - *groupIt; + } } + } } } // Finally write value to target vector. *resultIt = currentValue; - if (choices && compare(currentValue, oldSelectedChoiceValue)) { - *choiceIt = selectedChoice; + if(!dirOverridden) { + if (choices && compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } + } else { + if (choices && dirOverride.get()->get(*groupIt) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue)) { + *choiceIt = selectedChoice; + } } } } @@ -380,25 +429,26 @@ namespace storm { std::vector const* b; std::vector& result; std::vector* choices; + boost::optional dirOverride = boost::none; }; #endif template - void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { #ifdef STORM_HAVE_INTELTBB if (dir == storm::OptimizationDirection::Minimize) { - tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices)); + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices, dirOverride)); } else { - tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices)); + tbb::parallel_for(tbb::blocked_range(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor>(rowGroupIndices, this->gmmMatrix, x, b, result, choices, dirOverride)); } #else STORM_LOG_WARN("Storm was built without support for Intel TBB, defaulting to sequential version."); - multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices); + multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices, dirOverride); #endif } template<> - void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + void GmmxxMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); } diff --git a/src/storm/solver/GmmxxMultiplier.h b/src/storm/solver/GmmxxMultiplier.h index f0394770b..77050f8aa 100644 --- a/src/storm/solver/GmmxxMultiplier.h +++ b/src/storm/solver/GmmxxMultiplier.h @@ -2,47 +2,49 @@ #include "storm/solver/Multiplier.h" +#include "storm/storage/BitVector.h" + #include "storm/adapters/GmmxxAdapter.h" #include "storm-config.h" namespace storm { - + namespace storage { template class SparseMatrix; } - + namespace solver { - + template class GmmxxMultiplier : public Multiplier { public: GmmxxMultiplier(storm::storage::SparseMatrix const& matrix); virtual ~GmmxxMultiplier() = default; - + virtual void multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const override; virtual void multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b, bool backwards = true) const override; - 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 override; - virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) const override; + 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, storm::storage::BitVector* dirOverride = nullptr) const override; + virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const override; virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const override; virtual void clearCache() const override; - + private: void initialize() const; - + bool parallelize(Environment const& env) const; - + void multAdd(std::vector const& x, std::vector const* b, std::vector& result) const; void multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const; - void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; - void multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, bool backwards = true) const; - - template - void multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; + void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; + void multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const; + + template + void multAddReduceHelper(std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const; mutable gmm::csr_matrix gmmMatrix; }; - + } } From 790c57898cf81059f5d6b159a6916965d54edd53 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 19:17:29 +0100 Subject: [PATCH 3/5] adapted virtual multiplier functions for opt dir overrides --- src/storm/solver/Multiplier.cpp | 26 +++++--------------------- src/storm/solver/Multiplier.h | 27 +++++---------------------- 2 files changed, 10 insertions(+), 43 deletions(-) diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 556a4dfa9..a0533b06d 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -30,13 +30,13 @@ namespace storm { } template - void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { - multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices); + void Multiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices, storm::storage::BitVector* dirOverride) const { + multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices, dirOverride); } template - void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices, bool backwards) const { - multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, backwards); + void Multiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices, storm::storage::BitVector* dirOverride, bool backwards) const { + multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, dirOverride, backwards); } template @@ -55,7 +55,7 @@ namespace storm { } template - void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n) const { + void Multiplier::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, uint64_t n, storm::storage::BitVector* dirOverride) const { storm::utility::ProgressMeasurement progress("multiplications"); progress.setMaxCount(n); progress.startNewMeasurement(0); @@ -74,22 +74,6 @@ namespace storm { multiplyRow(rowIndex, x2, val2); } - template - void Multiplier::setOptimizationDirectionOverride(storm::storage::BitVector const& optDirOverride) { - optimizationDirectionOverride = optDirOverride; - } - - template - boost::optional Multiplier::getOptimizationDirectionOverride() const { - return optimizationDirectionOverride; - } - - template - bool Multiplier::isOverridden(uint_fast64_t const index) const { - if(!optimizationDirectionOverride.is_initialized()) return false; - return optimizationDirectionOverride.get().get(index); - } - template std::unique_ptr> MultiplierFactory::create(Environment const& env, storm::storage::SparseMatrix const& matrix) { auto type = env.solver().multiplier().getType(); diff --git a/src/storm/solver/Multiplier.h b/src/storm/solver/Multiplier.h index acf754e94..7662d355c 100644 --- a/src/storm/solver/Multiplier.h +++ b/src/storm/solver/Multiplier.h @@ -70,8 +70,8 @@ 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; + void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = 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, storm::storage::BitVector* dirOverride = nullptr) const = 0; /*! * Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups @@ -88,8 +88,8 @@ namespace storm { * @param choices If given, the choices made in the reduction process are written to this vector. * @param backwards if true, the iterations will be performed beginning from the last rowgroup and ending at the first rowgroup. */ - void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr, bool backwards = true) 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, bool backwards = true) const = 0; + void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector& x, std::vector const* b, std::vector* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) 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, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const = 0; /*! * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After @@ -117,7 +117,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& 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, storm::storage::BitVector* dirOverride = nullptr) const; /*! * Multiplies the row with the given index with x and adds the result to the provided value @@ -137,26 +137,9 @@ namespace storm { */ virtual void multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const; - /* - * TODO - */ - void setOptimizationDirectionOverride(storm::storage::BitVector const& optimizationDirectionOverride); - - /* - * TODO - */ - boost::optional getOptimizationDirectionOverride() const; - - /* - * TODO - */ - bool isOverridden(uint_fast64_t const index) const; - protected: mutable std::unique_ptr> cachedVector; storm::storage::SparseMatrix const& matrix; - - boost::optional optimizationDirectionOverride = boost::none; }; template From 7c31774678b9caccceb3c077209537b3b9c44706 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 19:19:20 +0100 Subject: [PATCH 4/5] removed residual function calls --- .../helper/infinitehorizon/internal/LraViHelper.cpp | 3 --- .../modelchecker/rpatl/helper/internal/GameViHelper.cpp | 1 - src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp | 5 ----- 3 files changed, 9 deletions(-) diff --git a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp index 239817adc..28ace1d81 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp +++ b/src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp @@ -332,9 +332,6 @@ namespace storm { _TsToIsMultiplier = storm::solver::MultiplierFactory().create(env, _TsToIsTransitions); _IsToTsMultiplier = storm::solver::MultiplierFactory().create(env, _IsToTsTransitions); } - if(env.solver().multiplier().getOptimizationDirectionOverride().is_initialized()) { - _TsMultiplier->setOptimizationDirectionOverride(env.solver().multiplier().getOptimizationDirectionOverride().get()); - } } template diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 4f6fc1e4e..5c9cab92e 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -26,7 +26,6 @@ namespace storm { // -> compute b vector from psiStates // -> clip transitionmatrix and create multiplier _multiplier = storm::solver::MultiplierFactory().create(env, _transitionMatrix); - _multiplier->setOptimizationDirectionOverride(_statesOfCoalition); _x1IsCurrent = false; } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 09bd57726..dbc5e634d 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -415,11 +415,6 @@ namespace storm { this->multiplierA = storm::solver::MultiplierFactory().create(env, *this->A); } - // TODO cleanup - if(env.solver().multiplier().getOptimizationDirectionOverride().is_initialized()) { - multiplierA->setOptimizationDirectionOverride(env.solver().multiplier().getOptimizationDirectionOverride().get()); - } - if (!auxiliaryRowGroupVector) { auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); } From 47bc2ae677d1f984ed1dcd4f481c9b97101c0335 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 29 Jan 2021 19:24:38 +0100 Subject: [PATCH 5/5] removed default parameter --- src/storm/solver/AcyclicMinMaxLinearEquationSolver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/solver/AcyclicMinMaxLinearEquationSolver.cpp b/src/storm/solver/AcyclicMinMaxLinearEquationSolver.cpp index d17e46528..3954c68b5 100644 --- a/src/storm/solver/AcyclicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/AcyclicMinMaxLinearEquationSolver.cpp @@ -83,9 +83,9 @@ namespace storm { choicesPtr = &(this->schedulerChoices.get()); } } - + // Since a topological ordering is guaranteed, we can solve the equations with a single matrix-vector Multiplication step. - this->multiplier->multiplyAndReduceGaussSeidel(env, dir, *xPtr, bPtr, choicesPtr, true); + this->multiplier->multiplyAndReduceGaussSeidel(env, dir, *xPtr, bPtr, choicesPtr); if (rowGroupOrdering) { // Restore the correct input-order for the output vector