Fixes from review

- Allow stat measurements to be disabled
- More consistent naming of stat objects and methods.
- Move stats measurements at several places to a separate method.

Author: magoorden

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

@@ -1355,44 +1355,52 @@ public void enableMeasurements() {
         	enabled = true;
         }
 
+        public void disableMeasurements() {
+            enabled = false;
+        }
+        
         public void newMeasurement(int newUsedBddNodes) {
             maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes);
         }
 
-        public int getMaxNodes() {
+        public int getMaxUsedNodes() {
         	return maxUsedBddNodes;
         }
     }
 
     /**
-     * Singleton object for maximum BDD nodes statistics.
+     * Singleton object for maximum used BDD nodes statistics.
      */
-    protected MaxUsedBddNodesStats maxbddnodesstats = new MaxUsedBddNodesStats();
+    protected MaxUsedBddNodesStats maxusedbddnodesstats = new MaxUsedBddNodesStats();
 
     /**
-     * <p>Return the current maximum BDD nodes statistics for this BDD factory.</p>
+     * <p>Return the current maximum used BDD nodes statistics for this BDD factory.</p>
      *
-     * @return  maximum memory statistics
+     * @return  maximum used BDD statistics
      */
-    public MaxUsedBddNodesStats getMaxBddNodesStats() {
-        return maxbddnodesstats;
+    public MaxUsedBddNodesStats getMaxUsedBddNodesStats() {
+        return maxusedbddnodesstats;
     }
 
     /**
      * Stores statistics about the maximum memory usage.
      * 
      * @author mgoorden
      */
-    public static class MaxMemoryStats {
+    public static class MaxUsedMemoryStats {
         protected boolean enabled = false;
         protected long maxUsedMemory;
 
-        protected MaxMemoryStats() { }
+        protected MaxUsedMemoryStats() { }
 
         public void enableMeasurements() {
             enabled = true;
         }
 
+        public void disableMeasurements() {
+            enabled = false;
+        }
+        
         public void newMeasurement(long newMemory) {
             maxUsedMemory = Math.max(newMemory, maxUsedMemory);
         }
@@ -1403,50 +1411,55 @@ public long getMaxUsedMemory() {
     }
 
     /**
-     * Singleton object for maximum memory statistics.
+     * Singleton object for maximum used memory statistics.
      */
-    protected MaxMemoryStats maxmemorystats = new MaxMemoryStats();
+    protected MaxUsedMemoryStats maxusedmemorystats = new MaxUsedMemoryStats();
 
     /**
-     * <p>Return the current maximum memory statistics for this BDD factory.</p>
+     * <p>Return the current maximum used memory statistics for this BDD factory.</p>
      * 
-     * <p>Note that measuring max memory usages fluctuates over time, tool 
+     * <p>Note that measuring max used memory usages fluctuates over time, tool 
      * implementation, used hardware, etc.</p>
      *
-     * @return  maximum memory statistics
+     * @return  maximum used memory statistics
      */
-    public MaxMemoryStats getMaxMemoryStats() {
-        return maxmemorystats;
+    public MaxUsedMemoryStats getMaxUsedMemoryStats() {
+        return maxusedmemorystats;
     }
 
     /**
-     * Stores continuously statistics about the memory usage and BDD operations.
+     * 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> contUsedOperations = new ArrayList<Long>();
+        protected List<Long> contOperations = new ArrayList<Long>();
 
         protected ContinuousStats() { }
 
         public void enableMeasurements() {
             enabled = true;
         }
 
+        public void disableMeasurements() {
+            enabled = false;
+        }
+        
         public List<Integer> getNodesStats() {
-            if (contUsedBddNodes.size() != contUsedOperations.size()) {
+            if (contUsedBddNodes.size() != contOperations.size()) {
                 throw new AssertionError("Incorrect data collection.");
             }
             return contUsedBddNodes;
         }
 
         public List<Long> getOperationsStats() {
-            if (contUsedBddNodes.size() != contUsedOperations.size()) {
+            if (contUsedBddNodes.size() != contOperations.size()) {
                 throw new AssertionError("Incorrect data collection.");
             }
-            return contUsedOperations;
+            return contOperations;
         }
     }
 

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

@@ -3522,25 +3522,7 @@ int bdd_used_nodes_count() {
     }
 
     int bdd_delref(int root) {
-        // The number of currently used BDD nodes, between 0 and bddnodesize.
-        // -1 indicates that it has not yet been calculated.
-        int usedBddNodes = -1;
-        
-        if (maxbddnodesstats.enabled) {
-            if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count();
-            maxbddnodesstats.newMeasurement(usedBddNodes);
-        }
-        
-        if (maxmemorystats.enabled) {
-            long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory();
-            maxmemorystats.newMeasurement(memory);
-        }
-        
-        if (continuousstats.enabled) {
-            if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count();
-            continuousstats.contUsedBddNodes.add(usedBddNodes);
-            continuousstats.contUsedOperations.add(cachestats.opMiss);
-        }
+        bdd_add_per_stats();
 
         if (root == INVALID_BDD)
             bdd_error(BDD_BREAK); /* distinctive */
@@ -5069,32 +5051,36 @@ int bdd_reorder_gain() {
     }
 
     public void done() { 
+        bdd_add_per_stats();
+        
+        super.done(); 
+        bdd_done(); 
+    }
+    
+    void bdd_add_per_stats() {
         // The number of currently used BDD nodes, between 0 and bddnodesize.
         // -1 indicates that it has not yet been calculated.
         int usedBddNodes = -1;
 
-        if (maxbddnodesstats.enabled) {
+        if (maxusedbddnodesstats.enabled) {
             if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count();
-            maxbddnodesstats.newMeasurement(usedBddNodes);
+            maxusedbddnodesstats.newMeasurement(usedBddNodes);
         }
 
-        if (maxmemorystats.enabled) {
+        if (maxusedmemorystats.enabled) {
             long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory();
-            maxmemorystats.newMeasurement(memory);
-            System.gc(); // To make sure subsequent memory measurements are accurate.
+            maxusedmemorystats.newMeasurement(memory);
         }
-            
+        
         if (continuousstats.enabled) {
             if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count();
             continuousstats.contUsedBddNodes.add(usedBddNodes);
-            continuousstats.contUsedOperations.add(cachestats.opMiss);
+            // cachestats.opMiss is the number of BDD operations performed until now that could not
+            // be taken from the cache. Thus it approximates time. 
+            continuousstats.contOperations.add(cachestats.opMiss);
         }
-        
-        super.done(); 
-        bdd_done(); 
     }
 
-    
     void bdd_done() {
         /*sanitycheck(); FIXME */
         //bdd_fdd_done();