sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge pull request 'Adapting Multipliers for Games' (#8) from gmmxx_refactoring into main 

Reviewed-on: http://git.pranger.xyz/TEMPEST/tempest-devel/pulls/8
main
Stefan Pranger 5 years ago
parent
6559a3554a 47bc2ae677
commit
6a90aa2d1c
12 changed files with 276 additions and 193 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
  2. 1
      src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
  3. 4
      src/storm/solver/AcyclicMinMaxLinearEquationSolver.cpp
  4. 130
      src/storm/solver/GmmxxMultiplier.cpp
  5. 32
      src/storm/solver/GmmxxMultiplier.h
  6. 5
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  7. 26
      src/storm/solver/Multiplier.cpp
  8. 27
      src/storm/solver/Multiplier.h
  9. 34
      src/storm/solver/NativeMultiplier.cpp
  10. 24
      src/storm/solver/NativeMultiplier.h
  11. 159
      src/storm/storage/SparseMatrix.cpp
  12. 24
      src/storm/storage/SparseMatrix.h

3
src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
View File

@ -332,9 +332,6 @@ namespace storm {
_TsToIsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _TsToIsTransitions);
_IsToTsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _IsToTsTransitions);
}
if(env.solver().multiplier().getOptimizationDirectionOverride().is_initialized()) {
_TsMultiplier->setOptimizationDirectionOverride(env.solver().multiplier().getOptimizationDirectionOverride().get());
}
}
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>

1
src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
View File

@ -26,7 +26,6 @@ namespace storm {
// -> compute b vector from psiStates
// -> clip transitionmatrix and create multiplier
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
_multiplier->setOptimizationDirectionOverride(_statesOfCoalition);
_x1IsCurrent = false;
}

4
src/storm/solver/AcyclicMinMaxLinearEquationSolver.cpp
View File

@ -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

130
src/storm/solver/GmmxxMultiplier.cpp
View File

