diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index d04156cc..50aaa32f 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -577,6 +577,13 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.print("Value iteration"); mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Return results res = new ModelCheckerResult(); res.soln = soln; @@ -654,6 +661,13 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.print("Gauss-Seidel"); mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Return results res = new ModelCheckerResult(); res.soln = soln; @@ -919,6 +933,13 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.print("Value iteration"); mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Return results res = new ModelCheckerResult(); res.soln = soln; @@ -979,6 +1000,13 @@ public class DTMCModelChecker extends ProbModelChecker mainLog.print("Value iteration"); mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Return results res = new ModelCheckerResult(); res.soln = soln; diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 973c010f..d3e76c57 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -563,6 +563,13 @@ public class MDPModelChecker extends ProbModelChecker mainLog.print("Value iteration (" + (min ? "min" : "max") + ")"); mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Print adversary if (genAdv) { PrismLog out = new PrismFileLog(exportAdvFilename); @@ -651,6 +658,13 @@ public class MDPModelChecker extends ProbModelChecker mainLog.print("Gauss-Seidel"); mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Return results res = new ModelCheckerResult(); res.soln = soln; @@ -1116,6 +1130,13 @@ public class MDPModelChecker extends ProbModelChecker mainLog.print("Value iteration (" + (min ? "min" : "max") + ")"); mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Return results res = new ModelCheckerResult(); res.soln = soln; diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 20e55b5f..579bf4fa 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -545,6 +545,13 @@ public class STPGModelChecker extends ProbModelChecker mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); } + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Print adversary if (genAdv) { PrismLog out = new PrismFileLog(exportAdvFilename); @@ -637,6 +644,13 @@ public class STPGModelChecker extends ProbModelChecker mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); } + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Return results res = new ModelCheckerResult(); res.soln = soln; @@ -943,6 +957,13 @@ public class STPGModelChecker extends ProbModelChecker mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); } + // Non-convergence is an error + if (!done) { + String msg = "Iterative method did not converge within " + iters + " iterations."; + msg += "\nConsider using a different numerical method or increasing the maximum number of iterations"; + throw new PrismException(msg); + } + // Return results res = new ModelCheckerResult(); res.soln = soln;