From: rtrimana <rtrimana@uci.edu>
Date: Thu, 28 Jan 2021 21:39:56 +0000 (-0800)
Subject: Adding a counter for unique transitions.
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=98c46e5011b7212deb87896a3ac764ae786c4ea0

Adding a counter for unique transitions.
---

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index a750c4d..9a4af0c 100755
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -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++;
+      }
     }
   }