@ -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<typename ValueType>
void GmmxxMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
void GmmxxMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
initialize();
std::vector<ValueType>* 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<typename ValueType>
void GmmxxMultiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
void GmmxxMultiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* 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<typename ValueType>
@ -134,25 +135,42 @@ namespace storm {
}
template<typename ValueType>
void GmmxxMultiplier<ValueType>::multAddReduceHelper(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices, bool backwards) const {
void GmmxxMultiplier<ValueType>::multAddReduceHelper(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices, storm::storage::BitVector* dirOverride, bool backwards) const {
bool isOverridden = (dirOverride && !dirOverride->empty()) ? true : false;
if (dir == storm::OptimizationDirection::Minimize) {
if (backwards) {
multAddReduceHelper<storm::utility::ElementLess<ValueType>, true>(rowGroupIndices, x, b, result, choices);
if(isOverridden) {
if (backwards) {
multAddReduceHelper<storm::utility::ElementLess<ValueType>, true, true>(rowGroupIndices, x, b, result, choices, dirOverride);
} else {
multAddReduceHelper<storm::utility::ElementLess<ValueType>, false, true>(rowGroupIndices, x, b, result, choices, dirOverride);
}
} else {
multAddReduceHelper<storm::utility::ElementLess<ValueType>, false>(rowGroupIndices, x, b, result, choices);
if (backwards) {
multAddReduceHelper<storm::utility::ElementLess<ValueType>, true, false>(rowGroupIndices, x, b, result, choices);
} else {
multAddReduceHelper<storm::utility::ElementLess<ValueType>, false, false>(rowGroupIndices, x, b, result, choices);
}
}
} else {
if (backwards) {
multAddReduceHelper<storm::utility::ElementGreater<ValueType>, true>(rowGroupIndices, x, b, result, choices);
if(isOverridden) {
if (backwards) {
multAddReduceHelper<storm::utility::ElementGreater<ValueType>, true, true>(rowGroupIndices, x, b, result, choices, dirOverride);
} else {
multAddReduceHelper<storm::utility::ElementGreater<ValueType>, false, true>(rowGroupIndices, x, b, result, choices, dirOverride);
}
} else {
multAddReduceHelper<storm::utility::ElementGreater<ValueType>, false>(rowGroupIndices, x, b, result, choices);
if (backwards) {
multAddReduceHelper<storm::utility::ElementGreater<ValueType>, true, false>(rowGroupIndices, x, b, result, choices);
} else {
multAddReduceHelper<storm::utility::ElementGreater<ValueType>, false, false>(rowGroupIndices, x, b, result, choices);
}
}
}
}
template<typename ValueType>
template<typename Compare, bool backwards>
void GmmxxMultiplier<ValueType>::multAddReduceHelper(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
template<typename Compare, bool backwards, bool directionOverridden>
void GmmxxMultiplier<ValueType>::multAddReduceHelper(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices, storm::storage::BitVector* dirOverride) const {
Compare compare;
typedef std::vector<ValueType> VectorType;
typedef gmm::csr_matrix<ValueType> MatrixType;
@ -169,11 +187,6 @@ namespace storm {
choice_it = backwards ? choices->end() - 1 : choices->begin();
}
boost::optional<storm::storage::BitVector> 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<MatrixType>::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<typename Compare, bool backwards>
void GmmxxMultiplier<storm::RationalFunction>::multAddReduceHelper(std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& x, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint64_t>* choices) const {
template<typename Compare, bool backwards, bool directionOverridden>
void GmmxxMultiplier<storm::RationalFunction>::multAddReduceHelper(std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& x, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint64_t>* 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<typename ValueType, typename Compare>
class TbbMultAddReduceFunctor {
public:
TbbMultAddReduceFunctor(std::vector<uint64_t> const& rowGroupIndices, gmm::csr_matrix<ValueType> const& matrix, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices) {
TbbMultAddReduceFunctor(std::vector<uint64_t> const& rowGroupIndices, gmm::csr_matrix<ValueType> const& matrix, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* 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<ValueType>();
newValue += vect_sp(gmm::linalg_traits<MatrixType>::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<ValueType> const* b;
std::vector<ValueType>& result;
std::vector<uint64_t>* choices;
boost::optional<storm::storage::BitVector*> dirOverride = boost::none;
};
#endif
template<typename ValueType>
void GmmxxMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
void GmmxxMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices, storm::storage::BitVector* dirOverride) const {
#ifdef STORM_HAVE_INTELTBB
if (dir == storm::OptimizationDirection::Minimize) {
tbb::parallel_for(tbb::blocked_range<unsigned long>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementLess<ValueType>>(rowGroupIndices, this->gmmMatrix, x, b, result, choices));
tbb::parallel_for(tbb::blocked_range<unsigned long>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementLess<ValueType>>(rowGroupIndices, this->gmmMatrix, x, b, result, choices, dirOverride));
} else {
tbb::parallel_for(tbb::blocked_range<unsigned long>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementGreater<ValueType>>(rowGroupIndices, this->gmmMatrix, x, b, result, choices));
tbb::parallel_for(tbb::blocked_range<unsigned long>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementGreater<ValueType>>(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<storm::RationalFunction>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& x, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint64_t>* choices) const {
void GmmxxMultiplier<storm::RationalFunction>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& x, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint64_t>* choices, storm::storage::BitVector* dirOverride) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
}

32
src/storm/solver/GmmxxMultiplier.h
View File

@ -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<typename ValueType>
class SparseMatrix;
}
namespace solver {
template<typename ValueType>
class GmmxxMultiplier : public Multiplier<ValueType> {
public:
GmmxxMultiplier(storm::storage::SparseMatrix<ValueType> const& matrix);
virtual ~GmmxxMultiplier() = default;
virtual void multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const override;
virtual void multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, bool backwards = true) const override;
virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const override;
virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, bool backwards = true) const override;
virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const override;
virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const override;
virtual void multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> 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<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const;
void multAddParallel(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const;
void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr) const;
void multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr, bool backwards = true) const;
template<typename Compare, bool backwards = true>
void multAddReduceHelper(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr) const;
void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const;
void multAddReduceHelper(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const;
template<typename Compare, bool backwards = true, bool directionOverridden = false>
void multAddReduceHelper(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const;
mutable gmm::csr_matrix<ValueType> gmmMatrix;
};
}
}

5
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
View File

@ -415,11 +415,6 @@ namespace storm {
this->multiplierA = storm::solver::MultiplierFactory<ValueType>().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<std::vector<ValueType>>(this->A->getRowGroupCount());
}

26
src/storm/solver/Multiplier.cpp
View File

@ -30,13 +30,13 @@ namespace storm {
}
template<typename ValueType>
void Multiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices);
void Multiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices, dirOverride);
}
template<typename ValueType>
void Multiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, backwards);
void Multiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride, bool backwards) const {
multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, dirOverride, backwards);
}
template<typename ValueType>
@ -55,7 +55,7 @@ namespace storm {
}
template<typename ValueType>
void Multiplier<ValueType>::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
void Multiplier<ValueType>::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> 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<typename ValueType>
void Multiplier<ValueType>::setOptimizationDirectionOverride(storm::storage::BitVector const& optDirOverride) {
optimizationDirectionOverride = optDirOverride;
}
template<typename ValueType>
boost::optional<storm::storage::BitVector> Multiplier<ValueType>::getOptimizationDirectionOverride() const {
return optimizationDirectionOverride;
}
template<typename ValueType>
bool Multiplier<ValueType>::isOverridden(uint_fast64_t const index) const {
if(!optimizationDirectionOverride.is_initialized()) return false;
return optimizationDirectionOverride.get().get(index);
}
template<typename ValueType>
std::unique_ptr<Multiplier<ValueType>> MultiplierFactory<ValueType>::create(Environment const& env, storm::storage::SparseMatrix<ValueType> const& matrix) {
auto type = env.solver().multiplier().getType();

27
src/storm/solver/Multiplier.h
View File

@ -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<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const;
virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const = 0;
void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const;
virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* 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<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, bool backwards = true) const;
virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, bool backwards = true) const = 0;
void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const;
virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* 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<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const;
void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> 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<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const;
/*
* TODO
*/
void setOptimizationDirectionOverride(storm::storage::BitVector const& optimizationDirectionOverride);
/*
* TODO
*/
boost::optional<storm::storage::BitVector> getOptimizationDirectionOverride() const;
/*
* TODO
*/
bool isOverridden(uint_fast64_t const index) const;
protected:
mutable std::unique_ptr<std::vector<ValueType>> cachedVector;
storm::storage::SparseMatrix<ValueType> const& matrix;
boost::optional<storm::storage::BitVector> optimizationDirectionOverride = boost::none;
};
template<typename ValueType>

