Fixing bug due to refactoring/moving of code in the previous commit to handle apps...

[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 9ce2c3dea6bffb7bdd0501604478e3b48ff12549..11d44ab8e0c8643bbd5726ac42470eaf03d653a9 100755 (executable)
--- 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
@@ -681,6 +681,13 @@ public class DPORStateReducer extends ListenerAdapter {
       transition = new TransitionEvent();
       currentExecution.addTransition(transition);
       transition.recordPredecessor(currentExecution, choiceCounter - 1);
+      // We have to check if there is a transition whose source state ID is the same
+      // If such exists, then we need to add its predecessors to the predecessor set of the current transition
+      for (TransitionEvent trans : rGraph.getReachableTransitionsAtState(stateId)) {
+        for (Predecessor pred : trans.getPredecessors()) {
+          transition.recordPredecessor(pred.getExecution(), pred.getChoice());
+        }
+      }
     }
     transition.setExecution(currentExecution);
     transition.setTransitionCG(icsCG);
@@ -722,7 +729,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 +757,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) {
+      // We perform updates on backtrack sets for every
       if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
-        return true;
+        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 +780,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 +990,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 +1099,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;
     }
@@ -1148,32 +1166,33 @@ public class DPORStateReducer extends ListenerAdapter {
       int newConflictChoice = conflictChoice;
       Execution newConflictExecution = conflictExecution;
       // Check if a conflict is found
-      if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) {
+      ReadWriteSet newCurrRWSet = currRWSet.getCopy();
+      if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) {
         createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice);
         newConflictChoice = predecessorChoice;
         newConflictExecution = predecessorExecution;
       }
       // Continue performing DFS if conflict is not found
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
-              currRWSet, visited);
+              newCurrRWSet, visited);
     }
   }
 
   // --- 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);
       }
     }
   }