Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Multiplier.cpp
Go to the documentation of this file.
2
3#include "storm-config.h"
4
6
9
13
15
21
22namespace storm {
23namespace solver {
24
25template<typename ValueType>
27 // Intentionally left empty.
28}
29
30template<typename ValueType>
32 cachedVector.reset();
33}
34
35template<typename ValueType>
36void Multiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x,
37 std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
38 multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices);
39}
40
41template<typename ValueType>
42void Multiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x,
43 std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
44 multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, backwards);
45}
46
47template<typename ValueType>
48void Multiplier<ValueType>::repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
49 storm::utility::ProgressMeasurement progress("multiplications");
50 progress.setMaxCount(n);
51 progress.startNewMeasurement(0);
52 for (uint64_t i = 0; i < n; ++i) {
53 progress.updateProgress(i);
54 multiply(env, x, b, x);
56 STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications.");
57 break;
58 }
59 }
60}
61
62template<typename ValueType>
63void Multiplier<ValueType>::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x,
64 std::vector<ValueType> const* b, uint64_t n) const {
65 storm::utility::ProgressMeasurement progress("multiplications");
66 progress.setMaxCount(n);
67 progress.startNewMeasurement(0);
68 for (uint64_t i = 0; i < n; ++i) {
69 multiplyAndReduce(env, dir, x, b, x);
71 STORM_LOG_WARN("Aborting after " << i << " of " << n << " multiplications");
72 break;
73 }
74 }
75}
76
77template<typename ValueType>
78
79std::vector<ValueType>& Multiplier<ValueType>::provideCachedVector(uint64_t size) const {
80 if (this->cachedVector) {
81 this->cachedVector->resize(size);
82 } else {
83 this->cachedVector = std::make_unique<std::vector<ValueType>>(size);
84 }
85 return *this->cachedVector;
86}
87
88template<typename ValueType>
89std::unique_ptr<Multiplier<ValueType>> MultiplierFactory<ValueType>::create(Environment const& env, storm::storage::SparseMatrix<ValueType> const& matrix) {
90 auto type = env.solver().multiplier().getType();
91
92 // Adjust the type if the ValueType is not supported
93 if (type == MultiplierType::ViOperator && (std::is_same_v<ValueType, storm::RationalFunction> || std::is_same_v<ValueType, storm::Interval>)) {
94 STORM_LOG_INFO("Switching multiplier type from 'vioperator' to 'native' because the given ValueType is not supported by the VI Operator multiplier.");
95 type = MultiplierType::Native;
96 }
97
98 switch (type) {
99 case MultiplierType::ViOperator:
100 if constexpr (std::is_same_v<ValueType, storm::RationalFunction> || std::is_same_v<ValueType, storm::Interval>) {
101 throw storm::exceptions::NotImplementedException() << "VI Operator multiplier not supported with given value type.";
102 }
103 if (matrix.hasTrivialRowGrouping()) {
104 return std::make_unique<ViOperatorMultiplier<ValueType, true>>(matrix);
105 } else {
106 return std::make_unique<ViOperatorMultiplier<ValueType, false>>(matrix);
107 }
108 case MultiplierType::Native:
109 return std::make_unique<NativeMultiplier<ValueType>>(matrix);
110 }
111 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType");
112}
113
114template class Multiplier<double>;
115template class MultiplierFactory<double>;
120template class Multiplier<storm::Interval>;
122
123} // namespace solver
124} // namespace storm
SolverEnvironment & solver()
storm::solver::MultiplierType const & getType() const
MultiplierEnvironment & multiplier()
std::unique_ptr< Multiplier< ValueType > > create(Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix)
std::vector< ValueType > & provideCachedVector(uint64_t size) const
virtual void clearCache() const
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
Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the r...
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
Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups...
void repeatedMultiply(Environment const &env, std::vector< ValueType > &x, std::vector< ValueType > const *b, uint64_t n) const
Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b.
Multiplier(storm::storage::SparseMatrix< ValueType > const &matrix)
void repeatedMultiplyAndReduce(Environment const &env, OptimizationDirection const &dir, 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...
A class that holds a possibly non-square matrix in the compressed row storage format.
bool hasTrivialRowGrouping() const
Retrieves whether the matrix has a trivial row grouping.
A class that provides convenience operations to display run times.
bool updateProgress(uint64_t count)
Updates the progress to the current count and prints it if the delay passed.
void setMaxCount(uint64_t maxCount)
Sets the maximal possible count.
void startNewMeasurement(uint64_t startCount)
Starts a new measurement, dropping all progress information collected so far.
#define STORM_LOG_INFO(message)
Definition logging.h:29
#define STORM_LOG_WARN(message)
Definition logging.h:30
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
LabParser.cpp.
Definition cli.cpp:18