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

added opt dir override bitvector to multiplier 

This is mainly used by the SMG model checker to override row group
optimization directions.
tempestpy_adaptions
Stefan Pranger 4 years ago
parent
972df05683
commit
7abc84449b
4 changed files with 82 additions and 41 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. 20
      src/storm/environment/solver/MultiplierEnvironment.cpp
  2. 18
      src/storm/environment/solver/MultiplierEnvironment.h
  3. 34
      src/storm/solver/Multiplier.cpp
  4. 51
      src/storm/solver/Multiplier.h

20
src/storm/environment/solver/MultiplierEnvironment.cpp
View File

@ -6,28 +6,36 @@
#include "storm/utility/macros.h"
namespace storm {
MultiplierEnvironment::MultiplierEnvironment() {
auto const& multiplierSettings = storm::settings::getModule<storm::settings::modules::MultiplierSettings>();
type = multiplierSettings.getMultiplierType();
typeSetFromDefault = multiplierSettings.isMultiplierTypeSetFromDefaultValue();
}
MultiplierEnvironment::~MultiplierEnvironment() {
// Intentionally left empty
}
storm::solver::MultiplierType const& MultiplierEnvironment::getType() const {
return type;
}
bool const& MultiplierEnvironment::isTypeSetFromDefault() const {
return typeSetFromDefault;
}
void MultiplierEnvironment::setType(storm::solver::MultiplierType value, bool isSetFromDefault) {
type = value;
typeSetFromDefault = isSetFromDefault;
}
void MultiplierEnvironment::setOptimizationDirectionOverride(storm::storage::BitVector optDirOverride) {
optimizationDirectionOverride = optDirOverride;
}
boost::optional<storm::storage::BitVector> const& MultiplierEnvironment::getOptimizationDirectionOverride() const {
return optimizationDirectionOverride;
}
}

18
src/storm/environment/solver/MultiplierEnvironment.h
View File

@ -1,23 +1,31 @@
#pragma once
#include <boost/optional.hpp>
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/solver/SolverSelectionOptions.h"
#include "storm/storage/BitVector.h"
namespace storm {
class MultiplierEnvironment {
public:
MultiplierEnvironment();
~MultiplierEnvironment();
storm::solver::MultiplierType const& getType() const;
bool const& isTypeSetFromDefault() const;
void setType(storm::solver::MultiplierType value, bool isSetFromDefault = false);
void setOptimizationDirectionOverride(storm::storage::BitVector optimizationDirectionOverride);
boost::optional<storm::storage::BitVector> const& getOptimizationDirectionOverride() const;
private:
storm::solver::MultiplierType type;
bool typeSetFromDefault;
boost::optional<storm::storage::BitVector> optimizationDirectionOverride = boost::none;
};
}

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

@ -18,17 +18,17 @@
namespace storm {
namespace solver {
template<typename ValueType>
Multiplier<ValueType>::Multiplier(storm::storage::SparseMatrix<ValueType> const& matrix) : matrix(matrix) {
// Intentionally left empty.
}
template<typename ValueType>
void Multiplier<ValueType>::clearCache() const {
cachedVector.reset();
}
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);
@ -38,7 +38,7 @@ namespace storm {
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);
}
template<typename ValueType>
void Multiplier<ValueType>::repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
storm::utility::ProgressMeasurement progress("multiplications");
@ -53,7 +53,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 {
storm::utility::ProgressMeasurement progress("multiplications");
@ -67,17 +67,27 @@ namespace storm {
}
}
}
template<typename ValueType>
void Multiplier<ValueType>::multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const {
multiplyRow(rowIndex, x1, val1);
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>
std::unique_ptr<Multiplier<ValueType>> MultiplierFactory<ValueType>::create(Environment const& env, storm::storage::SparseMatrix<ValueType> const& matrix) {
auto type = env.solver().multiplier().getType();
// Adjust the multiplier type if an eqsolver was specified but not a multiplier
if (!env.solver().isLinearEquationSolverTypeSetFromDefaultValue() && env.solver().multiplier().isTypeSetFromDefault()) {
bool changed = false;
@ -90,7 +100,7 @@ namespace storm {
}
STORM_LOG_INFO_COND(!changed, "Selecting '" + toString(type) + "' as the multiplier type to match the selected equation solver. If you want to override this, please explicitly specify a different multiplier type.");
}
switch (type) {
case MultiplierType::Gmmxx:
return std::make_unique<GmmxxMultiplier<ValueType>>(matrix);
@ -99,16 +109,16 @@ namespace storm {
}
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType");
}
template class Multiplier<double>;
template class MultiplierFactory<double>;
#ifdef STORM_HAVE_CARL
template class Multiplier<storm::RationalNumber>;
template class MultiplierFactory<storm::RationalNumber>;
template class Multiplier<storm::RationalFunction>;
template class MultiplierFactory<storm::RationalFunction>;
#endif
}
}

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

@ -2,34 +2,37 @@
#include <vector>
#include <memory>
#include <boost/optional.hpp>
#include "storm/storage/BitVector.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/solver/MultiplicationStyle.h"
namespace storm {
class Environment;
namespace storage {
template<typename ValueType>
class SparseMatrix;
}
namespace solver {
template<typename ValueType>
class Multiplier {
public:
Multiplier(storm::storage::SparseMatrix<ValueType> const& matrix);
virtual ~Multiplier() = default;
/*
* Clears the currently cached data of this multiplier in order to free some memory.
*/
virtual void clearCache() const;
/*!
* Performs a matrix-vector multiplication x' = A*x + b.
*
@ -41,7 +44,7 @@ namespace storm {
* to the number of rows of A. Can be the same as the x vector.
*/
virtual void multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const = 0;
/*!
* Performs a matrix-vector multiplication in gauss-seidel style.
*
@ -52,7 +55,7 @@ namespace storm {
* @param backwards if true, the iterations will be performed beginning from the last row and ending at the first row.
*/
virtual void multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, bool backwards = true) const = 0;
/*!
* Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups
* so that the resulting vector has the size of number of row groups of A.
@ -69,7 +72,7 @@ namespace storm {
*/
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;
/*!
* Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups
* so that the resulting vector has the size of number of row groups of A.
@ -87,7 +90,7 @@ namespace storm {
*/
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;
/*!
* Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After
* performing the necessary multiplications, the result is written to the input vector x. Note that the
@ -100,7 +103,7 @@ namespace storm {
* @param n The number of times to perform the multiplication.
*/
void repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const;
/*!
* Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups
* so that the resulting vector has the size of number of row groups of A.
@ -115,7 +118,7 @@ namespace storm {
* @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;
/*!
* Multiplies the row with the given index with x and adds the result to the provided value
* @param rowIndex The index of the considered row
@ -123,7 +126,7 @@ namespace storm {
* @param value The multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix.
*/
virtual void multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const = 0;
/*!
* Multiplies the row with the given index with x1 and x2 and adds the given offset o1 and o2, respectively
* @param rowIndex The index of the considered row
@ -133,12 +136,24 @@ namespace storm {
* @param val2 The second multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix.
*/
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;
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>
class MultiplierFactory {
public:
@ -147,6 +162,6 @@ namespace storm {
std::unique_ptr<Multiplier<ValueType>> create(Environment const& env, storm::storage::SparseMatrix<ValueType> const& matrix);
};
}
}
Write Preview
Loading…
Cancel
Save