X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=12bd44ff802e2547e86e1e22856f32ff6e31c6bf;hp=26dd6bd0b274f2b4fc6e6b963f0176fc224ca545;hb=01797c4785396958affd10f7a2abbc22b9e26da7;hpb=c540b2eddfd5b18a25070d2f85bfe94de3f535c5 diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 26dd6bd..12bd44f 100644 --- 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)