From 398c317a7d0b8229555d36b6354b4b11316fd5ab Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 18 Jan 2017 14:48:35 +0100 Subject: [PATCH] allowing constant definition string to refer to other variables on the right-hand side of assignments, added convergence statement in eigen solver --- .../solver/EigenLinearEquationSolver.cpp | 40 ++++++++++++++----- .../solver/GmmxxLinearEquationSolver.cpp | 2 +- src/storm/utility/cli.cpp | 6 ++- 3 files changed, 37 insertions(+), 11 deletions(-) diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp index 0eed80f13..bf80f4db9 100644 --- a/src/storm/solver/EigenLinearEquationSolver.cpp +++ b/src/storm/solver/EigenLinearEquationSolver.cpp @@ -140,6 +140,9 @@ namespace storm { 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) { @@ -148,21 +151,24 @@ namespace storm { solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); eigenX = solver.solveWithGuess(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == StormEigen::ComputationInfo::Success; + numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Diagonal) { StormEigen::BiCGSTAB, StormEigen::DiagonalPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == StormEigen::ComputationInfo::Success; + numberOfIterations = solver.iterations(); } else { StormEigen::BiCGSTAB, StormEigen::IdentityPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); solver.setMaxIterations(this->getSettings().getMaximalNumberOfIterations()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + numberOfIterations = solver.iterations(); + converged = solver.info() == StormEigen::ComputationInfo::Success; } } else if (solutionMethod == EigenLinearEquationSolverSettings::SolutionMethod::DGMRES) { if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Ilu) { @@ -172,7 +178,8 @@ namespace storm { solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == StormEigen::ComputationInfo::Success; + numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Diagonal) { StormEigen::DGMRES, StormEigen::DiagonalPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); @@ -180,7 +187,8 @@ namespace storm { solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == StormEigen::ComputationInfo::Success; + numberOfIterations = solver.iterations(); } else { StormEigen::DGMRES, StormEigen::IdentityPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); @@ -188,7 +196,8 @@ namespace storm { solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == StormEigen::ComputationInfo::Success; + numberOfIterations = solver.iterations(); } } else if (solutionMethod == EigenLinearEquationSolverSettings::SolutionMethod::GMRES) { if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Ilu) { @@ -198,7 +207,8 @@ namespace storm { solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == StormEigen::ComputationInfo::Success; + numberOfIterations = solver.iterations(); } else if (preconditioner == EigenLinearEquationSolverSettings::Preconditioner::Diagonal) { StormEigen::GMRES, StormEigen::DiagonalPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); @@ -206,7 +216,8 @@ namespace storm { solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == StormEigen::ComputationInfo::Success; + numberOfIterations = solver.iterations(); } else { StormEigen::GMRES, StormEigen::IdentityPreconditioner> solver; solver.setTolerance(this->getSettings().getPrecision()); @@ -214,10 +225,21 @@ namespace storm { solver.set_restart(this->getSettings().getNumberOfIterationsUntilRestart()); solver.compute(*this->eigenA); eigenX = solver.solveWithGuess(eigenB, eigenX); - return solver.info() == StormEigen::ComputationInfo::Success; + converged = solver.info() == StormEigen::ComputationInfo::Success; + numberOfIterations = solver.iterations(); } } + + // Check if the solver converged and issue a warning otherwise. + if (converged) { + STORM_LOG_DEBUG("Iterative solver converged after " << numberOfIterations << " iterations."); + return true; + } else { + STORM_LOG_WARN("Iterative solver did not converge."); + return false; + } } + return false; } diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index ecccd4682..c92817ac2 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -187,7 +187,7 @@ namespace storm { } } - if(!this->isCachingEnabled()) { + if (!this->isCachingEnabled()) { clearCache(); } diff --git a/src/storm/utility/cli.cpp b/src/storm/utility/cli.cpp index b8da7a264..d7606149b 100644 --- a/src/storm/utility/cli.cpp +++ b/src/storm/utility/cli.cpp @@ -36,7 +36,11 @@ namespace storm { STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::WrongFormatException, "Illegally trying to define constant '" << constantName <<"' twice."); definedConstants.insert(variable); - if (variable.hasBooleanType()) { + if (manager.hasVariable(value)) { + auto const& valueVariable = manager.getVariable(value); + STORM_LOG_THROW(variable.getType() == valueVariable.getType(), storm::exceptions::WrongFormatException, "Illegally trying to define constant '" << constantName << "' by constant '" << valueVariable.getName() << " of different type."); + constantDefinitions[variable] = valueVariable.getExpression(); + } else if (variable.hasBooleanType()) { if (value == "true") { constantDefinitions[variable] = manager.boolean(true); } else if (value == "false") {