Browse Source

started on requirements for MinMax solvers

tempestpy_adaptions
dehnert 7 years ago
parent
commit
72234e96b2
  1. 18
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  2. 9
      src/storm/solver/IterativeMinMaxLinearEquationSolver.h
  3. 19
      src/storm/solver/LpMinMaxLinearEquationSolver.cpp
  4. 11
      src/storm/solver/LpMinMaxLinearEquationSolver.h
  5. 67
      src/storm/solver/MinMaxLinearEquationSolver.cpp
  6. 86
      src/storm/solver/MinMaxLinearEquationSolver.h
  7. 49
      src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
  8. 14
      src/storm/solver/StandardMinMaxLinearEquationSolver.h
  9. 67
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
  10. 14
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.h

18
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@ -75,6 +75,11 @@ namespace storm {
return relative;
}
template<typename ValueType>
IterativeMinMaxLinearEquationSolver<ValueType>::IterativeMinMaxLinearEquationSolver(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings<ValueType> const& settings) : StandardMinMaxLinearEquationSolver<ValueType>(std::move(linearEquationSolverFactory)), settings(settings) {
// Intentionally left empty
}
template<typename ValueType>
IterativeMinMaxLinearEquationSolver<ValueType>::IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings<ValueType> const& settings) : StandardMinMaxLinearEquationSolver<ValueType>(A, std::move(linearEquationSolverFactory)), settings(settings) {
// Intentionally left empty.
@ -459,19 +464,10 @@ namespace storm {
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> IterativeMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized.");
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(std::move(matrix), this->linearEquationSolverFactory->clone(), settings);
result->setTrackScheduler(this->isTrackSchedulerSet());
return result;
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> IterativeMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> IterativeMinMaxLinearEquationSolverFactory<ValueType>::internalCreate() const {
STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized.");
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(std::move(matrix), this->linearEquationSolverFactory->clone(), settings);
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(this->linearEquationSolverFactory->clone(), settings);
result->setTrackScheduler(this->isTrackSchedulerSet());
return result;
}

9
src/storm/solver/IterativeMinMaxLinearEquationSolver.h

@ -36,7 +36,7 @@ namespace storm {
template<typename ValueType>
class IterativeMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver<ValueType> {
public:
IterativeMinMaxLinearEquationSolver() = default;
IterativeMinMaxLinearEquationSolver(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings<ValueType> const& settings = IterativeMinMaxLinearEquationSolverSettings<ValueType>());
IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings<ValueType> const& settings = IterativeMinMaxLinearEquationSolverSettings<ValueType>());
IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType>&& A, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings<ValueType> const& settings = IterativeMinMaxLinearEquationSolverSettings<ValueType>());
@ -81,18 +81,17 @@ namespace storm {
IterativeMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);
IterativeMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
IterativeMinMaxLinearEquationSolverSettings<ValueType>& getSettings();
IterativeMinMaxLinearEquationSolverSettings<ValueType> const& getSettings() const;
virtual void setMinMaxMethod(MinMaxMethodSelection const& newMethod) override;
virtual void setMinMaxMethod(MinMaxMethod const& newMethod) override;
protected:
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> internalCreate() const override;
private:
IterativeMinMaxLinearEquationSolverSettings<ValueType> settings;
};
}
}

19
src/storm/solver/LpMinMaxLinearEquationSolver.cpp

@ -9,6 +9,11 @@
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)) {
// 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)) {
// Intentionally left empty.
@ -119,21 +124,11 @@ namespace storm {
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> LpMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized.");
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> LpMinMaxLinearEquationSolverFactory<ValueType>::internalCreate() const {
STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized.");
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone());
result->setTrackScheduler(this->isTrackSchedulerSet());
return result;
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> LpMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized.");
STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized.");
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone());
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone());
result->setTrackScheduler(this->isTrackSchedulerSet());
return result;
}

