#include "storm/solver/EigenLinearEquationSolver.h" #include "storm/adapters/EigenAdapter.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/EigenEquationSolverSettings.h" #include "storm/utility/vector.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidSettingsException.h" namespace storm { namespace solver { template EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { // Get the settings object to customize linear solving. storm::settings::modules::EigenEquationSolverSettings const& settings = storm::settings::getModule(); // Determine the method to be used. storm::settings::modules::EigenEquationSolverSettings::LinearEquationMethod methodAsSetting = settings.getLinearEquationSystemMethod(); if (methodAsSetting == storm::settings::modules::EigenEquationSolverSettings::LinearEquationMethod::BiCGSTAB) { method = SolutionMethod::BiCGSTAB; } else if (methodAsSetting == storm::settings::modules::EigenEquationSolverSettings::LinearEquationMethod::SparseLU) { method = SolutionMethod::SparseLU; } else if (methodAsSetting == storm::settings::modules::EigenEquationSolverSettings::LinearEquationMethod::DGMRES) { method = SolutionMethod::DGMRES; } else if (methodAsSetting == storm::settings::modules::EigenEquationSolverSettings::LinearEquationMethod::GMRES) { method = SolutionMethod::GMRES; } // Check which preconditioner to use. storm::settings::modules::EigenEquationSolverSettings::PreconditioningMethod preconditionAsSetting = settings.getPreconditioningMethod(); if (preconditionAsSetting == storm::settings::modules::EigenEquationSolverSettings::PreconditioningMethod::Ilu) { preconditioner = Preconditioner::Ilu; } else if (preconditionAsSetting == storm::settings::modules::EigenEquationSolverSettings::PreconditioningMethod::Diagonal) { preconditioner = Preconditioner::Diagonal; } else if (preconditionAsSetting == storm::settings::modules::EigenEquationSolverSettings::PreconditioningMethod::None) { preconditioner = Preconditioner::None; } // Get appropriate settings. maximalNumberOfIterations = settings.getMaximalIterationCount(); precision = settings.getPrecision(); restart = settings.getRestartIterationCount(); // Finally force soundness and potentially overwrite some other settings. this->setForceSoundness(storm::settings::getModule().isSoundSet()); } template void EigenLinearEquationSolverSettings::setSolutionMethod(SolutionMethod const& method) { this->method = method; // Make sure we switch the method if we have to guarantee soundness. this->setForceSoundness(forceSoundness); } template void EigenLinearEquationSolverSettings::setPreconditioner(Preconditioner const& preconditioner) { this->preconditioner = preconditioner; } template void EigenLinearEquationSolverSettings::setPrecision(ValueType precision) { this->precision = precision; } template void EigenLinearEquationSolverSettings::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) { this->maximalNumberOfIterations = maximalNumberOfIterations; } template void EigenLinearEquationSolverSettings::setNumberOfIterationsUntilRestart(uint64_t restart) { this->restart = restart; } template void EigenLinearEquationSolverSettings::setForceSoundness(bool value) { forceSoundness = value; if (value) { STORM_LOG_WARN_COND(method != SolutionMethod::SparseLU, "To guarantee soundness, the equation solving technique has been switched to '" << storm::settings::modules::EigenEquationSolverSettings:: LinearEquationMethod::SparseLU << "'."); method = SolutionMethod::SparseLU; } } template typename EigenLinearEquationSolverSettings::SolutionMethod EigenLinearEquationSolverSettings::getSolutionMethod() const { return this->method; } template typename EigenLinearEquationSolverSettings::Preconditioner EigenLinearEquationSolverSettings::getPreconditioner() const { return this->preconditioner; } template ValueType EigenLinearEquationSolverSettings::getPrecision() const { return this->precision; } template uint64_t EigenLinearEquationSolverSettings::getMaximalNumberOfIterations() const { return this->maximalNumberOfIterations; } template uint64_t EigenLinearEquationSolverSettings::getNumberOfIterationsUntilRestart() const { return restart; } template bool EigenLinearEquationSolverSettings::getForceSoundness() const { return forceSoundness; } #ifdef STORM_HAVE_CARL EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { // Intentionally left empty. } EigenLinearEquationSolverSettings::EigenLinearEquationSolverSettings() { // Intentionally left empty. } #endif template EigenLinearEquationSolver::EigenLinearEquationSolver(EigenLinearEquationSolverSettings const& settings) : settings(settings) { // Intentionally left empty. } template EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix const& A, EigenLinearEquationSolverSettings const& settings) : settings(settings) { this->setMatrix(A); } template EigenLinearEquationSolver::EigenLinearEquationSolver(storm::storage::SparseMatrix&& A, EigenLinearEquationSolverSettings const& settings) : settings(settings) { this->setMatrix(std::move(A)); } template void EigenLinearEquationSolver::setMatrix(storm::storage::SparseMatrix const& A) { eigenA = storm::adapters::EigenAdapter::toEigenSparseMatrix(A); this->clearCache(); } template void EigenLinearEquationSolver::setMatrix(storm::storage::SparseMatrix&& A) { // Take ownership of the matrix so it is destroyed after we have translated it to Eigen's format. storm::storage::SparseMatrix localA(std::move(A)); this->setMatrix(localA); this->clearCache(); } template bool EigenLinearEquationSolver::internalSolveEquations(std::vector& x, std::vector const& b) const { // Map the input vectors to Eigen's format. auto eigenX = StormEigen::Matrix::Map(x.data(), x.size()); auto eigenB = StormEigen::Matrix::Map(b.data(), b.size()); typename EigenLinearEquationSolverSettings::SolutionMethod solutionMethod = this->getSettings().getSolutionMethod(); if (solutionMethod == EigenLinearEquationSolverSettings::SolutionMethod::SparseLU) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with sparse LU factorization (Eigen library)."); StormEigen::SparseLU, StormEigen::COLAMDOrdering> solver; solver.compute(*this->eigenA); solver._solve_impl(eigenB, eigenX); } else { bool converged = false; uint64_t numberOfIterations = 0; typename EigenLinearEquationSolverSettings::Preconditioner preconditioner = this->getSettings().getPreconditioner(); if (solutionMethod == EigenLinearEquationSolverSettings::SolutionMethod::BiCGSTAB) { if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Ilu) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Ilu preconditioner (Eigen library)."); StormEigen::BiCGSTAB, StormEigen::IncompleteLUT> solver; solver.compute(*this->eigenA); solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == StormEigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Diagonal) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with Diagonal preconditioner (Eigen library)."); StormEigen::BiCGSTAB, StormEigen::DiagonalPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == StormEigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with BiCGSTAB with identity preconditioner (Eigen library)."); StormEigen::BiCGSTAB, StormEigen::IdentityPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); numberOfIterations = solver.iterations(); converged = solver.info() == StormEigen::ComputationInfo::Success; } } else if (solutionMethod == EigenLinearEquationSolverSettings::SolutionMethod::DGMRES) { if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Ilu) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with Ilu preconditioner (Eigen library)."); StormEigen::DGMRES, StormEigen::IncompleteLUT> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == StormEigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Diagonal) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with Diagonal preconditioner (Eigen library)."); StormEigen::DGMRES, StormEigen::DiagonalPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == StormEigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with DGMRES with identity preconditioner (Eigen library)."); StormEigen::DGMRES, StormEigen::IdentityPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == StormEigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } } else if (solutionMethod == EigenLinearEquationSolverSettings::SolutionMethod::GMRES) { if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Ilu) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with Ilu preconditioner (Eigen library)."); StormEigen::GMRES, StormEigen::IncompleteLUT> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == StormEigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Diagonal) { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with Diagonal preconditioner (Eigen library)."); StormEigen::GMRES, StormEigen::DiagonalPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == StormEigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } else { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with GMRES with identity preconditioner (Eigen library)."); StormEigen::GMRES, StormEigen::IdentityPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); converged = solver.info() == StormEigen::ComputationInfo::Success; numberOfIterations = solver.iterations(); } } // Make sure that all results conform to the (global) bounds. storm::utility::vector::clip(x, this->lowerBound, this->upperBound); // Check if the solver converged and issue a warning otherwise. if (converged) { STORM_LOG_INFO("Iterative solver converged after " << numberOfIterations << " iterations."); return true; } else { STORM_LOG_WARN("Iterative solver did not converge."); return false; } } return true; } template void EigenLinearEquationSolver::multiply(std::vector& x, std::vector const* b, std::vector& result) const { // Typedef the map-type so we don't have to spell it out. typedef decltype(StormEigen::Matrix::Map(b->data(), b->size())) MapType; auto eigenX = StormEigen::Matrix::Map(x.data(), x.size()); auto eigenResult = StormEigen::Matrix::Map(result.data(), result.size()); std::unique_ptr eigenB; if (b != nullptr) { eigenB = std::make_unique(StormEigen::Matrix::Map(b->data(), b->size())); } if (&x != &result) { if (b != nullptr) { eigenResult.noalias() = *eigenA * eigenX + *eigenB; } else { eigenResult.noalias() = *eigenA * eigenX; } } else { if (b != nullptr) { eigenResult = *eigenA * eigenX + *eigenB; } else { eigenResult = *eigenA * eigenX; } } } template EigenLinearEquationSolverSettings& EigenLinearEquationSolver::getSettings() { return settings; } template LinearEquationSolverProblemFormat EigenLinearEquationSolver::getEquationProblemFormat() const { return LinearEquationSolverProblemFormat::EquationSystem; } template EigenLinearEquationSolverSettings const& EigenLinearEquationSolver::getSettings() const { return settings; } template uint64_t EigenLinearEquationSolver::getMatrixRowCount() const { return eigenA->rows(); } template uint64_t EigenLinearEquationSolver::getMatrixColumnCount() const { return eigenA->cols(); } #ifdef STORM_HAVE_CARL // Specialization for storm::RationalNumber template<> bool EigenLinearEquationSolver::internalSolveEquations(std::vector& x, std::vector const& b) const { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with with rational numbers using LU factorization (Eigen library)."); // Map the input vectors to Eigen's format. auto eigenX = StormEigen::Matrix::Map(x.data(), x.size()); auto eigenB = StormEigen::Matrix::Map(b.data(), b.size()); StormEigen::SparseLU, StormEigen::COLAMDOrdering> solver; solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); return solver.info() == StormEigen::ComputationInfo::Success; } // Specialization for storm::RationalFunction template<> bool EigenLinearEquationSolver::internalSolveEquations(std::vector& x, std::vector const& b) const { STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with rational functions using LU factorization (Eigen library)."); // Map the input vectors to Eigen's format. auto eigenX = StormEigen::Matrix::Map(x.data(), x.size()); auto eigenB = StormEigen::Matrix::Map(b.data(), b.size()); StormEigen::SparseLU, StormEigen::COLAMDOrdering> solver; solver.compute(*eigenA); solver._solve_impl(eigenB, eigenX); return solver.info() == StormEigen::ComputationInfo::Success; } #endif template std::unique_ptr> EigenLinearEquationSolverFactory::create() const { return std::make_unique>(settings); } template EigenLinearEquationSolverSettings& EigenLinearEquationSolverFactory::getSettings() { return settings; } template EigenLinearEquationSolverSettings const& EigenLinearEquationSolverFactory::getSettings() const { return settings; } template std::unique_ptr> EigenLinearEquationSolverFactory::clone() const { return std::make_unique>(*this); } template class EigenLinearEquationSolverSettings; template class EigenLinearEquationSolver; template class EigenLinearEquationSolverFactory; #ifdef STORM_HAVE_CARL template class EigenLinearEquationSolver; template class EigenLinearEquationSolver; template class EigenLinearEquationSolverFactory; template class EigenLinearEquationSolverFactory; #endif } }