Adding a counter for number of conflicts.
authorrtrimana <rtrimana@uci.edu>
Sun, 12 Apr 2020 07:21:43 +0000 (00:21 -0700)
committerrtrimana <rtrimana@uci.edu>
Sun, 12 Apr 2020 07:21:43 +0000 (00:21 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index a352864..22cc82f 100644 (file)
@@ -88,7 +88,8 @@ public class DPORStateReducer extends ListenerAdapter {
   private boolean isEndOfExecution;
 
   // Statistics
-  private int numOfTransitions;        
+  private int numOfConflicts;
+  private int numOfTransitions;
        
   public DPORStateReducer(Config config, JPF jpf) {
     verboseMode = config.getBoolean("printout_state_transition", false);
@@ -99,6 +100,7 @@ public class DPORStateReducer extends ListenerAdapter {
       out = null;
     }
     isBooleanCGFlipped = false;
+               numOfConflicts = 0;
                numOfTransitions = 0;
     restorableStateMap = new HashMap<>();
     initializeStatesVariables();
@@ -165,9 +167,14 @@ public class DPORStateReducer extends ListenerAdapter {
 
   @Override
   public void searchFinished(Search search) {
+    if (stateReductionMode) {
+      // Number of conflicts = first trace + subsequent backtrack points
+      numOfConflicts += 1 + doneBacktrackSet.size();
+    }
     if (verboseMode) {
       out.println("\n==> DEBUG: ----------------------------------- search finished");
       out.println("\n==> DEBUG: State reduction mode  : " + stateReductionMode);
+      out.println("\n==> DEBUG: Number of conflicts   : " + numOfConflicts);
       out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
     }
@@ -212,6 +219,8 @@ public class DPORStateReducer extends ListenerAdapter {
         if (!isBooleanCGFlipped) {
           isBooleanCGFlipped = true;
         } else {
+          // Number of conflicts = first trace + subsequent backtrack points
+          numOfConflicts = 1 + doneBacktrackSet.size();
           // Allocate new objects for data structure when the boolean is flipped from "false" to "true"
           initializeStatesVariables();
         }