11
src/storm/solver/LpMinMaxLinearEquationSolver.h

@ -10,7 +10,7 @@ namespace storm {
template<typename ValueType>
class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver<ValueType> {
public:
LpMinMaxLinearEquationSolver() = default;
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);
@ -29,12 +29,13 @@ namespace storm {
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler = false);
LpMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>>&& lpSolverFactory, bool trackScheduler = false);
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
virtual void setMinMaxMethod(MinMaxMethodSelection const& newMethod) override;
virtual void setMinMaxMethod(MinMaxMethod const& newMethod) override;
protected:
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> internalCreate() const override;
std::unique_ptr<LinearEquationSolverFactory<ValueType>> createLpEquationSolverFactory() const;
private:
std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;
};

67
src/storm/solver/MinMaxLinearEquationSolver.cpp

@ -19,7 +19,7 @@ namespace storm {
namespace solver {
template<typename ValueType>
MinMaxLinearEquationSolver<ValueType>::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), cachingEnabled(false) {
MinMaxLinearEquationSolver<ValueType>::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), cachingEnabled(false), requirementsChecked(false) {
// Intentionally left empty.
}
@ -132,13 +132,23 @@ namespace storm {
}
template<typename ValueType>
MinMaxLinearEquationSolverFactory<ValueType>::MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : trackScheduler(trackScheduler) {
setMinMaxMethod(method);
std::vector<MinMaxLinearEquationSolverRequirement> MinMaxLinearEquationSolver<ValueType>::getRequirements() const {
return std::vector<MinMaxLinearEquationSolverRequirement>();
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return this->create(matrix);
void MinMaxLinearEquationSolver<ValueType>::setRequirementsChecked(bool value) {
this->requirementsChecked = value;
}
template<typename ValueType>
bool MinMaxLinearEquationSolver<ValueType>::getRequirementsChecked() const {
return this->requirementsChecked;
}
template<typename ValueType>
MinMaxLinearEquationSolverFactory<ValueType>::MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : trackScheduler(trackScheduler) {
setMinMaxMethod(method);
}
template<typename ValueType>
@ -182,35 +192,45 @@ namespace storm {
MinMaxMethod const& MinMaxLinearEquationSolverFactory<ValueType>::getMinMaxMethod() const {
return method;
}
template<typename ValueType>
GeneralMinMaxLinearEquationSolverFactory<ValueType>::GeneralMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory<ValueType>(method, trackScheduler) {
// Intentionally left empty.
std::vector<MinMaxLinearEquationSolverRequirement> MinMaxLinearEquationSolverFactory<ValueType>::getRequirements() const {
// Create dummy solver and ask it for requirements.
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->internalCreate();
return solver->getRequirements();
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> GeneralMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return selectSolver(matrix);
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->internalCreate();
solver->setMatrix(matrix);
return solver;
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> GeneralMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return selectSolver(std::move(matrix));
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->internalCreate();
solver->setMatrix(std::move(matrix));
return solver;
}
template<typename ValueType>
template<typename MatrixType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> GeneralMinMaxLinearEquationSolverFactory<ValueType>::selectSolver(MatrixType&& matrix) const {
GeneralMinMaxLinearEquationSolverFactory<ValueType>::GeneralMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory<ValueType>(method, trackScheduler) {
// Intentionally left empty.
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> GeneralMinMaxLinearEquationSolverFactory<ValueType>::internalCreate() const {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result;
auto method = this->getMinMaxMethod();
if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) {
IterativeMinMaxLinearEquationSolverSettings<ValueType> iterativeSolverSettings;
iterativeSolverSettings.setSolutionMethod(method);
result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix), std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>(), iterativeSolverSettings);
result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>(), iterativeSolverSettings);
} else if (method == MinMaxMethod::Topological) {
result = std::make_unique<TopologicalMinMaxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix));
result = std::make_unique<TopologicalMinMaxLinearEquationSolver<ValueType>>();
} else if (method == MinMaxMethod::LinearProgramming) {
result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::forward<MatrixType>(matrix), std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>(), std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>());
result = std::make_unique<LpMinMaxLinearEquationSolver<ValueType>>(std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>(), std::make_unique<storm::utility::solver::LpSolverFactory<ValueType>>());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
@ -218,24 +238,23 @@ namespace storm {
return result;
}
#ifdef STORM_HAVE_CARL
template<>
template<typename MatrixType>
std::unique_ptr<MinMaxLinearEquationSolver<storm::RationalNumber>> GeneralMinMaxLinearEquationSolverFactory<storm::RationalNumber>::selectSolver(MatrixType&& matrix) const {
std::unique_ptr<MinMaxLinearEquationSolver<storm::RationalNumber>> GeneralMinMaxLinearEquationSolverFactory<storm::RationalNumber>::internalCreate() const {
std::unique_ptr<MinMaxLinearEquationSolver<storm::RationalNumber>> result;
auto method = this->getMinMaxMethod();
if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) {
IterativeMinMaxLinearEquationSolverSettings<storm::RationalNumber> iterativeSolverSettings;
iterativeSolverSettings.setSolutionMethod(method);
result = std::make_unique<IterativeMinMaxLinearEquationSolver<storm::RationalNumber>>(std::forward<MatrixType>(matrix), std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>(), iterativeSolverSettings);
result = std::make_unique<IterativeMinMaxLinearEquationSolver<storm::RationalNumber>>(std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>(), iterativeSolverSettings);
} else if (method == MinMaxMethod::LinearProgramming) {
result = std::make_unique<LpMinMaxLinearEquationSolver<storm::RationalNumber>>(std::forward<MatrixType>(matrix), 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<GeneralLinearEquationSolverFactory<storm::RationalNumber>>(), std::make_unique<storm::utility::solver::LpSolverFactory<storm::RationalNumber>>());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The selected method is not available for this data type.");
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
result->setTrackScheduler(this->isTrackSchedulerSet());
return result;
}
#endif
template class MinMaxLinearEquationSolver<float>;
template class MinMaxLinearEquationSolver<double>;

86
src/storm/solver/MinMaxLinearEquationSolver.h

@ -23,6 +23,14 @@ namespace storm {
namespace solver {
enum class MinMaxLinearEquationSolverRequirement {
ValidSchedulerHint,
ValidValueHint,
NoEndComponents,
GlobalUpperBound,
GlobalLowerBound
};
/*!
* A class representing the interface that all min-max linear equation solvers shall implement.
*/
@ -30,10 +38,13 @@ namespace storm {
class MinMaxLinearEquationSolver : public AbstractEquationSolver<ValueType> {
protected:
MinMaxLinearEquationSolver(OptimizationDirectionSetting direction = OptimizationDirectionSetting::Unset);
public:
virtual ~MinMaxLinearEquationSolver();
virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) = 0;
virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& matrix) = 0;
/*!
* Solves the equation system x = min/max(A*x + b) given by the parameters. Note that the matrix A has
* to be given upon construction time of the solver object.
@ -78,33 +89,33 @@ namespace storm {
* optimization direction is used. Note: this method can only be called after setting the optimization direction.
*/
virtual void repeatedMultiply(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.
*/
void setOptimizationDirection(OptimizationDirection direction);
/*!
* Unsets the optimization direction to use for calls to methods that do not explicitly provide one.
*/
void unsetOptimizationDirection();
/*!
* Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently
* stored scheduler (if any) is deleted.
*/
void setTrackScheduler(bool trackScheduler = true);
/*!
* Retrieves whether this solver is set to generate schedulers.
*/
bool isTrackSchedulerSet() const;
/*!
* Retrieves whether the solver generated a scheduler.
*/
bool hasScheduler() const;
/*!
* Retrieves the generated scheduler. Note: it is only legal to call this function if a scheduler was generated.
*/
@ -114,7 +125,7 @@ namespace storm {
* Retrieves the generated (deterministic) choices of the optimal scheduler. Note: it is only legal to call this function if a scheduler was generated.
*/
std::vector<uint_fast64_t> const& getSchedulerChoices() const;
/*!
* Sets whether some of the generated data during solver calls should be cached.
* This possibly decreases the runtime of subsequent calls but also increases memory consumption.
@ -125,12 +136,12 @@ namespace storm {
* Retrieves whether some of the generated data during solver calls should be cached.
*/
bool isCachingEnabled() const;
/*
* Clears the currently cached data that has been stored during previous calls of the solver.
*/
virtual void clearCache() const;
/*!
* Sets a lower bound for the solution that can potentially used by the solver.
*/
@ -154,15 +165,31 @@ namespace storm {
/*!
* Returns true iff a scheduler hint was defined
*/
bool hasSchedulerHint() const;
bool hasSchedulerHint() const;
/*!
* Retrieves the requirements of this solver for solving equations with the current settings.
*/
virtual std::vector<MinMaxLinearEquationSolverRequirement> getRequirements() const;
/*!
* Notifies the solver that the requirements for solving equations have been checked. If this has not been
* done before solving equations, the solver might issue a warning, perform the checks itself or even fail.
*/
void setRequirementsChecked(bool value = true);
/*!
* Retrieves whether the solver is aware that the requirements were checked.
*/
bool getRequirementsChecked() const;
protected:
/// The optimization direction to use for calls to functions that do not provide it explicitly. Can also be unset.
OptimizationDirectionSetting direction;
/// Whether we generate a scheduler during solving.
bool trackScheduler;
/// The scheduler choices that induce the optimal values (if they could be successfully generated).
mutable boost::optional<std::vector<uint_fast64_t>> schedulerChoices;
@ -179,16 +206,18 @@ namespace storm {
/// Whether some of the generated data during solver calls should be cached.
bool cachingEnabled;
/// A flag storing whether the requirements of the solver were checked.
bool requirementsChecked;
};
template<typename ValueType>
class MinMaxLinearEquationSolverFactory {
public:
MinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const = 0;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const;
void setTrackScheduler(bool value);
bool isTrackSchedulerSet() const;
@ -196,23 +225,24 @@ namespace storm {
virtual void setMinMaxMethod(MinMaxMethod const& newMethod);
MinMaxMethod const& getMinMaxMethod() const;
std::vector<MinMaxLinearEquationSolverRequirement> getRequirements() const;
protected:
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> internalCreate() const = 0;
private:
bool trackScheduler;
MinMaxMethod method;
};
template<typename ValueType>
class GeneralMinMaxLinearEquationSolverFactory : public MinMaxLinearEquationSolverFactory<ValueType> {
public:
GeneralMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
private:
template<typename MatrixType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> selectSolver(MatrixType&& matrix) const;
protected:
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> internalCreate() const override;
};
} // namespace solver

49
src/storm/solver/StandardMinMaxLinearEquationSolver.cpp

@ -15,7 +15,7 @@ namespace storm {
namespace solver {
template<typename ValueType>
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver() : A(nullptr) {
StandardMinMaxLinearEquationSolver<ValueType>::StandardMinMaxLinearEquationSolver(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), A(nullptr) {
// Intentionally left empty.
}
@ -29,6 +29,18 @@ namespace storm {
// Intentionally left empty.
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
this->localA = nullptr;
this->A = &matrix;
}
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();
}
template<typename ValueType>
void StandardMinMaxLinearEquationSolver<ValueType>::repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const {
if (!linEqSolverA) {
@ -80,46 +92,25 @@ namespace storm {
case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique<EliminationLinearEquationSolverFactory<ValueType>>(); break;
}
}
#ifdef STORM_HAVE_CARL
template<>
StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory<storm::RationalNumber>(method, trackScheduler) {
switch (solverType) {
case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique<EigenLinearEquationSolverFactory<storm::RationalNumber>>(); break;
case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique<EliminationLinearEquationSolverFactory<storm::RationalNumber>>(); break;
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, "Cannot create the requested solver for this data type.");
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported equation solver for this data type.");
}
}
#endif
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> StandardMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
STORM_LOG_ASSERT(linearEquationSolverFactory, "Linear equation solver factory not initialized.");
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result;
auto method = this->getMinMaxMethod();
if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) {
IterativeMinMaxLinearEquationSolverSettings<ValueType> iterativeSolverSettings;
iterativeSolverSettings.setSolutionMethod(method);
result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(matrix, linearEquationSolverFactory->clone(), iterativeSolverSettings);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}
result->setTrackScheduler(this->isTrackSchedulerSet());
return result;
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> StandardMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
STORM_LOG_ASSERT(linearEquationSolverFactory, "Linear equation solver factory not initialized.");
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> StandardMinMaxLinearEquationSolverFactory<ValueType>::internalCreate() const {
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> result;
auto method = this->getMinMaxMethod();
if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) {
IterativeMinMaxLinearEquationSolverSettings<ValueType> iterativeSolverSettings;
iterativeSolverSettings.setSolutionMethod(method);
result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(std::move(matrix), linearEquationSolverFactory->clone(), iterativeSolverSettings);
result = std::make_unique<IterativeMinMaxLinearEquationSolver<ValueType>>(this->linearEquationSolverFactory->clone(), iterativeSolverSettings);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
}

14
src/storm/solver/StandardMinMaxLinearEquationSolver.h

@ -9,11 +9,13 @@ namespace storm {
template<typename ValueType>
class StandardMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver<ValueType> {
public:
StandardMinMaxLinearEquationSolver();
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);
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(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const override;
@ -46,11 +48,13 @@ namespace storm {
StandardMinMaxLinearEquationSolverFactory(std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory, MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);
StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method = MinMaxMethodSelection::FROMSETTINGS, bool trackScheduler = false);
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
protected:
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> internalCreate() const override;
std::unique_ptr<LinearEquationSolverFactory<ValueType>> linearEquationSolverFactory;
private:
void createLinearEquationSolverFactory() const;
};
template<typename ValueType>

67
src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp

@ -23,15 +23,31 @@ namespace storm {
namespace solver {
template<typename ValueType>
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative)
{
// Get the settings object to customize solving.
this->enableCuda = storm::settings::getModule<storm::settings::modules::CoreSettings>().isCudaSet();
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) {
// Get the settings object to customize solving.
this->enableCuda = storm::settings::getModule<storm::settings::modules::CoreSettings>().isCudaSet();
#ifdef STORM_HAVE_CUDA
STORM_LOG_INFO_COND(this->enableCuda, "Option CUDA was not set, but the topological value iteration solver will use it anyways.");
STORM_LOG_INFO_COND(this->enableCuda, "Option CUDA was not set, but the topological value iteration solver will use it anyways.");
#endif
}
template<typename ValueType>
TopologicalMinMaxLinearEquationSolver<ValueType>::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : TopologicalMinMaxLinearEquationSolver(precision, maximalNumberOfIterations, relative) {
this->setMatrix(A);
}
template<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
this->localA = nullptr;
this->A = &matrix;
}
template<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::setMatrix(storm::storage::SparseMatrix<ValueType>&& matrix) {
this->localA = std::make_unique<storm::storage::SparseMatrix<ValueType>>(std::move(matrix));
this->A = this->localA.get();
}
template<typename ValueType>
bool TopologicalMinMaxLinearEquationSolver<ValueType>::solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
@ -42,7 +58,7 @@ namespace storm {
#endif
if (__FORCE_FLOAT_CALCULATION && std::is_same<ValueType, double>::value) {
// FIXME: This actually allocates quite some storage, because of this conversion, is it really necessary?
storm::storage::SparseMatrix<float> newA = this->A.template toValueType<float>();
storm::storage::SparseMatrix<float> newA = this->A->template toValueType<float>();
TopologicalMinMaxLinearEquationSolver<float> newSolver(newA, this->precision, this->maximalNumberOfIterations, this->relative);
@ -67,12 +83,12 @@ namespace storm {
}
// Now, we need to determine the SCCs of the MDP and perform a topological sort.
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = this->A.getRowGroupIndices();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = this->A->getRowGroupIndices();
// Check if the decomposition is necessary
#ifdef STORM_HAVE_CUDA
#define __USE_CUDAFORSTORM_OPT true
size_t const gpuSizeOfCompleteSystem = basicValueIteration_mvReduce_uint64_double_calculateMemorySize(static_cast<size_t>(A.getRowCount()), nondeterministicChoiceIndices.size(), static_cast<size_t>(A.getEntryCount()));
size_t const gpuSizeOfCompleteSystem = basicValueIteration_mvReduce_uint64_double_calculateMemorySize(static_cast<size_t>(A->getRowCount()), nondeterministicChoiceIndices.size(), static_cast<size_t>(A->getEntryCount()));
size_t const cudaFreeMemory = static_cast<size_t>(getFreeCudaMemory() * 0.95);
#else
#define __USE_CUDAFORSTORM_OPT false
@ -90,9 +106,9 @@ namespace storm {
bool result = false;
size_t globalIterations = 0;
if (dir == OptimizationDirection::Minimize) {
result = __basicValueIteration_mvReduce_minimize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, A.rowIndications, A.columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations);
result = __basicValueIteration_mvReduce_minimize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations);
} else {
result = __basicValueIteration_mvReduce_maximize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, A.rowIndications, A.columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations);
result = __basicValueIteration_mvReduce_maximize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, A->rowIndications, A->columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations);
}
STORM_LOG_INFO("Executed " << globalIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU.");
@ -116,16 +132,16 @@ namespace storm {
throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!";
#endif
} else {
storm::storage::BitVector fullSystem(this->A.getRowGroupCount(), true);
storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccDecomposition(this->A, fullSystem, false, false);
storm::storage::BitVector fullSystem(this->A->getRowGroupCount(), true);
storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccDecomposition(*this->A, fullSystem, false, false);
STORM_LOG_THROW(sccDecomposition.size() > 0, storm::exceptions::IllegalArgumentException, "Can not solve given equation system as the SCC decomposition returned no SCCs.");
storm::storage::SparseMatrix<ValueType> stronglyConnectedComponentsDependencyGraph = sccDecomposition.extractPartitionDependencyGraph(this->A);
storm::storage::SparseMatrix<ValueType> stronglyConnectedComponentsDependencyGraph = sccDecomposition.extractPartitionDependencyGraph(*this->A);
std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);
// Calculate the optimal distribution of sccs
std::vector<std::pair<bool, storm::storage::StateBlock>> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, this->A);
std::vector<std::pair<bool, storm::storage::StateBlock>> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, *this->A);
STORM_LOG_INFO("Optimized SCC Decomposition, originally " << topologicalSort.size() << " SCCs, optimized to " << optimalSccs.size() << " SCCs.");
std::vector<ValueType>* currentX = nullptr;
@ -142,8 +158,8 @@ namespace storm {
storm::storage::StateBlock const& scc = sccIndexIt->second;
// Generate a sub matrix
storm::storage::BitVector subMatrixIndices(this->A.getColumnCount(), scc.cbegin(), scc.cend());
storm::storage::SparseMatrix<ValueType> sccSubmatrix = this->A.getSubmatrix(true, subMatrixIndices, subMatrixIndices);
storm::storage::BitVector subMatrixIndices(this->A->getColumnCount(), scc.cbegin(), scc.cend());
storm::storage::SparseMatrix<ValueType> sccSubmatrix = this->A->getSubmatrix(true, subMatrixIndices, subMatrixIndices);
std::vector<ValueType> sccSubB(sccSubmatrix.getRowCount());
storm::utility::vector::selectVectorValues<ValueType>(sccSubB, subMatrixIndices, nondeterministicChoiceIndices, b);
std::vector<ValueType> sccSubX(sccSubmatrix.getColumnCount());
@ -167,7 +183,7 @@ namespace storm {
sccSubNondeterministicChoiceIndices.at(outerIndex + 1) = sccSubNondeterministicChoiceIndices.at(outerIndex) + (nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state]);
for (auto rowGroupIt = nondeterministicChoiceIndices[state]; rowGroupIt != nondeterministicChoiceIndices[state + 1]; ++rowGroupIt) {
typename storm::storage::SparseMatrix<ValueType>::const_rows row = this->A.getRow(rowGroupIt);
typename storm::storage::SparseMatrix<ValueType>::const_rows row = this->A->getRow(rowGroupIt);
for (auto rowIt = row.begin(); rowIt != row.end(); ++rowIt) {
if (!subMatrixIndices.get(rowIt->getColumn())) {
// This is an outgoing transition of a state in the SCC to a state not included in the SCC
@ -439,11 +455,11 @@ namespace storm {
template<typename ValueType>
void TopologicalMinMaxLinearEquationSolver<ValueType>::repeatedMultiply(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());
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);
this->A->multiplyWithVector(x, *multiplyResult);
// Add b if it is non-null.
if (b != nullptr) {
@ -452,7 +468,7 @@ namespace storm {
// 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());
storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, this->A->getRowGroupIndices());
}
}
@ -462,15 +478,10 @@ namespace storm {
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> TopologicalMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
return std::make_unique<TopologicalMinMaxLinearEquationSolver<ValueType>>(matrix);
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> TopologicalMinMaxLinearEquationSolverFactory<ValueType>::internalCreate() const {
return std::make_unique<TopologicalMinMaxLinearEquationSolver<ValueType>>();
}
template<typename ValueType>
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> TopologicalMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return std::make_unique<TopologicalMinMaxLinearEquationSolver<ValueType>>(std::move(matrix));
}
// Explicitly instantiate the solver.
template class TopologicalMinMaxLinearEquationSolver<double>;

14
src/storm/solver/TopologicalMinMaxLinearEquationSolver.h

@ -24,6 +24,8 @@ namespace storm {
template<class ValueType>
class TopologicalMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver<ValueType> {
public:
TopologicalMinMaxLinearEquationSolver(double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true);
/*!
* Constructs a min-max linear equation solver with parameters being set according to the settings
* object.
@ -31,7 +33,10 @@ namespace storm {
* @param A The matrix defining the coefficients of the linear equation system.
*/
TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, double precision = 1e-6, uint_fast64_t maximalNumberOfIterations = 20000, bool relative = true);
virtual void setMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) override;
virtual void setMatrix(storm::storage::SparseMatrix<ValueType>&& matrix) override;
virtual bool solveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
virtual void repeatedMultiply(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n) const override;
@ -40,7 +45,8 @@ namespace storm {
bool getRelative() const;
private:
storm::storage::SparseMatrix<ValueType> const& A;
storm::storage::SparseMatrix<ValueType> const* A;
std::unique_ptr<storm::storage::SparseMatrix<ValueType>> localA;
double precision;
uint_fast64_t maximalNumberOfIterations;
bool relative;
@ -144,8 +150,8 @@ namespace storm {
public:
TopologicalMinMaxLinearEquationSolverFactory(bool trackScheduler = false);
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType> const& matrix) const override;
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> create(storm::storage::SparseMatrix<ValueType>&& matrix) const override;
protected:
virtual std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> internalCreate() const override;
};
} // namespace solver

Loading…
Cancel
Save