import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.jvm.bytecode.*;
import gov.nasa.jpf.vm.*;
-import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
import gov.nasa.jpf.vm.bytecode.ReadInstruction;
-import gov.nasa.jpf.vm.bytecode.StoreInstruction;
import gov.nasa.jpf.vm.bytecode.WriteInstruction;
import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
-import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
-import java.awt.*;
import java.io.PrintWriter;
import java.util.*;
-import java.util.List;
// TODO: Fix for Groovy's model-checking
// TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
// State reduction fields
private Integer[] choices;
+ private IntChoiceFromSet currCG;
private int choiceCounter;
private Integer choiceUpperBound;
private boolean isInitialized;
private void initializeStateReduction() {
if (stateReductionMode) {
choices = null;
+ currCG = null;
choiceCounter = 0;
choiceUpperBound = 0;
isInitialized = false;
Integer[] cgChoices = icsCG.getAllChoices();
if (!isInitialized) {
// Get the upper bound from the last element of the choices
- choiceUpperBound = (Integer) cgChoices[cgChoices.length - 1];
+ choiceUpperBound = cgChoices[cgChoices.length - 1];
isInitialized = true;
}
// Record the subsequent Integer CGs only until we hit the upper bound
// Update the current pointer to the current set of choices
if (choices == null || choices != icsCG.getAllChoices()) {
choiceListStartIndexMap.remove(choices);
+ currCG = icsCG;
choices = icsCG.getAllChoices();
// Reset a few things for the sub-graph
conflictPairMap = new HashMap<>();
private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) {
LinkedList<Integer[]> backtrackChoiceLists;
- // Check if we have a list for this choice number
- // If not we create a new one for it
- if (!backtrackMap.containsKey(conflictEventNumber)) {
- backtrackChoiceLists = new LinkedList<>();
- backtrackMap.put(conflictEventNumber, backtrackChoiceLists);
- } else {
- backtrackChoiceLists = backtrackMap.get(conflictEventNumber);
- }
// Create a new list of choices for backtrack based on the current choice and conflicting event number
// If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack
// The backtrack point is the CG for event number 1 and the list length is one less than the original list
// (originally of length 6) since we don't start from event number 0
if (!isResetAfterAnalysis) {
+ // Check if we have a list for this choice number
+ // If not we create a new one for it
+ if (!backtrackMap.containsKey(conflictEventNumber)) {
+ backtrackChoiceLists = new LinkedList<>();
+ backtrackMap.put(conflictEventNumber, backtrackChoiceLists);
+ } else {
+ backtrackChoiceLists = backtrackMap.get(conflictEventNumber);
+ }
int maxListLength = choiceUpperBound + 1;
int listLength = maxListLength - conflictEventNumber;
Integer[] newChoiceList = new Integer[listLength + 1];
// The start index for the recursion is always 1 (from the main branch)
choiceListStartIndexMap.put(newChoiceList, 1);
} else { // This is a sub-graph
+ int backtrackListIndex = cgMap.get(currCG);
+ backtrackChoiceLists = backtrackMap.get(backtrackListIndex);
int listLength = choices.length;
Integer[] newChoiceList = new Integer[listLength];
// Copy everything before the conflict number