// Initialize with necessary information from the CG
if (nextCG instanceof IntChoiceFromSet) {
IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
+ // Tell JPF that we are performing DPOR
+ icsCG.setDpor();
if (!isEndOfExecution) {
// Check if CG has been initialized, otherwise initialize it
Integer[] cgChoices = icsCG.getAllChoices();
return executionTrace.get(0);
}
+ public TransitionEvent getLastTransition() {
+ return executionTrace.get(executionTrace.size() - 1);
+ }
+
public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
return readWriteFieldsMap;
}
}
public HashSet<TransitionEvent> getReachableTransitionsAtState(int stateId) {
+ if (!graph.containsKey(stateId)) {
+ // This is a loop from a transition to itself, so just return the current transition
+ HashSet<TransitionEvent> transitionSet = new HashSet<>();
+ transitionSet.add(currentExecution.getLastTransition());
+ return transitionSet;
+ }
return graph.get(stateId);
}
pushedExecution, pushedChoice, currRWSet, visited);
}
// Remove the transition after being explored
- visited.remove(confTrans);
+ // TODO: Seems to cause a lot of loops---commented out for now
+ //visited.remove(confTrans);
}
// --- Functions related to the reachability analysis when there is a state match