Fixing more bugs with the reachability analysis.

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

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 104af2bd9993dd0cabb776e3e793e1a2060ba2fa..26dd6bd0b274f2b4fc6e6b963f0176fc224ca545 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -404,10 +404,6 @@ public class DPORStateReducer extends ListenerAdapter {
     // Store restorable state object for this state (always store the latest)
     RestorableVMState restorableState = vm.getRestorableState();
     restorableStateMap.put(stateId, restorableState);
     // Store restorable state object for this state (always store the latest)
     RestorableVMState restorableState = vm.getRestorableState();
     restorableStateMap.put(stateId, restorableState);

-    // Map multiple state IDs to a choice counter
-    for (Integer stId : justVisitedStates) {
-      stateToChoiceCounterMap.put(stId, choiceCounter);
-    }

   }
 
   private Integer[] copyChoices(Integer[] choicesToCopy) {
   }
 
   private Integer[] copyChoices(Integer[] choicesToCopy) {


@@ -495,6 +491,7 @@ public class DPORStateReducer extends ListenerAdapter {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }

+    stateToChoiceCounterMap.put(stateId, choiceCounter);

     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
     justVisitedStates.add(stateId);
     currVisitedStates.add(stateId);
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
     justVisitedStates.add(stateId);
     currVisitedStates.add(stateId);


@@ -588,6 +585,10 @@ public class DPORStateReducer extends ListenerAdapter {
     if (currentCG instanceof IntIntervalGenerator) {
       // This is the interval CG used in device handlers
       ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
     if (currentCG instanceof IntIntervalGenerator) {
       // This is the interval CG used in device handlers
       ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();

+      // Iterate until we find the IntChoiceFromSet CG
+      while (!(parentCG instanceof IntChoiceFromSet)) {
+        parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator();
+      }

       int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice();
       // Find the index of the event/choice in refChoices
       for (int i = 0; i<refChoices.length; i++) {
       int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice();
       // Find the index of the event/choice in refChoices
       for (int i = 0; i<refChoices.length; i++) {


@@ -844,6 +845,9 @@ public class DPORStateReducer extends ListenerAdapter {
     if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 &&
             currVisitedStates.contains(stateId) && (stateId > 0)) {
       // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
     if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 &&
             currVisitedStates.contains(stateId) && (stateId > 0)) {
       // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts

+      if (stateToChoiceCounterMap.get(stateId) == null) {
+        System.out.println();
+      }

       int conflictChoice = stateToChoiceCounterMap.get(stateId);
       int currentChoice = choiceCounter - 1;
       // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
       int conflictChoice = stateToChoiceCounterMap.get(stateId);
       int currentChoice = choiceCounter - 1;
       // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)