Adding a counter for unique transitions.
authorrtrimana <rtrimana@uci.edu>
Thu, 28 Jan 2021 21:39:56 +0000 (13:39 -0800)
committerrtrimana <rtrimana@uci.edu>
Thu, 28 Jan 2021 21:39:56 +0000 (13:39 -0800)
src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java

index a750c4d..9a4af0c 100755 (executable)
@@ -22,6 +22,7 @@ import gov.nasa.jpf.JPF;
 import gov.nasa.jpf.ListenerAdapter;
 import gov.nasa.jpf.jvm.bytecode.INVOKEINTERFACE;
 import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
+import gov.nasa.jpf.report.Publisher;
 import gov.nasa.jpf.search.Search;
 import gov.nasa.jpf.vm.*;
 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
@@ -84,6 +85,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
 
   // Statistics
   private int numOfTransitions;
+  private int numOfUniqueTransitions;
 
   public DPORStateReducerWithSummary(Config config, JPF jpf) {
     verboseMode = config.getBoolean("printout_state_transition", false);
@@ -104,6 +106,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     isNotCheckedForEventsYet = true;
     mainSummary = new MainSummary();
     numOfTransitions = 0;
+    numOfUniqueTransitions = 0;
     nonRelevantClasses = new HashSet<>();
     nonRelevantFields = new HashSet<>();
     relevantFields = new HashSet<>();
@@ -177,12 +180,14 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   public void searchFinished(Search search) {
     if (verboseMode) {
       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: State reduction mode                : " + stateReductionMode);
+      out.println("\n==> DEBUG: Number of transitions               : " + numOfTransitions);
+      out.println("\n==> DEBUG: Number of unique transitions (DPOR) : " + numOfUniqueTransitions);
       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
 
-      fileWriter.println("==> DEBUG: State reduction mode  : " + stateReductionMode);
-      fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
+      fileWriter.println("==> DEBUG: State reduction mode         : " + stateReductionMode);
+      fileWriter.println("==> DEBUG: Number of transitions        : " + numOfTransitions);
+      fileWriter.println("==> DEBUG: Number of unique transitions : " + numOfUniqueTransitions);
       fileWriter.println();
       fileWriter.close();
     }
@@ -260,6 +265,9 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
           exploreNextBacktrackPoints(vm, icsCG);
         } else {
           numOfTransitions++;
+          if (choiceCounter < choices.length) {
+            numOfUniqueTransitions++;
+          }
         }
         // Map state to event
         mapStateToEvent(icsCG.getNextChoice());
@@ -267,7 +275,9 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
         choiceCounter++;
       }
     } else {
-      numOfTransitions++;
+      if (currentCG instanceof IntChoiceFromSet) {
+        numOfTransitions++;
+      }
     }
   }