34
src/storm/solver/NativeMultiplier.cpp
View File

@ -60,9 +60,9 @@ namespace storm {
this->matrix.multiplyWithVectorForward(x, x, b);
}
}
template<typename ValueType>
void NativeMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
void NativeMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
std::vector<ValueType>* 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<typename ValueType>
void NativeMultiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
void NativeMultiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* 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<typename ValueType>
void NativeMultiplier<ValueType>::multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const {
for (auto const& entry : this->matrix.getRow(rowIndex)) {
value += entry.getValue() * x[entry.getColumn()];
}
}
template<typename ValueType>
void NativeMultiplier<ValueType>::multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const {
for (auto const& entry : this->matrix.getRow(rowIndex)) {
@ -110,12 +110,12 @@ namespace storm {
void NativeMultiplier<ValueType>::multAdd(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
this->matrix.multiplyWithVector(x, result, b);
}
template<typename ValueType>
void NativeMultiplier<ValueType>::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices);
void NativeMultiplier<ValueType>::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices, storm::storage::BitVector* dirOverride) const {
this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices, dirOverride);
}
template<typename ValueType>
void NativeMultiplier<ValueType>::multAddParallel(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
#ifdef STORM_HAVE_INTELTBB
@ -125,11 +125,11 @@ namespace storm {
multAdd(x, b, result);
#endif
}
template<typename ValueType>
void NativeMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
void NativeMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* 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);

24
src/storm/solver/NativeMultiplier.h
View File

@ -9,33 +9,33 @@ namespace storm {
template<typename ValueType>
class SparseMatrix;
}
namespace solver {
template<typename ValueType>
class NativeMultiplier : public Multiplier<ValueType> {
public:
NativeMultiplier(storm::storage::SparseMatrix<ValueType> const& matrix);
virtual ~NativeMultiplier() = default;
virtual void multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const override;
virtual void multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, bool backwards = true) const override;
virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const override;
virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, bool backwards = true) const override;
virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const override;
virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr, bool backwards = true) const override;
virtual void multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const override;
virtual void multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const override;
private:
bool parallelize(Environment const& env) const;
void multAdd(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const;
void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr) const;
void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const;
void multAddParallel(std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const;
void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr) const;
void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices = nullptr, storm::storage::BitVector* dirOverride = nullptr) const;
};
}
}

