code: //==============================================================================
  //	
  //	Copyright (c) 2016-
  //	Authors:
  //	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
  //	
  //------------------------------------------------------------------------------
  //	
  //	This file is part of PRISM.
  //	
  //	PRISM is free software; you can redistribute it and/or modify
  //	it under the terms of the GNU General Public License as published by
  //	the Free Software Foundation; either version 2 of the License, or
  //	(at your option) any later version.
  //	
  //	PRISM is distributed in the hope that it will be useful,
  //	but WITHOUT ANY WARRANTY; without even the implied warranty of
  //	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  //	GNU General Public License for more details.
  //	
  //	You should have received a copy of the GNU General Public License
  //	along with PRISM; if not, write to the Free Software Foundation,
  //	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
  //	
  //==============================================================================
  
  package explicit;
  
  import java.util.HashMap;
  
  import dv.DoubleVector;
  import prism.PrismException;
  import prism.PrismFileLog;
  import prism.PrismLog;
  
  /**
   * Class for exporting / visualising the value vectors in
   * a numerical iteration algorithm.
   *
   */
  public class ExportIterations {
  	private static String defaultFilename = "iterations.html";
  
  	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));
  	}
  
  	/**
  	 * Constructor.
  	 * @param log the log used for export
  	 */
  	public ExportIterations(String title, PrismLog log)
  	{
  		this.log = log;
  
  		log.println("<!DOCTYPE html>");
  		log.println("<html><head>");
  		log.println("<meta charset=\"utf-8\">");
  		log.println("<!-- HTML file automatically generated by the PRISM model checker -->");
  		log.println("<!-- For visualising the individual steps of a value iteration computation -->");
  		log.println("<!-- Loads supporting Javascript and CSS from www.prismmodelchecker.org -->");
  		log.println("<title>" + title + "</title>");
  		log.println("<link rel='stylesheet' href='https://www.prismmodelchecker.org/js/res/iteration-vis-v1.css'>");
  		log.println("<script src=\"https://www.prismmodelchecker.org/js/res/d3.js-v4/d3.min.js\"></script>");
  		log.println("<body onload='init();'>");
  		log.println("<h1>" + title + "</h1>");
  		log.println("<svg></svg>");
  		log.println("<script src=\"https://www.prismmodelchecker.org/js/res/iteration-vis-v1.js\"></script>");
  		log.flush();
  	}
  
  	/**
  	 * Returns the name of the file used for exporting,
  	 * or {@code null} if it can not be determined.
  	 */
  	public String getFileName()
  	{
  		if (log instanceof PrismFileLog) {
  			return ((PrismFileLog)log).getFileName();
  		}
  		return null;
  	}
  
  	/**
  	 * Export the given vector.
  	 * @param soln the value vector
  	 */
  	public void exportVector(double[] soln)
  	{
  		exportVector(soln, 0);
  	}
  
  	/**
  	 * Export the given vector.
  	 * @param soln the value vector
  	 * @param type the vector type (0 = normal, VI from below, 1 = VI from above)
  	 */
  	public void exportVector(double[] soln, int type)
  	{
  		log.print("<script>addVector([");
  		for (int i = 0; i < soln.length; i++) {
  			if (i>0) log.print(",");
  			double d = soln[i];
  			exportValue(d);
  		}
  		log.print("]," + type + ")</script>\n");
  		log.flush();
  	}
  
  	/**
  	 * Export the given vector.
  	 * @param soln the value vector
  	 */
  	public void exportVector(DoubleVector soln)
  	{
  		exportVector(soln, 0);
  	}
  
  	/**
  	 * Export the given vector.
  	 * @param soln the value vector
  	 * @param type the vector type (0 = normal, VI from below, 1 = VI from above)
  	 */
  	public void exportVector(DoubleVector soln, int type)
  	{
  		log.print("<script>addVector([");
  		for (int i = 0, n = soln.getSize(); i < n; i++) {
  			if (i>0) log.print(",");
  			double d = soln.getElement(i);
  			exportValue(d);
  		}
  		log.print("]," + type + ")</script>\n");
  		log.flush();
  	}
  
  	private void exportValue(double d)
  	{
  		if (d == Double.POSITIVE_INFINITY) {
  			log.print("Infinity");
  		} else if (d == Double.NEGATIVE_INFINITY) {
  			log.print("-Infinity");
  		} else {
  			log.print(d);
  		}
  	}
  
  	/** Print footer, export log */
  	public void close()
  	{
  		log.println("\n</body></html>");
  		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;
  	}
  
  	public static String getDefaultFilename()
  	{
  		return defaultFilename;
  	}
  
  	public static void resetDefaultFilename()
  	{
  		defaultFilename = "iterations.html";
  	}
  }
  