From 35a177a2fce7cc83df80e5878b4a2e095f873597 Mon Sep 17 00:00:00 2001
From: UCI Networking Group <ucinetworkinggroup@UCIs-MacBook-Pro.local>
Date: Mon, 7 Dec 2020 10:44:11 -0800
Subject: [PATCH] Moving updateBacktrackSetsFromGraph into
 choiceGeneratorAdvanced so that it's always executed after updateBacktrackSet
 following Algorithm 2.

---
 .../nasa/jpf/listener/DPORStateReducer.java   | 37 ++++++++++++-------
 1 file changed, 24 insertions(+), 13 deletions(-)

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 9ce2c3d..a0abd98 100755
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -60,7 +60,7 @@ public class DPORStateReducer extends ListenerAdapter {
   private int choiceCounter;
   private int maxEventChoice;
   // Data structure to track the events seen by each state to track cycles (containing all events) for termination
-  private HashSet<Integer> currVisitedStates;   // States being visited in the current execution
+  private HashMap<Integer,Integer> currVisitedStates; // States visited in the current execution (maps to frequency)
   private HashSet<Integer> justVisitedStates;   // States just visited in the previous choice/event
   private HashSet<Integer> prevVisitedStates;   // States visited in the previous execution
   private HashSet<ClassInfo> nonRelevantClasses;// Class info objects of non-relevant classes
@@ -722,7 +722,7 @@ public class DPORStateReducer extends ListenerAdapter {
     choiceCounter = 0;
     maxEventChoice = 0;
     // Cycle tracking
-    currVisitedStates = new HashSet<>();
+    currVisitedStates = new HashMap<>();
     justVisitedStates = new HashSet<>();
     prevVisitedStates = new HashSet<>();
     stateToEventMap = new HashMap<>();
@@ -750,12 +750,19 @@ public class DPORStateReducer extends ListenerAdapter {
   private boolean terminateCurrentExecution() {
     // We need to check all the states that have just been visited
     // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
+    boolean terminate = false;
     for(Integer stateId : justVisitedStates) {
-      if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
-        return true;
+      // We only flip the value of terminate once ...
+      if (!terminate && prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
+        updateBacktrackSetsFromGraph(stateId);
+        terminate = true;
+      }
+      // If frequency > 1 then this means we have visited this stateId more than once
+      if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
+        updateBacktrackSetsFromGraph(stateId);
       }
     }
-    return false;
+    return terminate;
   }
 
   private void updateStateInfo(Search search) {
@@ -766,11 +773,15 @@ public class DPORStateReducer extends ListenerAdapter {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
-    analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
+    addPredecessorToRevisitedState(search.getVM(), stateId);
     justVisitedStates.add(stateId);
     if (!prevVisitedStates.contains(stateId)) {
       // It is a currently visited states if the state has not been seen in previous executions
-      currVisitedStates.add(stateId);
+      int frequency = 0;
+      if (currVisitedStates.containsKey(stateId)) {
+        frequency = currVisitedStates.get(stateId);
+      }
+      currVisitedStates.put(stateId, frequency + 1);  // Increment frequency counter
     }
   }
 
@@ -972,7 +983,7 @@ public class DPORStateReducer extends ListenerAdapter {
 			icsCG.setDone();
 		}
 		// Save all the visited states when starting a new execution of trace
-		prevVisitedStates.addAll(currVisitedStates);
+		prevVisitedStates.addAll(currVisitedStates.keySet());
 		// This marks a transitional period to the new CG
 		isEndOfExecution = true;
   }
@@ -1081,7 +1092,7 @@ public class DPORStateReducer extends ListenerAdapter {
       choices = icsCG.getAllChoices();
       refChoices = copyChoices(choices);
       // Clear data structures
-      currVisitedStates = new HashSet<>();
+      currVisitedStates = new HashMap<>();
       stateToEventMap = new HashMap<>();
       isEndOfExecution = false;
     }
@@ -1161,19 +1172,19 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // --- Functions related to the reachability analysis when there is a state match
 
-  private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
+  private void addPredecessorToRevisitedState(VM vm, int stateId) {
     // Perform this analysis only when:
     // 1) this is not during a switch to a new execution,
     // 2) at least 2 choices/events have been explored (choiceCounter > 1),
     // 3) state > 0 (state 0 is for boolean CG)
     if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) {
-      if (currVisitedStates.contains(stateId) || prevVisitedStates.contains(stateId)) {
+      if ((currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) ||
+              prevVisitedStates.contains(stateId)) {
         // Update reachable transitions in the graph with a predecessor
         HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
-        for(TransitionEvent transition : reachableTransitions) {
+        for (TransitionEvent transition : reachableTransitions) {
           transition.recordPredecessor(currentExecution, choiceCounter - 1);
         }
-        updateBacktrackSetsFromGraph(stateId);
       }
     }
   }
-- 
2.34.1