From ad7e014079bf4fc1972d162bd488c39bb1cf92a5 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 1 Oct 2013 14:59:13 +0000 Subject: [PATCH] Fix modified policy iteration (and add internal option to explicit state model checkers to not flag non-convergence as an error). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7498 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 16 ++++++++-------- prism/src/explicit/MDPModelChecker.java | 17 +++++++++-------- prism/src/explicit/ProbModelChecker.java | 20 ++++++++++++++++++++ prism/src/explicit/STPGModelChecker.java | 12 ++++++------ 4 files changed, 43 insertions(+), 22 deletions(-) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 2a0ebaff..aa468ff7 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -955,8 +955,8 @@ 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) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); @@ -1039,8 +1039,8 @@ 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) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); @@ -1326,8 +1326,8 @@ 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) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); @@ -1583,8 +1583,8 @@ 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) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 6106c7cc..c11d1a59 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -840,8 +840,8 @@ 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) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); @@ -927,8 +927,8 @@ 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) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); @@ -1068,6 +1068,7 @@ public class MDPModelChecker extends ProbModelChecker // Limit iters for DTMC solution - this implements "modified" policy iteration mcDTMC.setMaxIters(100); + mcDTMC.setErrorOnNonConverge(false); // Store num states n = mdp.getNumStates(); @@ -1488,8 +1489,8 @@ 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) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); @@ -1576,8 +1577,8 @@ public class MDPModelChecker extends ProbModelChecker mainLog.print("Gauss-Seidel (" + (min ? "min" : "max") + ")"); mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); - // Non-convergence is an error - if (!done) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 9ed36d99..c528eae5 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -67,6 +67,8 @@ public class ProbModelChecker extends NonProbModelChecker protected ValIterDir valIterDir = ValIterDir.BELOW; // Method used for numerical solution protected SolnMethod solnMethod = SolnMethod.VALUE_ITERATION; + // Is non-convergence of an iterative method an error? + protected boolean errorOnNonConverge = true; // Adversary export protected boolean exportAdv = false; protected String exportAdvFilename; @@ -233,6 +235,7 @@ public class ProbModelChecker extends NonProbModelChecker setProb1(other.getProb1()); setValIterDir(other.getValIterDir()); setSolnMethod(other.getSolnMethod()); + setErrorOnNonConverge(other.geterrorOnNonConverge()); } /** @@ -251,6 +254,7 @@ public class ProbModelChecker extends NonProbModelChecker mainLog.print("prob1 = " + prob1 + " "); mainLog.print("valIterDir = " + valIterDir + " "); mainLog.print("solnMethod = " + solnMethod + " "); + mainLog.print("errorOnNonConverge = " + errorOnNonConverge + " "); } // Set methods for flags/settings @@ -343,6 +347,14 @@ public class ProbModelChecker extends NonProbModelChecker this.solnMethod = solnMethod; } + /** + * Set whether non-convergence of an iterative method an error + */ + public void setErrorOnNonConverge(boolean errorOnNonConverge) + { + this.errorOnNonConverge = errorOnNonConverge; + } + public void setExportAdv(boolean exportAdv) { this.exportAdv = exportAdv; @@ -410,6 +422,14 @@ public class ProbModelChecker extends NonProbModelChecker return solnMethod; } + /** + * Is non-convergence of an iterative method an error? + */ + public boolean geterrorOnNonConverge() + { + return errorOnNonConverge; + } + // Model checking functions @Override diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 0351eb94..8ac7ce33 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -630,8 +630,8 @@ public class STPGModelChecker extends ProbModelChecker mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); } - // Non-convergence is an error - if (!done) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); @@ -729,8 +729,8 @@ public class STPGModelChecker extends ProbModelChecker mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); } - // Non-convergence is an error - if (!done) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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); @@ -1042,8 +1042,8 @@ public class STPGModelChecker extends ProbModelChecker mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); } - // Non-convergence is an error - if (!done) { + // Non-convergence is an error (usually) + if (!done && errorOnNonConverge) { 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);