s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

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
master
Dave Parker 12 years ago
parent
879cdc5ab0
commit
ad7e014079
4 changed files with 43 additions and 22 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      prism/src/explicit/DTMCModelChecker.java
  2. 17
      prism/src/explicit/MDPModelChecker.java
  3. 20
      prism/src/explicit/ProbModelChecker.java
  4. 12
      prism/src/explicit/STPGModelChecker.java

16
prism/src/explicit/DTMCModelChecker.java
View File

@ -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);

17
prism/src/explicit/MDPModelChecker.java
View File

@ -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);

20
prism/src/explicit/ProbModelChecker.java
View File

@ -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

12
prism/src/explicit/STPGModelChecker.java
View File

@ -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);

Write Preview
Loading…
Cancel
Save