#include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/solver/IterativeMinMaxLinearEquationSolver.h" #include "storm/solver/GmmxxLinearEquationSolver.h" #include "storm/solver/EigenLinearEquationSolver.h" #include "storm/solver/NativeLinearEquationSolver.h" #include "storm/solver/EliminationLinearEquationSolver.h" #include "storm/utility/vector.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/NotImplementedException.h" namespace storm { namespace solver { template StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(A) { // Intentionally left empty. } template StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique>(std::move(A))), A(*localA) { // Intentionally left empty. } template void StandardMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { if (!linEqSolverA) { linEqSolverA = linearEquationSolverFactory->create(A); linEqSolverA->setCachingEnabled(true); } if (!auxiliaryRowVector) { auxiliaryRowVector = std::make_unique>(A.getRowCount()); } std::vector& multiplyResult = *auxiliaryRowVector; for (uint64_t i = 0; i < n; ++i) { linEqSolverA->multiply(x, 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()); } if (!this->isCachingEnabled()) { clearCache(); } } template void StandardMinMaxLinearEquationSolver::clearCache() const { linEqSolverA.reset(); auxiliaryRowVector.reset(); MinMaxLinearEquationSolver::clearCache(); } template StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } template StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } template StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler) { switch (solverType) { case EquationSolverType::Gmmxx: linearEquationSolverFactory = std::make_unique>(); break; case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique>(); break; case EquationSolverType::Native: linearEquationSolverFactory = std::make_unique>(); break; case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique>(); break; } } #ifdef STORM_HAVE_CARL template<> StandardMinMaxLinearEquationSolverFactory::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, MinMaxMethodSelection const& method, bool trackScheduler) : MinMaxLinearEquationSolverFactory(method, trackScheduler) { switch (solverType) { case EquationSolverType::Eigen: linearEquationSolverFactory = std::make_unique>(); break; case EquationSolverType::Elimination: linearEquationSolverFactory = std::make_unique>(); break; default: STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot create the requested solver for this data type."); } } #endif template std::unique_ptr> StandardMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { STORM_LOG_ASSERT(linearEquationSolverFactory, "Linear equation solver factory not initialized."); std::unique_ptr> result; auto method = this->getMinMaxMethod(); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; iterativeSolverSettings.setSolutionMethod(method); result = std::make_unique>(matrix, linearEquationSolverFactory->clone(), iterativeSolverSettings); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } result->setTrackScheduler(this->isTrackSchedulerSet()); return result; } template std::unique_ptr> StandardMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { STORM_LOG_ASSERT(linearEquationSolverFactory, "Linear equation solver factory not initialized."); std::unique_ptr> result; auto method = this->getMinMaxMethod(); if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; iterativeSolverSettings.setSolutionMethod(method); result = std::make_unique>(std::move(matrix), linearEquationSolverFactory->clone(), iterativeSolverSettings); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } result->setTrackScheduler(this->isTrackSchedulerSet()); return result; } template GmmxxMinMaxLinearEquationSolverFactory::GmmxxMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Gmmxx, method, trackScheduler) { // Intentionally left empty. } template EigenMinMaxLinearEquationSolverFactory::EigenMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Eigen, method, trackScheduler) { // Intentionally left empty. } template NativeMinMaxLinearEquationSolverFactory::NativeMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Native, method, trackScheduler) { // Intentionally left empty. } template EliminationMinMaxLinearEquationSolverFactory::EliminationMinMaxLinearEquationSolverFactory(MinMaxMethodSelection const& method, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(EquationSolverType::Elimination, method, trackScheduler) { // Intentionally left empty. } template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolverFactory; template class GmmxxMinMaxLinearEquationSolverFactory; template class EigenMinMaxLinearEquationSolverFactory; template class NativeMinMaxLinearEquationSolverFactory; template class EliminationMinMaxLinearEquationSolverFactory; #ifdef STORM_HAVE_CARL template class StandardMinMaxLinearEquationSolver; template class StandardMinMaxLinearEquationSolverFactory; template class EigenMinMaxLinearEquationSolverFactory; template class EliminationMinMaxLinearEquationSolverFactory; #endif } }