From 4752262c2622ef8621d8cc09f90ec56cfa705b7c Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:25:01 +0200
Subject: [PATCH] JDD: add statisticsForDD(), printing CSV data about the
 number of nodes per level of a dd

---
 prism/src/jdd/JDD.java | 84 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)

diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java
index f329955d..dabf5f1e 100644
--- a/prism/src/jdd/JDD.java
+++ b/prism/src/jdd/JDD.java
@@ -30,6 +30,8 @@ package jdd;
 
 import java.util.*;
 
+import prism.PrismException;
+import prism.PrismFileLog;
 import prism.PrismLog;
 
 public class JDD
@@ -1773,6 +1775,88 @@ public class JDD
 			throw new CuddOutOfMemoryException();
 	}
 
+	/**
+	 * Write statistics about the different layers of a BDD (JDDNode) to a file.
+	 * The output consists of CSV lines
+	 * <br>
+	 *  index,variable-name,number-of-nodes-for-this-level
+	 * <br>
+	 * The last line is for the constants, with a variable name of 'constants'.
+	 *
+	 * <br>[ DEREFS: <i>none</i> ]
+	 * @param filename the file
+	 * @param dd the root of the BDD
+	 * @param varNames names for the variables for a given index (optional, may be {@code null})
+	 */
+	public static void statisticsForDD(String filename, JDDNode dd, Vector<String> varNames) throws PrismException {
+		try (PrismLog log = PrismFileLog.create(filename)) {
+			statisticsForDD(log, dd, varNames);
+		}
+	}
+
+	/**
+	 * Write statistics about the different layers of a BDD (JDDNode) to a PrismLog.
+	 * The output consists of CSV lines
+	 * <br>
+	 *  index,variable-name,number-of-nodes-for-this-level
+	 * <br>
+	 * The last line is for the constants, with a variable name of 'constants'.
+	 *
+	 * <br>[ DEREFS: <i>none</i> ]
+	 * @param log the PrismLog
+	 * @param dd the root of the BDD
+	 * @param varNames names for the variables for a given index (optional, may be {@code null})
+	 */
+	public static void statisticsForDD(PrismLog log, JDDNode dd, Vector<String> varNames)
+	{
+		HashSet<Long> seen = new HashSet<Long>();
+		HashMap<Integer, Integer> countPerIndex = new HashMap<Integer,Integer>();
+		int constantCount = 0;
+
+		Stack<JDDNode> todo = new Stack<JDDNode>();
+		todo.push(dd);
+
+		int maxIndex = 0;
+		while (!todo.isEmpty()) {
+			JDDNode cur = todo.pop();
+			if (seen.contains(cur.ptr()))
+				continue;
+			seen.add(cur.ptr());
+
+			if (cur.isConstant()) {
+				constantCount++;
+			} else {
+				int index = cur.getIndex();
+				maxIndex = Math.max(maxIndex, index);
+				if (countPerIndex.containsKey(index)) {
+					countPerIndex.put(index, countPerIndex.get(index)+1);
+				} else {
+					countPerIndex.put(index, 1);
+				}
+
+				todo.push(cur.getThen());
+				todo.push(cur.getElse());
+			}
+		}
+
+		for (int index = 0; index <= maxIndex; index++) {
+			Integer count = countPerIndex.get(index);
+			if (count == null) count = 0;
+
+			String name = "";
+			try {
+				if (varNames != null)
+					name = varNames.get(index);
+			} catch (ArrayIndexOutOfBoundsException exception) {
+				// name does not exist, ignore
+			}
+
+			log.println(index+","+name+","+count);
+		}
+		log.println((maxIndex+1)+",constants,"+constantCount);
+	}
+
+
 }
 
 //------------------------------------------------------------------------------