From 87489f7adc8454fdb1b06f1889232bb676258f92 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 6 Mar 2018 11:12:43 +0100
Subject: [PATCH] ExportIterations: Export steady-state BSCC iterations to
 individual HTML files

---
 prism/src/explicit/DTMCModelChecker.java | 14 ++++++++++++++
 prism/src/prism/ProbModelChecker.java    | 10 ++++++++++
 2 files changed, 24 insertions(+)

diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index c6278830..fffdffef 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -2365,6 +2365,12 @@ public class DTMCModelChecker extends ProbModelChecker
 		for (int i = bscc.nextSetBit(0); i >= 0; i = bscc.nextSetBit(i + 1))
 			soln[i] = soln2[i] = equiprob;
 
+		ExportIterations iterationsExport = null;
+		if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
+			iterationsExport = ExportIterations.createWithUniqueFilename("Explicit DTMC BSCC steady state value iteration", "iterations-ss-bscc");
+			iterationsExport.exportVector(soln);
+		}
+
 		// Start iterations
 		int iters = 0;
 		boolean done = false;
@@ -2378,12 +2384,20 @@ public class DTMCModelChecker extends ProbModelChecker
 			double[] tmpsoln = soln;
 			soln = soln2;
 			soln2 = tmpsoln;
+
+			if (iterationsExport != null) {
+				iterationsExport.exportVector(soln);
+			}
 		}
 
 		// Finished value iteration
 		watch.stop();
 		mainLog.println("Value iteration took " + iters + " iterations and " + watch.elapsedSeconds() + " 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/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index 71305916..47820d92 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/prism/src/prism/ProbModelChecker.java
@@ -61,6 +61,7 @@ import parser.type.TypePathDouble;
 import prism.LTLModelChecker.LTLProduct;
 import sparse.PrismSparse;
 import dv.DoubleVector;
+import explicit.ExportIterations;
 
 /*
  * Model checker for DTMCs.
@@ -2569,6 +2570,11 @@ public class ProbModelChecker extends NonProbModelChecker
 		JDD.Ref(bscc);
 		init = JDD.Apply(JDD.DIVIDE, bscc, JDD.Constant(n));
 
+		if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
+			String filename = ExportIterations.getUniqueFilename("iterations-ss-bscc");
+			PrismNative.setDefaultExportIterationsFilename(filename);
+		}
+
 		// compute remaining probabilities
 		mainLog.println("\nComputing probabilities...");
 		mainLog.println("Engine: " + Prism.getEngineString(engine));
@@ -2593,6 +2599,10 @@ public class ProbModelChecker extends NonProbModelChecker
 			JDD.Deref(trf);
 			JDD.Deref(init);
 			throw e;
+		} finally {
+			if (settings.getBoolean(PrismSettings.PRISM_EXPORT_ITERATIONS)) {
+				PrismNative.setDefaultExportIterationsFilename(ExportIterations.getDefaultFilename());
+			}
 		}
 
 		// derefs