From e13f09f0caa5d03927bc000f9a80cdc12ddd30ea Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 15 Nov 2011 23:30:57 +0000 Subject: [PATCH] Explicit model checkers should throw an exception when iterative numerical methods do not converge within maxIters. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4166 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 28 ++++++++++++++++++++++++ prism/src/explicit/MDPModelChecker.java | 21 ++++++++++++++++++ prism/src/explicit/STPGModelChecker.java | 21 ++++++++++++++++++ 3 files changed, 70 insertions(+) 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;