Fixing a bug: mapping state to event has to be done after the execution termination...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 26dd6bd0b274f2b4fc6e6b963f0176fc224ca545..12bd44ff802e2547e86e1e22856f32ff6e31c6bf 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -228,8 +228,6 @@ public class DPORStateReducer extends ListenerAdapter {
         resetStatesForNewExecution(icsCG, vm);
         // If we don't see a fair scheduling of events/choices then we have to enforce it
         fairSchedulingAndBacktrackPoint(icsCG, vm);
-        // Map state to event
-        mapStateToEvent(icsCG.getNextChoice());
         // Explore the next backtrack point: 
         // 1) if we have seen this state or this state contains cycles that involve all events, and
         // 2) after the current CG is advanced at least once
@@ -238,6 +236,8 @@ public class DPORStateReducer extends ListenerAdapter {
         } else {
           numOfTransitions++;
         }
+        // Map state to event
+        mapStateToEvent(icsCG.getNextChoice());
         justVisitedStates.clear();
         choiceCounter++;
       }
@@ -845,9 +845,6 @@ 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 (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)