- // Record the events (from choices)
- if (choices == null) {
- choices = cgChoices;
- // Make a copy of choices as reference
- refChoices = copyChoices(choices);
- // Record the max event choice (the last element of the choice array)
- maxEventChoice = choices[choices.length - 1];
+ if (cgChoices.length == 2 && cgChoices[0] == 0 && cgChoices[1] == -1) {
+ // This means the benchmark only has 2 choices, i.e., 0 and -1 which means that it has no events
+ stateReductionMode = false;
+ }
+ isNotCheckedForEventsYet = false;
+ }
+ } else {
+ // 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();
+ // Record the events (from choices)
+ if (choices == null) {
+ choices = cgChoices;
+ // Make a copy of choices as reference
+ refChoices = copyChoices(choices);
+ // Record the max event choice (the last element of the choice array)
+ maxEventChoice = choices[choices.length - 1];
+ }
+ icsCG.setNewValues(choices);
+ icsCG.reset();
+ // Use a modulo since choiceCounter is going to keep increasing
+ int choiceIndex = choiceCounter % choices.length;
+ icsCG.advance(choices[choiceIndex]);
+ } else {
+ // Set done all CGs while transitioning to a new execution
+ icsCG.setDone();