Merge pull request #2 from magoorden/1-performance-measurement

#1 Added platform-independent performance statistics + other improvements.

- Added the collection of platform-independent performance statistics.
- Added `bdd_used_nodes_count()` that counts the number of used nodes.
- Replaced static `CACHESTATS` by non-static `cachestats.enabled`, which is adaptable by user and configurable per BDD factory instance.
- Removed global JVM shutdown hook, that prints cache statistics to `stdout`, from `JFactory`.
- Cache statistics are now measured using `longs` rather than `ints` to reduce integer overflow issues.
- Added `opAccess` statistic to cache statistics.
- Added functionality to reset statistics.

Author: dhendriks

CHANGES.md

@@ -4,6 +4,13 @@ All notable changes to this project will be documented in this file.
 
 ## [Unreleased]
 * Added CHANGES.md to track changes between releases.
+* Added the collection of platform-independent performance statistics.
+* Added `bdd_used_nodes_count()` that counts the number of used nodes.
+* Replaced static `CACHESTATS` by non-static `cachestats.enabled`, which is adaptable by user and configurable per BDD factory instance.
+* Removed global JVM shutdown hook, that prints cache statistics to `stdout`, from `JFactory`.
+* Cache statistics are now measured using `longs` rather than `ints` to reduce integer overflow issues.
+* Added `opAccess` statistic to cache statistics.
+* Added functionality to reset statistics.
 
 ## [1.0.1] - 2020-03-17
 * Updated SCM URL for proper Maven Central metadata.

src/main/java/com/github/javabdd/BDDFactory.java

@@ -3,6 +3,7 @@
 // Licensed under the terms of the GNU LGPL; see COPYING for details.
 package com.github.javabdd;
 
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.BitSet;
 import java.util.Collection;
@@ -1235,16 +1236,20 @@ public ReorderStats getReorderStats() {
      * Stores statistics about the operator cache.
      * 
      * @author jwhaley
+     * @author sthuijsman
+     * @author mgoorden
      * @version $Id: BDDFactory.java 480 2010-11-16 01:29:49Z robimalik $
      */
     public static class CacheStats {
-        public int uniqueAccess;
-        public int uniqueChain;
-        public int uniqueHit;
-        public int uniqueMiss;
-        public int opHit;
-        public int opMiss;
-        public int swapCount;
+        protected boolean enabled = false;
+        public long uniqueAccess;
+        public long uniqueChain;
+        public long uniqueHit;
+        public long uniqueMiss;
+        public long opAccess;
+        public long opHit;
+        public long opMiss;
+        public long swapCount;
 
         protected CacheStats() { }
 
@@ -1253,11 +1258,31 @@ void copyFrom(CacheStats that) {
             this.uniqueChain = that.uniqueChain;
             this.uniqueHit = that.uniqueHit;
             this.uniqueMiss = that.uniqueMiss;
+            this.opAccess = that.opAccess;
             this.opHit = that.opHit;
             this.opMiss = that.opMiss;
             this.swapCount = that.swapCount;
         }
 
+        public void enableMeasurements() {
+        	enabled = true;
+        }
+        
+        public void disableMeasurements() {
+            enabled = false;
+        }
+        
+        public void resetMeasurements() {
+            uniqueAccess = 0;
+            uniqueChain = 0;
+            uniqueHit = 0;
+            uniqueMiss = 0;
+            opAccess = 0;
+            opHit = 0;
+            opMiss = 0;
+            swapCount = 0;
+        }
+        
         /* (non-Javadoc)
          * @see java.lang.Object#toString()
          */
@@ -1294,6 +1319,9 @@ public String toString() {
             else
                 sb.append((float)0);
             sb.append(newLine);
+            sb.append("Operator Access:  ");
+            sb.append(opAccess);
+            sb.append(newLine);
             sb.append("Operator Hits:  ");
             sb.append(opHit);
             sb.append(newLine);
@@ -1327,6 +1355,107 @@ public CacheStats getCacheStats() {
         return cachestats;
     }
 
+    /**
+     * Stores statistics about the maximum BDD nodes usage.
+     * 
+     * @author mgoorden
+     */
+    public static class MaxUsedBddNodesStats {
+        protected boolean enabled = false;
+        protected int maxUsedBddNodes;
+        
+        protected MaxUsedBddNodesStats() { }
+        
+        public void enableMeasurements() {
+        	enabled = true;
+        }
+        
+        public void disableMeasurements() {
+            enabled = false;
+        }
+        
+        public void resetMeasurements() {
+            maxUsedBddNodes = 0;
+        }
+        
+        public void newMeasurement(int newUsedBddNodes) {
+            maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes);
+        }
+        
+        public int getMaxUsedBddNodes() {
+        	return maxUsedBddNodes;
+        }
+    }
+    
+    /**
+     * Singleton object for maximum used BDD nodes statistics.
+     */
+    protected MaxUsedBddNodesStats maxusedbddnodesstats = new MaxUsedBddNodesStats();
+
+    /**
+     * <p>Return the current maximum used BDD nodes statistics for this BDD factory.</p>
+     *
+     * @return  maximum used BDD nodes statistics
+     */
+    public MaxUsedBddNodesStats getMaxUsedBddNodesStats() {
+        return maxusedbddnodesstats;
+    }
+    
+    /**
+     * Stores continuously statistics about the BDD nodes usage and BDD operations,
+     * where BDD operations is a proxy for time.
+     * 
+     * @author mgoorden
+     */
+    public static class ContinuousStats {
+        protected boolean enabled = false;
+        protected List<Integer> contUsedBddNodes = new ArrayList<Integer>();
+        protected List<Long> contOperations = new ArrayList<Long>();
+        
+        protected ContinuousStats() { }
+
+        public void enableMeasurements() {
+            enabled = true;
+        }
+        
+        public void disableMeasurements() {
+            enabled = false;
+        }
+        
+        public void resetMeasurements() {
+            contUsedBddNodes = new ArrayList<Integer>();
+            contOperations = new ArrayList<Long>();
+        }
+        
+        public List<Integer> getNodesStats() {
+            if (contUsedBddNodes.size() != contOperations.size()) {
+                throw new AssertionError("Incorrect data collection.");
+            }
+            return contUsedBddNodes;
+        }
+        
+        public List<Long> getOperationsStats() {
+            if (contUsedBddNodes.size() != contOperations.size()) {
+                throw new AssertionError("Incorrect data collection.");
+            }
+            return contOperations;
+        }
+    }
+    
+    /**
+     * Singleton object for continuous statistics.
+     */
+    protected ContinuousStats continuousstats = new ContinuousStats();
+    
+    /**
+     * <p>Return the current continuous statistics for this BDD factory.</p>
+     *
+     * @return  continuous statistics
+     */
+    public ContinuousStats getContinuousStats() {
+        return continuousstats;
+    }
+    
     // TODO: bdd_sizeprobe_hook
     // TODO: bdd_reorder_probe