diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index b50bb357..7d8e6604 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -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."; diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index b8406d23..3b334606 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -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") + ")");