Removing dead/commented code.

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index 5762ec5ec6628788dd3f03457199a06b9e5fbe51..31b48004ea1f6a77a707f0da02f1b3e5ff07891c 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -392,13 +392,10 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
   private class RGraph {
     private int hiStateId;                                     // Maximum state Id
     private HashMap<Integer, HashSet<TransitionEvent>> graph;  // Reachable transitions from past executions
-    // TODO: THIS IS THE ACCESS SUMMARY
-    //private HashMap<Integer, HashMap<Integer, SummaryNode>> graphSummary;
 
     public RGraph() {
       hiStateId = 0;
       graph = new HashMap<>();
-      //graphSummary = new HashMap<>();
     }
 
     public void addReachableTransition(int stateId, TransitionEvent transition) {
@@ -429,96 +426,6 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       }
       return graph.get(stateId);
     }
-
-//    public HashSet<TransitionEvent> getReachableTransitions(int stateId) {
-//      HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
-//      // All transitions from states higher than the given state ID (until the highest state ID) are reachable
-//      for(int stId = stateId; stId <= hiStateId; stId++) {
-//        // We might encounter state IDs from the first round of Boolean CG
-//        // The second round of Boolean CG should consider these new states
-//        if (graph.containsKey(stId)) {
-//          reachableTransitions.addAll(graph.get(stId));
-//        }
-//      }
-//      return reachableTransitions;
-//    }
-
-//    public HashMap<Integer, SummaryNode> getReachableTransitionSummary(int stateId) {
-//      // Just return an empty map if the state ID is not recorded yet
-//      // This means that there is no reachable transition from this state
-//      if (!graphSummary.containsKey(stateId)) {
-//        return new HashMap<>();
-//      }
-//      return graphSummary.get(stateId);
-//    }
-
-//    private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
-//      // Combine the same write accesses and record in the recordedRWSet
-//      HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
-//      HashMap<String, Integer> writeMap = rwSet.getWriteMap();
-//      for(Map.Entry<String, Integer> entry : recordedWriteMap.entrySet()) {
-//        String writeField = entry.getKey();
-//        // Remove the entry from rwSet if both field and object ID are the same
-//        if (writeMap.containsKey(writeField) &&
-//                (writeMap.get(writeField) == recordedWriteMap.get(writeField))) {
-//          writeMap.remove(writeField);
-//        }
-//      }
-//      // Then add everything into the recorded map because these will be traversed
-//      recordedWriteMap.putAll(writeMap);
-//      // Combine the same read accesses and record in the recordedRWSet
-//      HashMap<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
-//      HashMap<String, Integer> readMap = rwSet.getReadMap();
-//      for(Map.Entry<String, Integer> entry : recordedReadMap.entrySet()) {
-//        String readField = entry.getKey();
-//        // Remove the entry from rwSet if both field and object ID are the same
-//        if (readMap.containsKey(readField) &&
-//                (readMap.get(readField) == recordedReadMap.get(readField))) {
-//          readMap.remove(readField);
-//        }
-//      }
-//      // Then add everything into the recorded map because these will be traversed
-//      recordedReadMap.putAll(readMap);
-//
-//      return rwSet;
-//    }
-
-//    public ReadWriteSet recordTransitionSummary(int stateId, TransitionEvent transition, ReadWriteSet rwSet) {
-//      // Record transition into graphSummary
-//      // TransitionMap maps event (choice) number to a R/W set
-//      HashMap<Integer, SummaryNode> transitionSummary;
-//      if (graphSummary.containsKey(stateId)) {
-//        transitionSummary = graphSummary.get(stateId);
-//      } else {
-//        transitionSummary = new HashMap<>();
-//        graphSummary.put(stateId, transitionSummary);
-//      }
-//      int choice = transition.getChoice();
-//      SummaryNode summaryNode;
-//      // Insert transition into the map if we haven't had this event number recorded
-//      if (!transitionSummary.containsKey(choice)) {
-//        summaryNode = new SummaryNode(transition, rwSet.getCopy());
-//        transitionSummary.put(choice, summaryNode);
-//      } else {
-//        summaryNode = transitionSummary.get(choice);
-//        // Perform union and subtraction between the recorded and the given R/W sets
-//        rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet);
-//      }
-//      return rwSet;
-//    }
-
-//    public void recordTransitionSummaryAtState(int stateId, HashMap<Integer, SummaryNode> transitionSummary) {
-//      // Record transition summary into graphSummary
-//      HashMap<Integer, SummaryNode> transSummary;
-//      if (!graphSummary.containsKey(stateId)) {
-//        transSummary = new HashMap<>(transitionSummary);
-//        graphSummary.put(stateId, transSummary);
-//      } else {
-//        transSummary = graphSummary.get(stateId);
-//        // Merge the two transition summaries
-//        transSummary.putAll(transitionSummary);
-//      }
-//    }
   }
 
   // This class compactly stores Read and Write field sets
@@ -631,7 +538,6 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     private int choiceCounter;                 // Choice counter at this transition
     private Execution execution;               // The execution where this transition belongs
     private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
-    // TODO: THIS IS THE ACCESS SUMMARY
     private HashMap<Integer, SummaryNode> transitionSummary;
                                                // Summary of pushed transitions at the current transition
     private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
@@ -1279,41 +1185,10 @@ public class DPORStateReducerEfficient 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
-    // 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);
   }
 
-//  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
+  // Recursive method to perform backward DFS to traverse the graph
   private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
                                            Execution conflictExecution, int conflictChoice,
                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
@@ -1322,12 +1197,9 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       return;
     }
     visited.add(currTrans);
-    // TODO: THIS IS THE ACCESS SUMMARY
     TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
     // Record this transition into rGraph summary
-//    currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), confTrans, currRWSet);
     currRWSet = currTrans.recordTransitionSummary(confTrans, currRWSet);
-//    rGraph.recordTransitionSummaryAtState(currTrans.getStateId(), currTrans.getTransitionSummary());
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
       return;
@@ -1356,36 +1228,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
   }
 
   // --- Functions related to the reachability analysis when there is a state match
-
-  /*private void analyzeReachabilityAndCreateBacktrackPoints(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)) {
-        // Update reachable transitions in the graph with a predecessor
-        HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
-        for(TransitionEvent transition : reachableTransitions) {
-          transition.recordPredecessor(currentExecution, choiceCounter - 1);
-        }
-        updateBacktrackSetsFromPreviousExecution(stateId);
-      }
-    }
-  }
-
-  // Update the backtrack sets from previous executions
-  private void updateBacktrackSetsFromPreviousExecution(int stateId) {
-    // Collect all the reachable transitions from R-Graph
-    HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitions(stateId);
-    for(TransitionEvent transition : reachableTransitions) {
-      Execution execution = transition.getExecution();
-      int currentChoice = transition.getChoiceCounter();
-      updateBacktrackSet(execution, currentChoice);
-    }
-  }*/
-
-  // TODO: THIS IS THE ACCESS SUMMARY
+  
   private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
     // Perform this analysis only when:
     // 1) this is not during a switch to a new execution,
@@ -1405,7 +1248,6 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
 
   private void updateBacktrackSetsFromPreviousExecution(int stateId) {
     // Collect all the reachable transitions from R-Graph
-    //HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionSummary(stateId);
     HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
     for(TransitionEvent transition : reachableTransitions) {
       // Current transition that stems from this state ID