From 6e9f7cf97a62d88f27abcfc4fe89f9f78e3a5f02 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 6 Mar 2018 11:12:42 +0100
Subject: [PATCH] ExportIterations: Support for generating unique filenames
 (for multiple iterations during the same PRISM run)

---
 prism/src/explicit/ExportIterations.java | 27 ++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/prism/src/explicit/ExportIterations.java b/prism/src/explicit/ExportIterations.java
index 54c874c5..9b353800 100644
--- a/prism/src/explicit/ExportIterations.java
+++ b/prism/src/explicit/ExportIterations.java
@@ -26,6 +26,8 @@
 
 package explicit;
 
+import java.util.HashMap;
+
 import dv.DoubleVector;
 import prism.PrismException;
 import prism.PrismFileLog;
@@ -41,6 +43,9 @@ public class ExportIterations {
 
 	private PrismLog log;
 
+	/** A hashmap for generating unique filenames */
+	private static HashMap<String, Integer> counts = new HashMap<>();
+
 	public ExportIterations(String title) throws PrismException
 	{
 		this(title, PrismFileLog.create(defaultFilename));
@@ -152,6 +157,28 @@ public class ExportIterations {
 		log.flush();
 	}
 
+	/**
+	 * Get a unique HTML file name with the given prefix, of the form
+	 * 'prefix-counter.html', where counter starts with 0 and
+	 * is incremented each time a unique filename with the same prefix is
+	 * requested.
+	 */
+	public static String getUniqueFilename(String prefix)
+	{
+		int count = counts.getOrDefault(prefix, 0);
+		counts.put(prefix, count+1);
+		return prefix + "-" + count + ".html";
+	}
+
+	/**
+	 * Create an ExportIterations helper with a unique filename generated
+	 * from {@code prefix} (see getUniqueFilename).
+	 */
+	public static ExportIterations createWithUniqueFilename(String title, String prefix) throws PrismException
+	{
+		return new ExportIterations(title, PrismFileLog.create(getUniqueFilename(prefix)));
+	}
+
 	public static void setDefaultFilename(String newDefaultFilename)
 	{
 		defaultFilename = newDefaultFilename;