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

removed multiplication support from minmax equation solvers. Also removed Factories.

tempestpy_adaptions
TimQu 7 years ago
parent
b7bac59ae0
commit
64ba34a397
11 changed files with 25 additions and 350 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. 36
      src/storm/solver/LpMinMaxLinearEquationSolver.cpp
  2. 21
      src/storm/solver/LpMinMaxLinearEquationSolver.h
  3. 10
      src/storm/solver/MinMaxLinearEquationSolver.cpp
  4. 26
      src/storm/solver/MinMaxLinearEquationSolver.h
  5. 114
      src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
  6. 61
      src/storm/solver/StandardMinMaxLinearEquationSolver.h
  7. 19
      src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp
  8. 2
      src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.h
  9. 3
      src/storm/solver/TopologicalLinearEquationSolver.h
  10. 57
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
  11. 26
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.h

36
src/storm/solver/LpMinMaxLinearEquationSolver.cpp
View File

@ -10,17 +10,17 @@ namespace storm {
namespace solver {
template<typename ValueType>
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) {
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty.
}
template<typename ValueType>
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(A, std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) {
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(A), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty.
}
template<typename ValueType>
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(std::move(A), std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) {
LpMinMaxLinearEquationSolver<ValueType>::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver<ValueType>(std::move(A)), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty.
}
@ -113,7 +113,7 @@ namespace storm {
template<typename ValueType>
MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& hasInitialScheduler) const {
MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements(env, LinearEquationSolverTask::Multiply));
MinMaxLinearEquationSolverRequirements requirements;
// In case we need to retrieve a scheduler, the solution has to be unique
if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) {
@ -127,38 +127,10 @@ namespace storm {
return requirements;
}
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory<ValueType>(), lpSolverFactory(std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>()) {
// Intentionally left empty
}
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory<ValueType>(), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty
}
template<typename ValueType>
LpMinMaxLinearEquationSolverFactory<ValueType>::LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory) : StandardMinMaxLinearEquationSolverFactory<ValueType>(std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) {
// Intentionally left empty
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> LpMinMaxLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
STORM_LOG_THROW(env.solver().minMax().getMethod() == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidEnvironmentException, "This min max solver does not support the selected technique.");
STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized.");
STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized.");
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone());
result->setRequirementsChecked(this->isRequirementsCheckedSet());
return result;
}
template class LpMinMaxLinearEquationSolver<double>;
template class LpMinMaxLinearEquationSolverFactory<double>;
#ifdef STORM_HAVE_CARL
template class LpMinMaxLinearEquationSolver<storm::RationalNumber>;
template class LpMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
#endif
}
}

21
src/storm/solver/LpMinMaxLinearEquationSolver.h
View File

