Cleaning up: Removing the full-blown graph traversal.

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 791a7dad4b2d67eb3e629a74f8bfb8d5b1158384..b426d26f49d85044ddefebae2311263eb21cc361 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -38,10 +38,9 @@ import java.util.*;
  **/
 
 public class ConflictTracker extends ListenerAdapter {
  **/
 
 public class ConflictTracker extends ListenerAdapter {

-  // Public graph: to allow the StateReducer class to access it
-  public static final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
-  // Private
+

   private final PrintWriter out;
   private final PrintWriter out;

+  private final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph

   private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
   private final HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions
   private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
   private final HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 96d49a3d3ccfe5d930369f14485812ab0b7d343f..0a27b5ce2f8f30f70d970576746d900d1dfeb7fd 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -89,8 +89,6 @@ public class StateReducer extends ListenerAdapter {
   // HashSet that stores references to unused CGs
   private HashSet<IntChoiceFromSet> unusedCG;
 
   // HashSet that stores references to unused CGs
   private HashSet<IntChoiceFromSet> unusedCG;
 

-  // Reference to the state graph in the ConflictTracker class
-  // TODO: The following is a full-blown graph traversal that we can do if we need to in the future

   //private HashMap<Integer, ConflictTracker.Node> stateGraph;
   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
   // Map state to event
   //private HashMap<Integer, ConflictTracker.Node> stateGraph;
   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
   // Map state to event


@@ -120,8 +118,6 @@ public class StateReducer extends ListenerAdapter {
     backtrackSet = new HashSet<>();
     conflictPairMap = new HashMap<>();
     unusedCG = new HashSet<>();
     backtrackSet = new HashSet<>();
     conflictPairMap = new HashMap<>();
     unusedCG = new HashSet<>();

-    // TODO: The following is a full-blown graph traversal that we can do if we need to in the future
-    //stateGraph = ConflictTracker.nodes;

     stateToEventMap = new HashMap<>();
     prevVisitedStates = new HashSet<>();
     currVisitedStates = new HashSet<>();
     stateToEventMap = new HashMap<>();
     prevVisitedStates = new HashSet<>();
     currVisitedStates = new HashSet<>();


@@ -278,42 +274,6 @@ public class StateReducer extends ListenerAdapter {
     return containsCyclesWithAllEvts;
   }
 
     return containsCyclesWithAllEvts;
   }
 

-  // TODO: The following is a full-blown graph traversal that we can do if we need to in the future
-  // Detect cycles in the current execution/trace
-  // We terminate the execution iff:
-  // (1) the state has been visited in the current execution
-  // (2) the state has one or more cycles that involve all the events
-//  private boolean containsCyclesWithAllEvents(int stId) {
-//
-//    HashSet<ConflictTracker.Node> visitingStates = new HashSet<>();
-//    HashSet<Integer> visitedEvents = new HashSet<>();
-//    boolean containsCyclesWithAllEvts = false;
-//    ConflictTracker.Node currNode = stateGraph.get(stId);
-//    dfsFindCycles(currNode, visitingStates, visitedEvents, new HashSet<>());
-//    if (checkIfAllEventsInvolved(visitedEvents)) {
-//      containsCyclesWithAllEvts = true;
-//    }
-//
-//    return containsCyclesWithAllEvts;
-//  }
-//
-//  private void dfsFindCycles(ConflictTracker.Node currNode, HashSet<ConflictTracker.Node> visitingStates,
-//                             HashSet<Integer> visitedEvents, HashSet<Integer> visitingEvents) {
-//
-//    // Stop when there is a cycle and record all the events
-//    if (visitingStates.contains(currNode)) {
-//      visitedEvents.addAll(visitingEvents);
-//    } else {
-//      visitingStates.add(currNode);
-//      for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
-//        visitingEvents.add(edge.getEventNumber());
-//        dfsFindCycles(edge.getDst(), visitingStates, visitedEvents, visitingEvents);
-//        visitingEvents.remove(edge.getEventNumber());
-//      }
-//      visitingStates.remove(currNode);
-//    }
-//  }
-

   private boolean checkIfAllEventsInvolved(HashSet<Integer> visitedEvents) {
 
     // Check if this set contains all the event choices
   private boolean checkIfAllEventsInvolved(HashSet<Integer> visitedEvents) {
 
     // Check if this set contains all the event choices