Adding a counter for number of conflicts.

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index a35286454e3025d6311d0b50c72cb7ab0f538082..22cc82f859545e3e2bdf1d778cdc06c191d34b41 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -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();
         }