ExportIterations: Support for generating unique filenames (for multiple iterations during the same PRISM run)

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;