From 90fa90e5dab492d7e034e16f26f69015bd3c39fe Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 20 Nov 2017 17:57:25 +0100
Subject: [PATCH] explicit.ExportIterations: add flush() for useful
 iterations.html

If there are exceptions during the iteration, we want to have a working HTML file with the iterations up to that point.

By flushing after each vector, we can ensure that the HTML is in a working state.
---
 prism/src/explicit/ExportIterations.java | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/prism/src/explicit/ExportIterations.java b/prism/src/explicit/ExportIterations.java
index 04e658ef..196177bb 100644
--- a/prism/src/explicit/ExportIterations.java
+++ b/prism/src/explicit/ExportIterations.java
@@ -67,6 +67,7 @@ public class ExportIterations {
 		log.println("<h1>" + title + "</h1>");
 		log.println("<svg></svg>");
 		log.println("<script src=\"http://www.prismmodelchecker.org/js/res/iteration-vis-v1.js\"></script>");
+		log.flush();
 	}
 
 	/**
@@ -92,6 +93,7 @@ public class ExportIterations {
 			exportValue(d);
 		}
 		log.print("]," + type + ")</script>\n");
+		log.flush();
 	}
 
 	/**
@@ -117,6 +119,7 @@ public class ExportIterations {
 			exportValue(d);
 		}
 		log.print("]," + type + ")</script>\n");
+		log.flush();
 	}
 
 	private void exportValue(double d)
@@ -134,6 +137,7 @@ public class ExportIterations {
 	public void close()
 	{
 		log.println("\n</body></html>");
+		log.flush();
 	}
 
 	public static void setDefaultFilename(String newDefaultFilename)