Code refactoring for sleep set and persistent set analyses.

[jpf-core.git] / src / main / gov / nasa / jpf / listener / EfficientStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/EfficientStateReducer.java b/src/main/gov/nasa/jpf/listener/EfficientStateReducer.java
index 03efc87b594f06860b2f59e09eee692f2f35c824..f0d25d730d9056f0d9149c21b6620f8eada38c89 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/EfficientStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/EfficientStateReducer.java
@@ -413,6 +413,32 @@ public class EfficientStateReducer extends ListenerAdapter {
     return integerArray;
   }
 
+  private void completeBacktrackChoiceList(List<Integer> newChoiceList, int currentChoice, int conflictEventNumber,
+                                         LinkedList<Integer[]> backtrackChoiceLists) {
+    // Put the conflicting event numbers first and reverse the order
+    newChoiceList.add(choices[currentChoice]);
+    newChoiceList.add(choices[conflictEventNumber]);
+    // Put the rest of the event numbers into the array starting from the minimum to the upper bound
+    for (int i = conflictEventNumber + 1; i < choices.length - 1; i++) {
+      // Check the sleep sets for excepted events that do not conflict with the current one
+      int prevChoiceNum = newChoiceList.get(newChoiceList.size()-1);
+      HashSet<Integer> sleepSet = sleepSetMap.get(prevChoiceNum);
+      if (choices[i] != choices[currentChoice] && !sleepSet.contains(choices[i])) {
+        newChoiceList.add(choices[i]);
+      }
+    }
+    // Set the last element to '-1' as the end of the sequence
+    newChoiceList.add(-1);
+    Integer[] newChoiceArray = copyIntegerListToArray(newChoiceList);
+    backtrackChoiceLists.addLast(newChoiceArray);
+    if (!isResetAfterAnalysis) {
+      // The start index for the recursion is always 1 (from the main branch)
+      choiceListStartIndexMap.put(newChoiceArray, 1);
+    } else {
+      choiceListStartIndexMap.put(newChoiceArray, conflictEventNumber + 1);
+    }
+  }
+
   private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) {
 
     LinkedList<Integer[]> backtrackChoiceLists;
@@ -430,52 +456,20 @@ public class EfficientStateReducer extends ListenerAdapter {
         backtrackChoiceLists = backtrackMap.get(conflictEventNumber);
       }
       List<Integer> newChoiceList = new ArrayList<>();
-      // Put the conflicting event numbers first and reverse the order
-      newChoiceList.add(choices[currentChoice]);
-      newChoiceList.add(choices[conflictEventNumber]);
-      // Put the rest of the event numbers into the array starting from the minimum to the upper bound
-      for (int i = conflictEventNumber + 1; i < choices.length - 1; i++) {
-        // Check the sleep sets for excepted events that do not conflict with the current one
-        int prevSleepSet = newChoiceList.get(newChoiceList.size()-1);
-        HashSet<Integer> sleepSet = sleepSetMap.get(prevSleepSet);
-        if (choices[i] != choices[currentChoice] && !sleepSet.contains(choices[i])) {
-          newChoiceList.add(choices[i]);
-        }
-      }
-      // Set the last element to '-1' as the end of the sequence
-      newChoiceList.add(-1);
-      Integer[] newChoiceArray = copyIntegerListToArray(newChoiceList);
-      backtrackChoiceLists.addLast(newChoiceArray);
-      // The start index for the recursion is always 1 (from the main branch)
-      choiceListStartIndexMap.put(newChoiceArray, 1);
+      completeBacktrackChoiceList(newChoiceList, currentChoice, conflictEventNumber, backtrackChoiceLists);
     } else { // This is a sub-graph
       int backtrackListIndex = cgMap.get(currCG);
       backtrackChoiceLists = backtrackMap.get(backtrackListIndex);
       List<Integer> newChoiceList = new ArrayList<>();
       // Copy everything before the conflict number
-      int conflictEventCurrentIndex = getChoiceIndex(conflictEventNumber);
-      for(int i = 0; i < conflictEventCurrentIndex; i++) {
+      int conflictEventCurrentNumber = getChoiceIndex(conflictEventNumber);
+      for(int i = 0; i < conflictEventCurrentNumber; i++) {
         newChoiceList.add(choices[i]);
       }
       // Put the conflicting events
-      int currentChoiceCurrentIndex = getChoiceIndex(currentChoice);
-      newChoiceList.add(choices[currentChoiceCurrentIndex]);
-      newChoiceList.add(choices[conflictEventCurrentIndex]);
-      // Copy the rest
-      for(int i = conflictEventCurrentIndex + 1; i < choices.length - 1; i++) {
-        // Check the sleep sets for excepted events that do not conflict with the current one
-        int prevSleepSet = newChoiceList.get(newChoiceList.size()-1);
-        HashSet<Integer> sleepSet = sleepSetMap.get(prevSleepSet);
-        if (choices[i] != choices[currentChoiceCurrentIndex] && !sleepSet.contains(choices[i])) {
-          newChoiceList.add(choices[i]);
-        }
-      }
-      // Set the last element to '-1' as the end of the sequence
-      newChoiceList.add(-1);
-      Integer[] newChoiceArray = copyIntegerListToArray(newChoiceList);
-      backtrackChoiceLists.addLast(newChoiceArray);
-      // For the sub-graph the start index depends on the conflicting event number
-      choiceListStartIndexMap.put(newChoiceArray, conflictEventCurrentIndex + 1);
+      int currentChoiceCurrentNumber = getChoiceIndex(currentChoice);
+      completeBacktrackChoiceList(newChoiceList, currentChoiceCurrentNumber, conflictEventCurrentNumber,
+              backtrackChoiceLists);
     }
   }