@ -13,9 +13,9 @@ namespace storm {
template<typename ValueType>
class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver<ValueType> {
public:
LpMinMaxLinearEquationSolver(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
LpMinMaxLinearEquationSolver(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
virtual bool internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
@ -27,20 +27,5 @@ namespace storm {
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
};
template<typename ValueType>
class LpMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory<ValueType> {
public:
LpMinMaxLinearEquationSolverFactory();
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory);
// Make the other create methods visible.
using MinMaxLinearEquationSolverFactory<ValueType>::create;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(Environment const& env) const override;
private:
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
};
}
}

10
src/storm/solver/MinMaxLinearEquationSolver.cpp
View File

@ -40,12 +40,6 @@ namespace storm {
solveEquations(env, convert(this->direction), x, b);
}
template<typename ValueType>
void MinMaxLinearEquationSolver<ValueType>::repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType>* b, uint_fast64_t n) const {
STORM_LOG_THROW(isSet(this->direction), storm::exceptions::IllegalFunctionCallException, "Optimization direction not set.");
return repeatedMultiply(env, convert(this->direction), x, b, n);
}
template<typename ValueType>
void MinMaxLinearEquationSolver<ValueType>::setOptimizationDirection(OptimizationDirection d) {
direction = convert(d);
@ -204,7 +198,7 @@ namespace storm {
} else if (method == MinMaxMethod::TopologicalCuda) {
result = std::make_unique<TopologicalCudaMinMaxLinearEquationSolver<ValueType>>();
} else if (method == MinMaxMethod::LinearProgramming) {
result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>(), std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>());
result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
@ -219,7 +213,7 @@ namespace storm {
if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration) {
result = std::make_unique<IterativeMinMaxLinearEquationSolver<storm::RationalNumber>>(std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>());
} else if (method == MinMaxMethod::LinearProgramming) {
result = std::make_unique<LpMinMaxLinearEquationSolver<storm::RationalNumber>>(std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>(), std::make_unique<storm::utility::solver::LpSolverFactory<storm::RationalNumber>>());
result = std::make_unique<LpMinMaxLinearEquationSolver<storm::RationalNumber>>(std::make_unique<storm::utility::solver::LpSolverFactory<storm::RationalNumber>>());
} else if (method == MinMaxMethod::Topological) {
result = std::make_unique<TopologicalMinMaxLinearEquationSolver<storm::RationalNumber>>();
} else {

26
src/storm/solver/MinMaxLinearEquationSolver.h
View File

@ -60,32 +60,6 @@ namespace storm {
*/
void solveEquations(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
/*!
* Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes
* x[i+1] = min/max(A*x[i] + b) until x[n], where x[0] = x. After each multiplication and addition, the
* minimal/maximal value out of each row group is selected to reduce the resulting vector to obtain the
* vector for the next iteration. Note that the matrix A has to be given upon construction time of the
* solver object.
*
* @param d For minimum, all the value of a group of rows is the taken as the minimum over all rows and as
* the maximum otherwise.
* @param x The initial vector that is to be multiplied with the matrix. This is also the output parameter,
* i.e. after the method returns, this vector will contain the computed values.
* @param b If not null, this vector is added after each multiplication.
* @param n Specifies the number of iterations the matrix-vector multiplication is performed.
* @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this
* vector must be equal to the number of rows of A.
* @return The result of the repeated matrix-vector multiplication as the content of the vector x.
*/
virtual void repeatedMultiply(Environment const& env, OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1) const = 0;
/*!
* Behaves the same as the other variant of <code>multiply</code>, with the
* distinction that instead of providing the optimization direction as an argument, the internally set
* optimization direction is used. Note: this method can only be called after setting the optimization direction.
*/
virtual void repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType>* b , uint_fast64_t n) const;
/*!
* Sets an optimization direction to use for calls to methods that do not explicitly provide one.
*/

114
src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
View File

@ -18,17 +18,17 @@ namespace storm {
namespace solver {
template<typename ValueType>
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), A(nullptr) {
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver() : A(nullptr) {
// Intentionally left empty.
}
template<typename ValueType>
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(&A) {
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : localA(nullptr), A(&A) {
// Intentionally left empty.
}
template<typename ValueType>
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A))), A(localA.get()) {
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A) : localA(std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A))), A(localA.get()) {
// Intentionally left empty.
}
@ -36,124 +36,20 @@ namespace storm {
void StandardMinMaxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
this->localA = nullptr;
this->A = &matrix;
clearCache();
this->clearCache();
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType>&& matrix) {
this->localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(matrix));
this->A = this->localA.get();
clearCache();
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::repeatedMultiply(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
if (!linEqSolverA) {
linEqSolverA = linearEquationSolverFactory->create(env, *A, LinearEquationSolverTask::Multiply);
linEqSolverA->setCachingEnabled(true);
}
if (!auxiliaryRowGroupVector) {
auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
}
this->startMeasureProgress();
for (uint64_t i = 0; i < n; ++i) {
linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, b, *auxiliaryRowGroupVector);
std::swap(x, *auxiliaryRowGroupVector);
// Potentially show progress.
this->showProgressIterative(i, n);
}
if (!this->isCachingEnabled()) {
clearCache();
}
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::clearCache() const {
linEqSolverA.reset();
auxiliaryRowVector.reset();
MinMaxLinearEquationSolver<ValueType>::clearCache();
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverFactory<ValueType>::StandardMinMaxLinearEquationSolverFactory() : MinMaxLinearEquationSolverFactory<ValueType>(), linearEquationSolverFactory(std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>()) {
// Intentionally left empty.
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverFactory<ValueType>::StandardMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : MinMaxLinearEquationSolverFactory<ValueType>(), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) {
// Intentionally left empty.
}
template<typename ValueType>
StandardMinMaxLinearEquationSolverFactory<ValueType>::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType) : MinMaxLinearEquationSolverFactory<ValueType>() {
switch (solverType) {
case EquationSolverType::Gmmxx: linearEquationSolverFactory = std::make_unique<GmmxxLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique<EigenLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Native: linearEquationSolverFactory = std::make_unique<NativeLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique<EliminationLinearEquationSolverFactory<ValueType>>(); break;
case EquationSolverType::Topological: linearEquationSolverFactory = std::make_unique<TopologicalLinearEquationSolverFactory<ValueType>>(); break;
}
}
template<>
StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType) : MinMaxLinearEquationSolverFactory<storm::RationalNumber>() {
switch (solverType) {
case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique<EigenLinearEquationSolverFactory<storm::RationalNumber>>(); break;
case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique<EliminationLinearEquationSolverFactory<storm::RationalNumber>>(); break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported equation solver for this data type.");
}
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> StandardMinMaxLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result;
auto method = env.solver().minMax().getMethod();
if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::RationalSearch || method == MinMaxMethod::IntervalIteration || method == MinMaxMethod::SoundValueIteration) {
result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(this->linearEquationSolverFactory->clone());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The selected min max method is not supported by this solver.");
}
result->setRequirementsChecked(this->isRequirementsCheckedSet());
return result;
}
template<typename ValueType>
GmmxxMinMaxLinearEquationSolverFactory<ValueType>::GmmxxMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory<ValueType>(EquationSolverType::Gmmxx) {
// Intentionally left empty.
}
template<typename ValueType>
EigenMinMaxLinearEquationSolverFactory<ValueType>::EigenMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory<ValueType>(EquationSolverType::Eigen) {
// Intentionally left empty.
}
template<typename ValueType>
NativeMinMaxLinearEquationSolverFactory<ValueType>::NativeMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory<ValueType>(EquationSolverType::Native) {
// Intentionally left empty.
}
template<typename ValueType>
EliminationMinMaxLinearEquationSolverFactory<ValueType>::EliminationMinMaxLinearEquationSolverFactory() : StandardMinMaxLinearEquationSolverFactory<ValueType>(EquationSolverType::Elimination) {
// Intentionally left empty.
this->clearCache();
}
template class StandardMinMaxLinearEquationSolver<double>;
template class StandardMinMaxLinearEquationSolverFactory<double>;
template class GmmxxMinMaxLinearEquationSolverFactory<double>;
template class EigenMinMaxLinearEquationSolverFactory<double>;
template class NativeMinMaxLinearEquationSolverFactory<double>;
template class EliminationMinMaxLinearEquationSolverFactory<double>;
#ifdef STORM_HAVE_CARL
template class StandardMinMaxLinearEquationSolver<storm::RationalNumber>;
template class StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
template class EigenMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
template class EliminationMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
#endif
}
}

