private HashSet<String> backtrackSet;
private HashMap<Integer, HashSet<Integer>> conflictPairMap;
// Map choicelist with start index
-// private HashMap<Integer[],Integer> choiceListStartIndexMap;
+ // private HashMap<Integer[],Integer> choiceListStartIndexMap;
// Map that represents graph G
// (i.e., visible operation dependency graph (VOD Graph)
private HashSet<Integer> visitedStateSet;
// Current state
private int stateId;
+ // Previous choice number
+ private int prevChoiceValue;
public StateReducer(Config config, JPF jpf) {
debugMode = config.getBoolean("debug_state_transition", false);
vodGraphMap = new HashMap<>();
visitedStateSet = new HashSet<>();
stateId = -1;
+ prevChoiceValue = -1;
initializeStateReduction();
}
// Advance choice counter for sub-graphs
choiceCounter++;
// Do this for every CG after finishing each backtrack list
- if (icsCG.getNextChoice() == -1) {
+ if (icsCG.getNextChoice() == -1 || visitedStateSet.contains(stateId)) {
int event = cgMap.get(icsCG);
LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
if (choiceLists != null && choiceLists.peekFirst() != null) {
" which is " + detail + " Transition: " + transition + "\n");
}
if (stateReductionMode) {
- // Line 19 in the paper page 11 (see the heading note above)
- stateId = search.getStateId();
- if (visitedStateSet.contains(stateId)) {
- // VOD graph is not updated if the "new" state has been seen earlier
- return;
- }
- // Add state ID into the visited state set
- visitedStateSet.add(stateId);
// Update vodGraph
int currChoice = choiceCounter - 1;
- int prevChoice = currChoice - 1;
- if (currChoice < 0) {
- // Current choice has to be at least 0 (initial case can be -1)
+ if (currChoice < 0 || currChoice > choices.length - 1 || choices[currChoice] == -1 || prevChoiceValue == choices[currChoice]) {
+ // Handle all corner cases (e.g., out of bound values)
return;
}
- // Current choice and previous choice values could be -1 (since we use -1 as the end-of-array condition)
- int currChoiceValue = (choices[currChoice] == -1) ? 0 : choices[currChoice];
// When current choice is 0, previous choice could be -1
- int prevChoiceValue = (prevChoice == -1) ? -1 : choices[prevChoice];
- updateVODGraph(prevChoiceValue, currChoiceValue);
+ updateVODGraph(prevChoiceValue, choices[currChoice]);
+ // Current choice becomes previous choice in the next iteration
+ prevChoiceValue = choices[currChoice];
+ // Line 19 in the paper page 11 (see the heading note above)
+ stateId = search.getStateId();
+ // Add state ID into the visited state set
+ visitedStateSet.add(stateId);
}
}