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

(export-iterations) Explicit engine (DTMC/MDP): If enabled, export iterations to HTML file 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12077 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
00a5721cbe
commit
1fc8dfa9c4
2 changed files with 92 additions and 0 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. 46
      prism/src/explicit/DTMCModelChecker.java
  2. 46
      prism/src/explicit/MDPModelChecker.java

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

@ -41,6 +41,7 @@ import prism.Prism;
import prism.PrismComponent;
import prism.PrismException;
import prism.PrismFileLog;
import prism.PrismSettings;
import prism.PrismUtils;
import acceptance.AcceptanceReach;
import acceptance.AcceptanceType;
@ -960,6 +961,11 @@ public class DTMCModelChecker extends ProbModelChecker
timer = System.currentTimeMillis();
mainLog.println("Starting value iteration...");
ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit DTMC ReachProbs value iteration");
}
// Store num states
n = dtmc.getNumStates();
@ -992,6 +998,9 @@ public class DTMCModelChecker extends ProbModelChecker
if (known != null)
unknown.andNot(known);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Start iterations
iters = 0;
done = false;
@ -999,6 +1008,10 @@ public class DTMCModelChecker extends ProbModelChecker
iters++;
// Matrix-vector multiply
dtmc.mvMult(soln, soln2, unknown, false);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Check termination
done = PrismUtils.doublesAreClose(soln, soln2, termCritParam, termCrit == TermCrit.ABSOLUTE);
// Swap vectors for next iter
@ -1012,6 +1025,9 @@ public class DTMCModelChecker extends ProbModelChecker
mainLog.print("Value iteration");
mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
if (iterationsExport != null)
iterationsExport.close();
// Non-convergence is an error (usually)
if (!done && errorOnNonConverge) {
String msg = "Iterative method did not converge within " + iters + " iterations.";
@ -1049,6 +1065,11 @@ public class DTMCModelChecker extends ProbModelChecker
timer = System.currentTimeMillis();
mainLog.println("Starting Gauss-Seidel...");
ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit DTMC ReachProbs Gauss Seidel value iteration");
}
// Store num states
n = dtmc.getNumStates();
@ -1080,6 +1101,9 @@ public class DTMCModelChecker extends ProbModelChecker
if (known != null)
unknown.andNot(known);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Start iterations
iters = 0;
done = false;
@ -1087,6 +1111,10 @@ public class DTMCModelChecker extends ProbModelChecker
iters++;
// Matrix-vector multiply
maxDiff = dtmc.mvMultGS(soln, unknown, false, termCrit == TermCrit.ABSOLUTE);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Check termination
done = maxDiff < termCritParam;
}
@ -1096,6 +1124,9 @@ public class DTMCModelChecker extends ProbModelChecker
mainLog.print("Gauss-Seidel");
mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
if (iterationsExport != null)
iterationsExport.close();
// Non-convergence is an error (usually)
if (!done && errorOnNonConverge) {
String msg = "Iterative method did not converge within " + iters + " iterations.";
@ -1341,6 +1372,11 @@ public class DTMCModelChecker extends ProbModelChecker
timer = System.currentTimeMillis();
mainLog.println("Starting value iteration...");
ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit DTMC ReachRewards value iteration");
}
// Store num states
n = dtmc.getNumStates();
@ -1371,6 +1407,9 @@ public class DTMCModelChecker extends ProbModelChecker
if (known != null)
unknown.andNot(known);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Start iterations
iters = 0;
done = false;
@ -1379,6 +1418,10 @@ public class DTMCModelChecker extends ProbModelChecker
iters++;
// Matrix-vector multiply
dtmc.mvMultRew(soln, mcRewards, soln2, unknown, false);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Check termination
done = PrismUtils.doublesAreClose(soln, soln2, termCritParam, termCrit == TermCrit.ABSOLUTE);
// Swap vectors for next iter
@ -1392,6 +1435,9 @@ public class DTMCModelChecker extends ProbModelChecker
mainLog.print("Value iteration");
mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
if (iterationsExport != null)
iterationsExport.close();
// Non-convergence is an error (usually)
if (!done && errorOnNonConverge) {
String msg = "Iterative method did not converge within " + iters + " iterations.";

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

@ -46,6 +46,7 @@ import prism.PrismException;
import prism.PrismFileLog;
import prism.PrismLog;
import prism.PrismNotSupportedException;
import prism.PrismSettings;
import prism.PrismUtils;
import strat.MDStrategyArray;
import acceptance.AcceptanceReach;
@ -702,6 +703,11 @@ public class MDPModelChecker extends ProbModelChecker
timer = System.currentTimeMillis();
mainLog.println("Starting value iteration (" + (min ? "min" : "max") + ")...");
ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit ReachRewards value iteration");
}
// Store num states
n = mdp.getNumStates();
@ -734,6 +740,9 @@ public class MDPModelChecker extends ProbModelChecker
if (known != null)
unknown.andNot(known);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Start iterations
iters = 0;
done = false;
@ -741,6 +750,10 @@ public class MDPModelChecker extends ProbModelChecker
iters++;
// Matrix-vector multiply and min/max ops
mdp.mvMultMinMax(soln, min, soln2, unknown, false, strat);
if (iterationsExport != null)
iterationsExport.exportVector(soln2, 0);
// Check termination
done = PrismUtils.doublesAreClose(soln, soln2, termCritParam, termCrit == TermCrit.ABSOLUTE);
// Swap vectors for next iter
@ -754,6 +767,9 @@ public class MDPModelChecker extends ProbModelChecker
mainLog.print("Value iteration (" + (min ? "min" : "max") + ")");
mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
if (iterationsExport != null)
iterationsExport.close();
// Non-convergence is an error (usually)
if (!done && errorOnNonConverge) {
String msg = "Iterative method did not converge within " + iters + " iterations.";
@ -794,6 +810,11 @@ public class MDPModelChecker extends ProbModelChecker
timer = System.currentTimeMillis();
mainLog.println("Starting Gauss-Seidel (" + (min ? "min" : "max") + ")...");
ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit MDP ReachProbs Gauss-Seidel iteration");
}
// Store num states
n = mdp.getNumStates();
@ -825,6 +846,9 @@ public class MDPModelChecker extends ProbModelChecker
if (known != null)
unknown.andNot(known);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Start iterations
iters = 0;
done = false;
@ -832,6 +856,10 @@ public class MDPModelChecker extends ProbModelChecker
iters++;
// Matrix-vector multiply
maxDiff = mdp.mvMultGSMinMax(soln, min, unknown, false, termCrit == TermCrit.ABSOLUTE, strat);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Check termination
done = maxDiff < termCritParam;
}
@ -841,6 +869,9 @@ public class MDPModelChecker extends ProbModelChecker
mainLog.print("Gauss-Seidel");
mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
if (iterationsExport != null)
iterationsExport.close();
// Non-convergence is an error (usually)
if (!done && errorOnNonConverge) {
String msg = "Iterative method did not converge within " + iters + " iterations.";
@ -1605,6 +1636,11 @@ public class MDPModelChecker extends ProbModelChecker
timer = System.currentTimeMillis();
mainLog.println("Starting value iteration (" + (min ? "min" : "max") + ")...");
ExportIterations iterationsExport = null;
if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
iterationsExport = new ExportIterations("Explicit MDP ReachProbs value iteration");
}
// Store num states
n = mdp.getNumStates();
@ -1635,6 +1671,9 @@ public class MDPModelChecker extends ProbModelChecker
if (known != null)
unknown.andNot(known);
if (iterationsExport != null)
iterationsExport.exportVector(soln, 0);
// Start iterations
iters = 0;
done = false;
@ -1643,6 +1682,10 @@ public class MDPModelChecker extends ProbModelChecker
iters++;
// Matrix-vector multiply and min/max ops
mdp.mvMultRewMinMax(soln, mdpRewards, min, soln2, unknown, false, strat);
if (iterationsExport != null)
iterationsExport.exportVector(soln2, 0);
// Check termination
done = PrismUtils.doublesAreClose(soln, soln2, termCritParam, termCrit == TermCrit.ABSOLUTE);
// Swap vectors for next iter
@ -1651,6 +1694,9 @@ public class MDPModelChecker extends ProbModelChecker
soln2 = tmpsoln;
}
if (iterationsExport != null)
iterationsExport.close();
// Finished value iteration
timer = System.currentTimeMillis() - timer;
mainLog.print("Value iteration (" + (min ? "min" : "max") + ")");

Write Preview
Loading…
Cancel
Save