Cleaning up DPORStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
old mode 100644 (file)
new mode 100755 (executable)
index 5b0359e..9ce2c3d
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -1123,41 +1123,9 @@ public class DPORStateReducer extends ListenerAdapter {
     // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
     HashSet<TransitionEvent> visited = new HashSet<>();
     // Update backtrack set recursively
     // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
     HashSet<TransitionEvent> visited = new HashSet<>();
     // Update backtrack set recursively

-    // TODO: The following is the call to the original version of the method
-//    updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
-    // TODO: The following is the call to the version of the method with pushing up happens-before transitions

     updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
   }
 
     updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
   }
 

-//  TODO: This is the original version of the recursive method
-//  private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
-//                                           Execution conflictExecution, int conflictChoice,
-//                                           ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
-//    // Halt when we have found the first read/write conflicts for all memory locations
-//    if (currRWSet.isEmpty()) {
-//      return;
-//    }
-//    TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
-//    // Halt when we have visited this transition (in a cycle)
-//    if (visited.contains(confTrans)) {
-//      return;
-//    }
-//    visited.add(confTrans);
-//    // Explore all predecessors
-//    for (Predecessor predecessor : confTrans.getPredecessors()) {
-//      // Get the predecessor (previous conflict choice)
-//      conflictChoice = predecessor.getChoice();
-//      conflictExecution = predecessor.getExecution();
-//      // Check if a conflict is found
-//      if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) {
-//        createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice);
-//      }
-//      // Continue performing DFS if conflict is not found
-//      updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
-//    }
-//  }
-
-  // TODO: This is the version of the method with pushing up happens-before transitions

   private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
                                            Execution conflictExecution, int conflictChoice,
                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
   private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
                                            Execution conflictExecution, int conflictChoice,
                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {


@@ -1189,9 +1157,6 @@ public class DPORStateReducer extends ListenerAdapter {
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
               currRWSet, visited);
     }
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
               currRWSet, visited);
     }

-    // Remove the transition after being explored
-    // TODO: Seems to cause a lot of loops---commented out for now
-    //visited.remove(confTrans);

   }
 
   // --- Functions related to the reachability analysis when there is a state match
   }
 
   // --- Functions related to the reachability analysis when there is a state match


@@ -1208,13 +1173,13 @@ public class DPORStateReducer extends ListenerAdapter {
         for(TransitionEvent transition : reachableTransitions) {
           transition.recordPredecessor(currentExecution, choiceCounter - 1);
         }
         for(TransitionEvent transition : reachableTransitions) {
           transition.recordPredecessor(currentExecution, choiceCounter - 1);
         }

-        updateBacktrackSetsFromPreviousExecution(stateId);
+        updateBacktrackSetsFromGraph(stateId);

       }
     }
   }
 
   // Update the backtrack sets from previous executions
       }
     }
   }
 
   // Update the backtrack sets from previous executions

-  private void updateBacktrackSetsFromPreviousExecution(int stateId) {
+  private void updateBacktrackSetsFromGraph(int stateId) {

     // Collect all the reachable transitions from R-Graph
     HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitions(stateId);
     for(TransitionEvent transition : reachableTransitions) {
     // Collect all the reachable transitions from R-Graph
     HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitions(stateId);
     for(TransitionEvent transition : reachableTransitions) {