61
src/storm/solver/StandardMinMaxLinearEquationSolver.h
View File

@ -12,29 +12,17 @@ namespace storm {
template<typename ValueType>
class StandardMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver<ValueType> {
public:
StandardMinMaxLinearEquationSolver(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
StandardMinMaxLinearEquationSolver();
explicit StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A);
explicit StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A);
virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) override;
virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& matrix) override;
virtual ~StandardMinMaxLinearEquationSolver() = default;
virtual void repeatedMultiply(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const override;
virtual void clearCache() const override;
protected:
// possibly cached data
mutable std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linEqSolverA;
mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowVector; // A.rowCount() entries
mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowGroupVector; // A.rowCount() entries
/// The factory used to obtain linear equation solvers.
std::unique_ptr<LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;
// If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted
// when the solver is destructed.
std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localA;
@ -44,48 +32,5 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> const* A;
};
template<typename ValueType>
class StandardMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> {
public:
StandardMinMaxLinearEquationSolverFactory();
StandardMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType);
// Make the other create methods visible.
using MinMaxLinearEquationSolverFactory<ValueType>::create;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(Environment const& env) const override;
protected:
std::unique_ptr<LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;
private:
void createLinearEquationSolverFactory() const;
};
template<typename ValueType>
class GmmxxMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory<ValueType> {
public:
GmmxxMinMaxLinearEquationSolverFactory();
};
template<typename ValueType>
class EigenMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory<ValueType> {
public:
EigenMinMaxLinearEquationSolverFactory();
};
template<typename ValueType>
class NativeMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory<ValueType> {
public:
NativeMinMaxLinearEquationSolverFactory();
};
template<typename ValueType>
class EliminationMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory<ValueType> {
public:
EliminationMinMaxLinearEquationSolverFactory();
};
}
}

