diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp index b05fe6add..d82994e50 100644 --- a/src/storm/solver/EigenLinearEquationSolver.cpp +++ b/src/storm/solver/EigenLinearEquationSolver.cpp @@ -137,6 +137,7 @@ namespace storm { 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); @@ -147,6 +148,8 @@ namespace storm { 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()); @@ -155,6 +158,8 @@ namespace storm { 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()); @@ -163,6 +168,8 @@ namespace storm { 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()); @@ -173,6 +180,8 @@ namespace storm { } } 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()); @@ -182,6 +191,8 @@ namespace storm { 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()); @@ -191,6 +202,8 @@ namespace storm { 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()); @@ -202,6 +215,8 @@ namespace storm { } } 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()); @@ -211,6 +226,8 @@ namespace storm { 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()); @@ -220,6 +237,8 @@ namespace storm { 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()); @@ -236,7 +255,7 @@ namespace storm { // Check if the solver converged and issue a warning otherwise. if (converged) { - STORM_LOG_DEBUG("Iterative solver converged after " << numberOfIterations << " iterations."); + STORM_LOG_INFO("Iterative solver converged after " << numberOfIterations << " iterations."); return true; } else { STORM_LOG_WARN("Iterative solver did not converge."); @@ -299,6 +318,8 @@ namespace storm { // Specialization for storm::RationalNumber template<> bool EigenLinearEquationSolver::solveEquations(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()); @@ -312,6 +333,8 @@ namespace storm { // Specialization for storm::RationalFunction template<> bool EigenLinearEquationSolver::solveEquations(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()); diff --git a/src/storm/solver/EliminationLinearEquationSolver.cpp b/src/storm/solver/EliminationLinearEquationSolver.cpp index 4fd658294..6bfac7031 100644 --- a/src/storm/solver/EliminationLinearEquationSolver.cpp +++ b/src/storm/solver/EliminationLinearEquationSolver.cpp @@ -63,7 +63,7 @@ namespace storm { // not work for systems that have a 0 on the diagonal. This is not a restriction of this technique in general // but arbitrary matrices require pivoting, which is not currently implemented. - STORM_LOG_DEBUG("Solving equation system using elimination."); + STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with elimination"); // We need to revert the transformation into an equation system matrix, because the elimination procedure // and the distance computation is based on the probability matrix instead. diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index 31c358a22..7503584c8 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -139,7 +139,7 @@ namespace storm { bool GmmxxLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { auto method = this->getSettings().getSolutionMethod(); auto preconditioner = this->getSettings().getPreconditioner(); - STORM_LOG_DEBUG("Using method '" << method << "' with preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations)."); + STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with Gmmxx linear equation solver with method '" << method << "' and preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations)."); if (method == GmmxxLinearEquationSolverSettings::SolutionMethod::Jacobi && preconditioner != GmmxxLinearEquationSolverSettings::Preconditioner::None) { STORM_LOG_WARN("Jacobi method currently does not support preconditioners. The requested preconditioner will be ignored."); } @@ -197,7 +197,7 @@ namespace storm { // Check if the solver converged and issue a warning otherwise. if (iter.converged()) { - STORM_LOG_DEBUG("Iterative solver converged after " << iter.get_iteration() << " iterations."); + STORM_LOG_INFO("Iterative solver converged after " << iter.get_iteration() << " iterations."); return true; } else { STORM_LOG_WARN("Iterative solver did not converge."); @@ -211,7 +211,7 @@ namespace storm { // Check if the solver converged and issue a warning otherwise. if (iterations < this->getSettings().getMaximalNumberOfIterations()) { - STORM_LOG_DEBUG("Iterative solver converged after " << iterations << " iterations."); + STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); return true; } else { STORM_LOG_WARN("Iterative solver did not converge."); diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index f9763434a..339e56c6f 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -117,7 +117,9 @@ namespace storm { if (this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::SOR || this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::GaussSeidel) { // Define the omega used for SOR. ValueType omega = this->getSettings().getSolutionMethod() == NativeLinearEquationSolverSettings::SolutionMethod::SOR ? this->getSettings().getOmega() : storm::utility::one(); - + + STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (Gauss-Seidel, SOR omega = " << omega << ")"); + // Set up additional environment variables. uint_fast64_t iterationCount = 0; bool converged = false; @@ -141,9 +143,17 @@ namespace storm { clearCache(); } + if (converged) { + STORM_LOG_INFO("Iterative solver converged in " << iterationCount << " iterations."); + } else { + STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterations."); + } + return converged; } else { + STORM_LOG_INFO("Solving linear equation system (" << x.size() << " rows) with NativeLinearEquationSolver (Jacobi)"); + // Get a Jacobi decomposition of the matrix A. if(!jacobiDecomposition) { jacobiDecomposition = std::make_unique, std::vector>>(A->getJacobiDecomposition()); @@ -183,7 +193,13 @@ namespace storm { if (!this->isCachingEnabled()) { clearCache(); } - + + if (converged) { + STORM_LOG_INFO("Iterative solver converged in " << iterationCount << " iterations."); + } else { + STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterations."); + } + return iterationCount < this->getSettings().getMaximalNumberOfIterations(); } } diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp index 02e93ecfd..2fef23623 100644 --- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp @@ -102,7 +102,7 @@ namespace storm { STORM_LOG_TRACE("Completed iteration " << iterations << " of elimination process."); } - STORM_LOG_DEBUG("Elimination completed in " << iterations << " iterations."); + STORM_LOG_INFO("Elimination completed in " << iterations << " iterations."); return solution.swapVariables(rowRowMetaVariablePairs); } diff --git a/src/storm/solver/SymbolicGameSolver.cpp b/src/storm/solver/SymbolicGameSolver.cpp index 996c7fc72..cead11f2a 100644 --- a/src/storm/solver/SymbolicGameSolver.cpp +++ b/src/storm/solver/SymbolicGameSolver.cpp @@ -113,7 +113,7 @@ namespace storm { ++iterations; } while (!converged && iterations < this->maximalNumberOfIterations); - STORM_LOG_TRACE("Numerically solving the game took " << iterations << " iterations."); + STORM_LOG_INFO("Numerically solving the game took " << iterations << " iterations."); return xCopy; } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 78e889b1b..7499f166c 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -123,7 +123,7 @@ namespace storm { } if (converged) { - STORM_LOG_TRACE("Iterative solver (value iteration) converged in " << iterations << " iterations."); + STORM_LOG_INFO("Iterative solver (value iteration) converged in " << iterations << " iterations."); } else { STORM_LOG_WARN("Iterative solver (value iteration) did not converge in " << iterations << " iterations."); } @@ -181,7 +181,7 @@ namespace storm { } if (converged) { - STORM_LOG_TRACE("Iterative solver (policy iteration) converged in " << iterations << " iterations."); + STORM_LOG_INFO("Iterative solver (policy iteration) converged in " << iterations << " iterations."); } else { STORM_LOG_WARN("Iterative solver (policy iteration) did not converge in " << iterations << " iterations."); } diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index 4bd28f38b..000e25926 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -92,7 +92,7 @@ namespace storm { } if (converged) { - STORM_LOG_TRACE("Iterative solver converged in " << iterationCount << " iterations."); + STORM_LOG_INFO("Iterative solver converged in " << iterationCount << " iterations."); } else { STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterations."); }