X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerWithSummary.java;fp=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerWithSummary.java;h=08ae9a64c380d14c2e192bdf30a79638eab257bd;hb=cf7ff2a3eae7f0a5b8c214259e0902d5fab646d6;hp=9e232bb31e24dad83b6c9709266ddb061e5f86c8;hpb=5b5f4e395544de9213d47ac5ab2106d2cae2f4b3;p=jpf-core.git

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index 9e232bb..08ae9a6 100755
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -179,15 +179,16 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   @Override
   public void searchFinished(Search search) {
     if (verboseMode) {
+      int summaryOfUniqueTransitions = summarizeUniqueTransitions();
       out.println("\n==> DEBUG: ----------------------------------- search finished");
       out.println("\n==> DEBUG: State reduction mode                : " + stateReductionMode);
       out.println("\n==> DEBUG: Number of transitions               : " + numOfTransitions);
-      out.println("\n==> DEBUG: Number of unique transitions (DPOR) : " + summarizeUniqueStateIds());
+      out.println("\n==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
 
-      fileWriter.println("==> DEBUG: State reduction mode         : " + stateReductionMode);
-      fileWriter.println("==> DEBUG: Number of transitions        : " + numOfTransitions);
-      fileWriter.println("==> DEBUG: Number of unique transitions : " + summarizeUniqueStateIds());
+      fileWriter.println("==> DEBUG: State reduction mode                : " + stateReductionMode);
+      fileWriter.println("==> DEBUG: Number of transitions               : " + numOfTransitions);
+      fileWriter.println("==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
       fileWriter.println();
       fileWriter.close();
     }
@@ -264,6 +265,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
         if (choiceCounter > 0 && terminateCurrentExecution()) {
           exploreNextBacktrackPoints(vm, icsCG);
         } else {
+          // We only count IntChoiceFromSet CGs
           numOfTransitions++;
           countUniqueStateId(vm.getStateId(), icsCG.getNextChoice());
         }
@@ -273,39 +275,11 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
         choiceCounter++;
       }
     } else {
-      numOfTransitions++;
-    }
-  }
-
-  // Count unique state IDs
-  private void countUniqueStateId(int stateId, int nextChoiceValue) {
-    HashSet<Integer> events;
-    // Get the set of events
-    if (!stateToUniqueEventMap.containsKey(stateId)) {
-      events = new HashSet<>();
-      stateToUniqueEventMap.put(stateId, events);
-    } else {
-      events = stateToUniqueEventMap.get(stateId);
-    }
-    // Insert the event
-    if (!events.contains(nextChoiceValue)) {
-      events.add(nextChoiceValue);
-    }
-  }
-
-  // Summarize unique state IDs
-  private int summarizeUniqueStateIds() {
-    // Just count the set size of each of entry map and sum them up
-    int numOfUniqueTransitions = 0;
-    for (Map.Entry<Integer,HashSet<Integer>> entry : stateToUniqueEventMap.entrySet()) {
-      numOfUniqueTransitions = numOfUniqueTransitions + entry.getValue().size();
-    }
-    // We also need to count root and boolean CG if this is in state reduction mode (DPOR)
-    if (stateReductionMode) {
-      numOfUniqueTransitions = numOfUniqueTransitions + 3;
+      // We only count IntChoiceFromSet CGs
+      if (currentCG instanceof IntChoiceFromSet) {
+        numOfTransitions++;
+      }
     }
-
-    return numOfUniqueTransitions;
   }
 
   @Override
@@ -834,6 +808,34 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     return transition;
   }
 
+  // --- Functions related to statistics counting
+  // Count unique state IDs
+  private void countUniqueStateId(int stateId, int nextChoiceValue) {
+    HashSet<Integer> events;
+    // Get the set of events
+    if (!stateToUniqueEventMap.containsKey(stateId)) {
+      events = new HashSet<>();
+      stateToUniqueEventMap.put(stateId, events);
+    } else {
+      events = stateToUniqueEventMap.get(stateId);
+    }
+    // Insert the event
+    if (!events.contains(nextChoiceValue)) {
+      events.add(nextChoiceValue);
+    }
+  }
+
+  // Summarize unique state IDs
+  private int summarizeUniqueTransitions() {
+    // Just count the set size of each of entry map and sum them up
+    int numOfUniqueTransitions = 0;
+    for (Map.Entry<Integer,HashSet<Integer>> entry : stateToUniqueEventMap.entrySet()) {
+      numOfUniqueTransitions = numOfUniqueTransitions + entry.getValue().size();
+    }
+
+    return numOfUniqueTransitions;
+  }
+
   // --- Functions related to cycle detection and reachability graph
 
   // Detect cycles in the current execution/trace