Refactoring/moving handler in the listener to check if the benchmark has no event...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index 6422b7dad5fb464860896adf2f0e65ca2e2289fa..cfc70678086df38f980d793e691aeb9b06831926 100755 (executable)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -190,42 +190,44 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
 
   @Override
   public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
-    if (isNotCheckedForEventsYet) {
-      // Check if this benchmark has no events
-      if (nextCG instanceof IntChoiceFromSet) {
-        IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
-        Integer[] cgChoices = icsCG.getAllChoices();
-        if (cgChoices.length == 2 && cgChoices[0] == 0 && cgChoices[1] == -1) {
-          stateReductionMode = false;
-        }
-        isNotCheckedForEventsYet = false;
-      }
-    }
     if (stateReductionMode) {
-      // 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
+      if (isNotCheckedForEventsYet) {
+        // Check if this benchmark has no events
+        if (nextCG instanceof IntChoiceFromSet) {
+          IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
           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];
+          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();
           }
-          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();
         }
       }
     }