19
src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.cpp
View File

@ -447,25 +447,6 @@ namespace storm {
return result;
}
template<typename ValueType>
void TopologicalCudaMinMaxLinearEquationSolver<ValueType>::repeatedMultiply(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
std::unique_ptr<std::vector<ValueType>> multiplyResult = std::make_unique<std::vector<ValueType>>(this->A->getRowCount());
// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
for (uint_fast64_t i = 0; i < n; ++i) {
this->A->multiplyWithVector(x, *multiplyResult);
// Add b if it is non-null.
if (b != nullptr) {
storm::utility::vector::addVectors(*multiplyResult, *b, *multiplyResult);
}
// Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost
// element of the min/max operator stack.
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A->getRowGroupIndices());
}
}
template<typename ValueType>
TopologicalCudaMinMaxLinearEquationSolverFactory<ValueType>::TopologicalCudaMinMaxLinearEquationSolverFactory(bool trackScheduler) {
// Intentionally left empty.

2
src/storm/solver/TopologicalCudaMinMaxLinearEquationSolver.h
View File

@ -39,8 +39,6 @@ namespace storm {
virtual bool internalSolveEquations(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void repeatedMultiply(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const override;
private:
storm::storage::SparseMatrix<ValueType> const* A;
std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localA;

3
src/storm/solver/TopologicalLinearEquationSolver.h
View File

@ -56,9 +56,6 @@ namespace storm {
// the pointer refers to localA.
storm::storage::SparseMatrix<ValueType> const* A;
// An object to dispatch all multiplication operations.
NativeMultiplier<ValueType> multiplier;
// cached auxiliary data
mutable std::unique_ptr<storm::storage::StronglyConnectedComponentDecomposition<ValueType>> sortedSccDecomposition;
mutable boost::optional<uint64_t> longestSccChainSize;

57
src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
View File

@ -14,32 +14,18 @@ namespace storm {
namespace solver {
template<typename ValueType>
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver() : localA(nullptr), A(nullptr) {
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver() {
// Intentionally left empty.
}
template<typename ValueType>
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : localA(nullptr), A(nullptr) {
this->setMatrix(A);
}
template<typename ValueType>
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A) : localA(nullptr), A(nullptr) {
this->setMatrix(std::move(A));
}
template<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& A) {
localA.reset();
this->A = &A;
clearCache();
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A) : StandardMinMaxLinearEquationSolver<ValueType>(A) {
// Intentionally left empty.
}
template<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType>&& A) {
localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(A));
this->A = localA.get();
clearCache();
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A) : StandardMinMaxLinearEquationSolver<ValueType>(std::move(A)) {
// Intentionally left empty.
}
template<typename ValueType>
@ -59,12 +45,6 @@ namespace storm {
STORM_LOG_ASSERT(x.size() == this->A->getRowGroupCount(), "Provided x-vector has invalid size.");
STORM_LOG_ASSERT(b.size() == this->A->getRowCount(), "Provided b-vector has invalid size.");
//std::cout << "Solving equation system with fixpoint characterization " << std::endl;
//std::cout << *this->A << std::endl;
//std::cout << storm::utility::vector::toString(b) << std::endl;
//std::cout << "Initial solution vector: " << std::endl;
//std::cout << storm::utility::vector::toString(x) << std::endl;
// For sound computations we need to increase the precision in each SCC
bool needAdaptPrecision = env.solver().isForceSoundness();
@ -307,24 +287,6 @@ namespace storm {
return res;
}
template<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::repeatedMultiply(Environment const& env, OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env);
// Set up the SCC solver
if (!this->sccSolver) {
this->sccSolver = GeneralMinMaxLinearEquationSolverFactory<ValueType>().create(sccSolverEnvironment);
this->sccSolver->setCachingEnabled(true);
}
this->sccSolver->setMatrix(*this->A);
this->sccSolver->repeatedMultiply(sccSolverEnvironment, d, x, b, n);
if (!this->isCachingEnabled()) {
clearCache();
}
}
template<typename ValueType>
MinMaxLinearEquationSolverRequirements TopologicalMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& hasInitialScheduler) const {
// Return the requirements of the underlying solver
@ -337,21 +299,14 @@ namespace storm {
longestSccChainSize = boost::none;
sccSolver.reset();
auxiliaryRowGroupVector.reset();
MinMaxLinearEquationSolver<ValueType>::clearCache();
}
template<typename ValueType>
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> TopologicalMinMaxLinearEquationSolverFactory<ValueType>::create(Environment const& env) const {
return std::make_unique<storm::solver::TopologicalMinMaxLinearEquationSolver<ValueType>>();
StandardMinMaxLinearEquationSolver<ValueType>::clearCache();
}
// Explicitly instantiate the min max linear equation solver.
template class TopologicalMinMaxLinearEquationSolver<double>;
template class TopologicalMinMaxLinearEquationSolverFactory<double>;
#ifdef STORM_HAVE_CARL
template class TopologicalMinMaxLinearEquationSolver<storm::RationalNumber>;
template class TopologicalMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
#endif
}
}

26
src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
View File

@ -1,6 +1,6 @@
#pragma once
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
#include "storm/solver/SolverSelectionOptions.h"
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
@ -12,18 +12,14 @@ namespace storm {
namespace solver {
template<typename ValueType>
class TopologicalMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver<ValueType> {
class TopologicalMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver<ValueType> {
public:
TopologicalMinMaxLinearEquationSolver();
TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A);
TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A);
virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& A) override;
virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& A) override;
virtual void clearCache() const override;
virtual void repeatedMultiply(Environment const& env, OptimizationDirection d, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1) const override;
virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none, bool const& hasInitialScheduler = false) const override ;
protected:
@ -44,29 +40,11 @@ namespace storm {
// ... for the remaining cases (1 < scc.size() < x.size())
bool solveScc(storm::Environment const& sccSolverEnvironment, OptimizationDirection d, storm::storage::BitVector const& sccRowGroups, storm::storage::BitVector const& sccRows, std::vector<ValueType>& globalX, std::vector<ValueType> const& globalB) const;
// If the solver takes posession of the matrix, we store the moved matrix in this member, so it gets deleted
// when the solver is destructed.
std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localA;
// A pointer to the original sparse matrix given to this solver. If the solver takes posession of the matrix
// the pointer refers to localA.
storm::storage::SparseMatrix<ValueType> const* A;
// cached auxiliary data
mutable std::unique_ptr<storm::storage::StronglyConnectedComponentDecomposition<ValueType>> sortedSccDecomposition;
mutable boost::optional<uint64_t> longestSccChainSize;
mutable std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> sccSolver;
mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowGroupVector; // A.rowGroupCount() entries
};
template<typename ValueType>
class TopologicalMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> {
public:
using MinMaxLinearEquationSolverFactory<ValueType>::create;
virtual std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> create(Environment const& env) const override;
};
}
}
Write Preview
Loading…
Cancel
Save