From e536851e5309df10dd8020c8f2c05049cf7c0984 Mon Sep 17 00:00:00 2001 From: JK Date: Wed, 5 Apr 2017 16:51:07 +0200 Subject: [PATCH 1/3] Solver: provide information about solving method + number of iterations at INFO log level --- .../solver/EigenLinearEquationSolver.cpp | 25 ++++++++++++++++++- .../EliminationLinearEquationSolver.cpp | 2 +- .../solver/GmmxxLinearEquationSolver.cpp | 6 ++--- .../solver/NativeLinearEquationSolver.cpp | 20 +++++++++++++-- ...ymbolicEliminationLinearEquationSolver.cpp | 2 +- src/storm/solver/SymbolicGameSolver.cpp | 2 +- .../SymbolicMinMaxLinearEquationSolver.cpp | 4 +-- .../SymbolicNativeLinearEquationSolver.cpp | 2 +- 8 files changed, 51 insertions(+), 12 deletions(-) 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."); } From 60ab1716b1178407b41ebaef8c186343a098171c Mon Sep 17 00:00:00 2001 From: JK Date: Wed, 22 Feb 2017 17:43:13 +0100 Subject: [PATCH 2/3] storm: bisimulation statistics --- src/storm/utility/storm.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 145583a61..407c0b40c 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -195,7 +195,7 @@ namespace storm { storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); bisimulationDecomposition.computeBisimulationDecomposition(); model = bisimulationDecomposition.getQuotient(); - STORM_LOG_INFO("Bisimulation done. "); + STORM_LOG_INFO("Bisimulation done, quotient model has " << model->getNumberOfStates() << " states and " << model->getNumberOfTransitions() << " transitions."); return model; } @@ -211,7 +211,7 @@ namespace storm { storm::storage::NondeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); bisimulationDecomposition.computeBisimulationDecomposition(); model = bisimulationDecomposition.getQuotient(); - STORM_LOG_INFO("Bisimulation done."); + STORM_LOG_INFO("Bisimulation done, quotient model has " << model->getNumberOfStates() << " states and " << model->getNumberOfTransitions() << " transitions."); return model; } From becc43e1e1f68432a1f8f4c79c66d9a7a5119d4b Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 5 Apr 2017 17:26:01 +0200 Subject: [PATCH 3/3] added wokaround proposed by jklein to make the new sylvan version build on older osx --- resources/3rdparty/sylvan/src/lace.c | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/resources/3rdparty/sylvan/src/lace.c b/resources/3rdparty/sylvan/src/lace.c index de97b8ff5..abdbbca39 100755 --- a/resources/3rdparty/sylvan/src/lace.c +++ b/resources/3rdparty/sylvan/src/lace.c @@ -26,6 +26,12 @@ #include #include +// work around for missing MAP_ANONYMOUS definition in sys/mman.h on +// older OS X versions +#if !(defined MAP_ANONYMOUS) && defined MAP_ANON +#define MAP_ANONYMOUS MAP_ANON +#endif + #include #include