Fixing bugs: moving VOD-graph building into the CGAdvanced method to have the most...

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index ec2fe98df4e7a8d043ce554241e283b000fa47f9..532076b91d1418696ca8c31a96558b71a95ca542 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -203,6 +203,7 @@ public class StateReducer extends ListenerAdapter {
             icsCG.advance(choices[choiceIndex]);
             unusedCG.add(icsCG);
           }
+          //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0;
           choiceCounter++;
         } else {
           // Set new CGs to done so that the search algorithm explores the existing CGs
@@ -241,6 +242,7 @@ public class StateReducer extends ListenerAdapter {
       cg.setDone();
     }
     unusedCG.clear();
+    saveVisitedStates();
   }
 
   // Detect cycles in the current execution/trace
@@ -249,12 +251,11 @@ public class StateReducer extends ListenerAdapter {
   // (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);
-    for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
-      dfsFindCycles(edge.getDst(), visitedEvents, new HashSet<>());
-    }
+    dfsFindCycles(currNode, visitingStates, visitedEvents, new HashSet<>());
     if (checkIfAllEventsInvolved(visitedEvents)) {
       containsCyclesWithAllEvts = true;
     }
@@ -262,18 +263,20 @@ public class StateReducer extends ListenerAdapter {
     return containsCyclesWithAllEvts;
   }
 
-  private void dfsFindCycles(ConflictTracker.Node currNode, HashSet<Integer> visitedEvents,
-                             HashSet<Integer> visitingEvents) {
+  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 (visitingEvents.contains(currNode.getId())) {
+    if (visitingStates.contains(currNode)) {
       visitedEvents.addAll(visitingEvents);
     } else {
+      visitingStates.add(currNode);
       for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
         visitingEvents.add(edge.getEventNumber());
-        dfsFindCycles(edge.getDst(), visitedEvents, visitingEvents);
+        dfsFindCycles(edge.getDst(), visitingStates, visitedEvents, visitingEvents);
         visitingEvents.remove(edge.getEventNumber());
       }
+      visitingStates.remove(currNode);
     }
   }
 
@@ -289,6 +292,13 @@ public class StateReducer extends ListenerAdapter {
     return true;
   }
 
+  private void saveVisitedStates() {
+    // CG is being reset
+    // Save all the visited states
+    prevVisitedStates.addAll(currVisitedStates);
+    currVisitedStates.clear();
+  }
+
   @Override
   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
 
@@ -315,7 +325,6 @@ public class StateReducer extends ListenerAdapter {
           choiceCounter = 0;
         }
         // Check if we have seen this state or this state contains cycles that involve all events
-//        if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) {
         if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
           // Traverse the sub-graphs
           if (isResetAfterAnalysis) {
@@ -335,6 +344,7 @@ public class StateReducer extends ListenerAdapter {
                 // Set done if this was the last backtrack list
                 icsCG.setDone();
               }
+              saveVisitedStates();
             }
           } else {
             // Update and reset the CG if needed (do this for the first time after the analysis)
@@ -342,13 +352,19 @@ public class StateReducer extends ListenerAdapter {
             resetAllCGs();
             isResetAfterAnalysis = true;
           }
-          // Save all the visited states
-          prevVisitedStates.addAll(currVisitedStates);
         }
+        // Update the VOD graph always with the latest
+        updateVODGraph(icsCG.getNextChoice());
       }
     }
   }
 
+  private void updateVODGraph(int currChoiceValue) {
+    // Update the graph when we have the current choice value
+    updateVODGraph(prevChoiceValue, currChoiceValue);
+    prevChoiceValue = currChoiceValue;
+  }
+
   private void updateVODGraph(int prevChoice, int currChoice) {
 
     HashSet<Integer> choiceSet;
@@ -383,23 +399,6 @@ public class StateReducer extends ListenerAdapter {
               " which is " + detail + " Transition: " + transition + "\n");
     }
     if (stateReductionMode) {
-      // Update vodGraph
-      int currChoice = choiceCounter - 1;
-      // Adjust currChoice with modulo
-      currChoice = currChoice >= 0 ? currChoice % (choices.length -1) : currChoice;
-      if (currChoice < 0 || choices[currChoice] == -1 ||
-              prevChoiceValue == choices[currChoice]) {
-        // When current choice is 0, previous choice could be -1
-//        updateVODGraph(prevChoiceValue, choices[currChoice]);
-        // Update the state ID variables
-        stateId = search.getStateId();
-        currVisitedStates.add(stateId);
-        return;
-      }
-      // When current choice is 0, previous choice could be -1
-      updateVODGraph(prevChoiceValue, choices[currChoice]);
-      // Current choice becomes previous choice in the next iteration
-      prevChoiceValue = choices[currChoice];
       // Update the state ID variables
       stateId = search.getStateId();
       currVisitedStates.add(stateId);
@@ -417,6 +416,7 @@ public class StateReducer extends ListenerAdapter {
       // Update the state variables
       // Line 19 in the paper page 11 (see the heading note above)
       stateId = search.getStateId();
+      currVisitedStates.add(stateId);
 
       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
               " and depth: " + depth + "\n");
@@ -664,6 +664,10 @@ public class StateReducer extends ListenerAdapter {
         if (currChoiceNextNodes != null) {
           // Add only if there is a mapping for next nodes
           for (Integer nextNode : currChoiceNextNodes) {
+            // Skip cycles
+            if (nextNode == currChoice) {
+              continue;
+            }
             nodesToVisit.addLast(nextNode);
           }
         }