projects
/
jpf-core.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
c540b2e
)
Fixing a bug: mapping state to event has to be done after the execution termination...
author
rtrimana
<rtrimana@uci.edu>
Thu, 16 Apr 2020 21:44:45 +0000
(14:44 -0700)
committer
rtrimana
<rtrimana@uci.edu>
Thu, 16 Apr 2020 21:44:45 +0000
(14:44 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
patch
|
blob
|
history
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);
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
// 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++;
}
} else {
numOfTransitions++;
}
+ // Map state to event
+ mapStateToEvent(icsCG.getNextChoice());
justVisitedStates.clear();
choiceCounter++;
}
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 (!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)