159
src/storm/storage/SparseMatrix.cpp
View File

@ -1753,17 +1753,25 @@ namespace storm {
#endif
template<typename ValueType>
void SparseMatrix<ValueType>::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
if (dir == OptimizationDirection::Minimize) {
multiplyAndReduceForward<storm::utility::ElementLess<ValueType>>(rowGroupIndices, vector, summand, result, choices);
void SparseMatrix<ValueType>::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
if(dirOverride && !dirOverride->empty()) {
if (dir == OptimizationDirection::Minimize) {
multiplyAndReduceForward<storm::utility::ElementLess<ValueType>, true>(rowGroupIndices, vector, summand, result, choices, dirOverride);
} else {
multiplyAndReduceForward<storm::utility::ElementGreater<ValueType>, true>(rowGroupIndices, vector, summand, result, choices, dirOverride);
}
} else {
multiplyAndReduceForward<storm::utility::ElementGreater<ValueType>>(rowGroupIndices, vector, summand, result, choices);
if (dir == OptimizationDirection::Minimize) {
multiplyAndReduceForward<storm::utility::ElementLess<ValueType>, false>(rowGroupIndices, vector, summand, result, choices);
} else {
multiplyAndReduceForward<storm::utility::ElementGreater<ValueType>, false>(rowGroupIndices, vector, summand, result, choices);
}
}
}
template<typename ValueType>
template<typename Compare>
void SparseMatrix<ValueType>::multiplyAndReduceForward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
template<typename Compare, bool dirOverridden>
void SparseMatrix<ValueType>::multiplyAndReduceForward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* 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<ValueType>();
// 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<storm::RationalFunction>::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& vector, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint_fast64_t>* choices) const {
void SparseMatrix<storm::RationalFunction>::multiplyAndReduceForward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& vector, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
}
#endif
template<typename ValueType>
void SparseMatrix<ValueType>::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
if (dir == storm::OptimizationDirection::Minimize) {
multiplyAndReduceBackward<storm::utility::ElementLess<ValueType>>(rowGroupIndices, vector, summand, result, choices);
void SparseMatrix<ValueType>::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
if(dirOverride && !dirOverride->empty()) {
if (dir == storm::OptimizationDirection::Minimize) {
multiplyAndReduceBackward<storm::utility::ElementLess<ValueType>, true>(rowGroupIndices, vector, summand, result, choices, dirOverride);
} else {
multiplyAndReduceBackward<storm::utility::ElementGreater<ValueType>, true>(rowGroupIndices, vector, summand, result, choices, dirOverride);
}
} else {
multiplyAndReduceBackward<storm::utility::ElementGreater<ValueType>>(rowGroupIndices, vector, summand, result, choices);
if (dir == storm::OptimizationDirection::Minimize) {
multiplyAndReduceBackward<storm::utility::ElementLess<ValueType>, false>(rowGroupIndices, vector, summand, result, choices);
} else {
multiplyAndReduceBackward<storm::utility::ElementGreater<ValueType>, false>(rowGroupIndices, vector, summand, result, choices);
}
}
}
template<typename ValueType>
template<typename Compare>
void SparseMatrix<ValueType>::multiplyAndReduceBackward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
template<typename Compare, bool directionOverridden>
void SparseMatrix<ValueType>::multiplyAndReduceBackward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* 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<ValueType>();
// 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<storm::RationalFunction>::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& vector, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint_fast64_t>* choices) const {
void SparseMatrix<storm::RationalFunction>::multiplyAndReduceBackward(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& vector, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
}
#endif
#ifdef STORM_HAVE_INTELTBB
template <typename ValueType, typename Compare>
template <typename ValueType, typename Compare, bool directionOverridden>
class TbbMultAddReduceFunctor {
public:
typedef typename storm::storage::SparseMatrix<ValueType>::index_type index_type;
typedef typename storm::storage::SparseMatrix<ValueType>::value_type value_type;
typedef typename storm::storage::SparseMatrix<ValueType>::const_iterator const_iterator;
TbbMultAddReduceFunctor(std::vector<uint64_t> const& rowGroupIndices, std::vector<MatrixEntry<index_type, value_type>> const& columnsAndEntries, std::vector<uint64_t> const& rowIndications, std::vector<ValueType> const& x, std::vector<ValueType>& result, std::vector<value_type> const* summand, std::vector<uint_fast64_t>* choices) : rowGroupIndices(rowGroupIndices), columnsAndEntries(columnsAndEntries), rowIndications(rowIndications), x(x), result(result), summand(summand), choices(choices) {
TbbMultAddReduceFunctor(std::vector<uint64_t> const& rowGroupIndices, std::vector<MatrixEntry<index_type, value_type>> const& columnsAndEntries, std::vector<uint64_t> const& rowIndications, std::vector<ValueType> const& x, std::vector<ValueType>& result, std::vector<value_type> const* summand, std::vector<uint_fast64_t>* 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<ValueType>();
// 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<ValueType>& result;
std::vector<value_type> const* summand;
std::vector<uint_fast64_t>* choices;
boost::optional<storm::storage::BitVector*> dirOverride = boost::none;
};
template<typename ValueType>
void SparseMatrix<ValueType>::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
if (dir == storm::OptimizationDirection::Minimize) {
tbb::parallel_for(tbb::blocked_range<index_type>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementLess<ValueType>>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices));
void SparseMatrix<ValueType>::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
if(dirOverride && !dirOverride->empty()) {
if (dir == storm::OptimizationDirection::Minimize) {
tbb::parallel_for(tbb::blocked_range<index_type>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementLess<ValueType>, true>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices, dirOverride));
} else {
tbb::parallel_for(tbb::blocked_range<index_type>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementGreater<ValueType>, true>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices, dirOverride));
}
} else {
tbb::parallel_for(tbb::blocked_range<index_type>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementGreater<ValueType>>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices));
if (dir == storm::OptimizationDirection::Minimize) {
tbb::parallel_for(tbb::blocked_range<index_type>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementLess<ValueType>, false>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices));
} else {
tbb::parallel_for(tbb::blocked_range<index_type>(0, rowGroupIndices.size() - 1, 100), TbbMultAddReduceFunctor<ValueType, storm::utility::ElementGreater<ValueType>, false>(rowGroupIndices, columnsAndValues, rowIndications, vector, result, summand, choices));
}
}
}
#ifdef STORM_HAVE_CARL
template<>
void SparseMatrix<storm::RationalFunction>::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& vector, std::vector<storm::RationalFunction> const* summand, std::vector<storm::RationalFunction>& result, std::vector<uint_fast64_t>* choices) const {
void SparseMatrix<storm::RationalFunction>::multiplyAndReduceParallel(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& vector, std::vector<storm::RationalFunction> const* summand, std::vector<storm::RationalFunction>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
}
#endif
#endif
template<typename ValueType>
void SparseMatrix<ValueType>::multiplyAndReduce(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
void SparseMatrix<ValueType>::multiplyAndReduce(OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride) const {
// If the vector and the result are aliases, we need and temporary vector.
std::vector<ValueType>* target;

24
src/storm/storage/SparseMatrix.h
View File

@ -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<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const;
void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const;
template<typename Compare>
void multiplyAndReduceForward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const;
void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const;
template<typename Compare>
void multiplyAndReduceBackward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const;
void multiplyAndReduce(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const;
void multiplyAndReduceForward(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const;
template<typename Compare, bool directionOverridden>
void multiplyAndReduceForward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* summand, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const;
void multiplyAndReduceBackward(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const;
template<typename Compare, bool directionOverridden>
void multiplyAndReduceBackward(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const;
#ifdef STORM_HAVE_INTELTBB
void multiplyAndReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const;
template<typename Compare>
void multiplyAndReduceParallel(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const;
void multiplyAndReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const;
template<typename Compare, bool directionOverridden>
void multiplyAndReduceParallel(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& vector, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices, storm::storage::BitVector* dirOverride = nullptr) const;
#endif
/*!

Write Preview
Loading…
Cancel
Save