Fixing the counter for unique transitions.

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

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index 6422b7dad5fb464860896adf2f0e65ca2e2289fa..9e232bb31e24dad83b6c9709266ddb061e5f86c8 100755 (executable)
--- 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;
@@ -66,7 +67,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   private HashSet<ClassInfo> nonRelevantClasses;// Class info objects of non-relevant classes
   private HashSet<FieldInfo> nonRelevantFields; // Field info objects of non-relevant fields
   private HashSet<FieldInfo> relevantFields;    // Field info objects of relevant fields
-  private HashMap<Integer, HashSet<Integer>> stateToEventMap;
+  private HashMap<Integer, HashSet<Integer>> stateToEventMap;       // Map state ID to events
   // Data structure to analyze field Read/Write accesses and conflicts
   private HashMap<Integer, LinkedList<BacktrackExecution>> backtrackMap;  // Track created backtracking points
   private PriorityQueue<Integer> backtrackStateQ;                 // Heap that returns the latest state
@@ -84,6 +85,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
 
   // Statistics
   private int numOfTransitions;
+  private HashMap<Integer, HashSet<Integer>> stateToUniqueEventMap;
 
   public DPORStateReducerWithSummary(Config config, JPF jpf) {
     verboseMode = config.getBoolean("printout_state_transition", false);
@@ -109,6 +111,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     relevantFields = new HashSet<>();
     restorableStateMap = new HashMap<>();
     stateToPredInfo = new HashMap<>();
+    stateToUniqueEventMap = new HashMap<>();
     initializeStatesVariables();
   }
 
@@ -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) : " + summarizeUniqueStateIds());
       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 : " + summarizeUniqueStateIds());
       fileWriter.println();
       fileWriter.close();
     }
@@ -196,6 +201,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
         Integer[] cgChoices = icsCG.getAllChoices();
         if (cgChoices.length == 2 && cgChoices[0] == 0 && cgChoices[1] == -1) {
+          // This means the benchmark only has 2 choices, i.e., 0 and -1 which means that it has no events
           stateReductionMode = false;
         }
         isNotCheckedForEventsYet = false;
@@ -259,6 +265,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
           exploreNextBacktrackPoints(vm, icsCG);
         } else {
           numOfTransitions++;
+          countUniqueStateId(vm.getStateId(), icsCG.getNextChoice());
         }
         // Map state to event
         mapStateToEvent(icsCG.getNextChoice());
@@ -270,6 +277,37 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     }
   }
 
+  // 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;
+    }
+
+    return numOfUniqueTransitions;
+  }
+
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
@@ -1337,11 +1375,19 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     Set<Integer> eventChoicesAtStateId = mainSummary.getEventChoicesAtStateId(stateId);
     for (Integer eventChoice : eventChoicesAtStateId) {
       // Get the ReadWriteSet object for this event at state ID
-      ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId);
+      ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId).getCopy();
+      // We have to first check for conflicts between the event and the current transition
+      // Push up one happens-before transition
+      int conflictEventChoice = eventChoice;
+      if (isConflictFound(eventChoice, currExecution, currChoice, rwSet)) {
+        createBacktrackingPoint(eventChoice, currExecution, currChoice);
+        // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+        conflictEventChoice = currExecution.getExecutionTrace().get(currChoice).getChoice();
+      }
       // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
       HashSet<TransitionEvent> visited = new HashSet<>();
       // Update the backtrack sets recursively
-      updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet.getCopy(), visited);
+      updateBacktrackSetDFS(currExecution, currChoice, conflictEventChoice, rwSet, visited);
     }
   }
 }