From 65940568a7cd0c600af6e481d12b97afb3c55b19 Mon Sep 17 00:00:00 2001
From: rtrimana <rtrimana@uci.edu>
Date: Tue, 19 Jan 2021 10:22:39 -0800
Subject: [PATCH] Fixing bug due to refactoring/moving of code in the previous
 commit to handle apps with no events.

---
 .../listener/DPORStateReducerWithSummary.java | 69 +++++++++----------
 1 file changed, 34 insertions(+), 35 deletions(-)

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index cfc7067..2bc18a9 100755
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -190,44 +190,43 @@ 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) {
+          // This means the benchmark only has 2 choices, i.e., 0 and -1 which means that it has no events
+          stateReductionMode = false;
+        }
+        isNotCheckedForEventsYet = false;
+      }
+    }
     if (stateReductionMode) {
-      if (isNotCheckedForEventsYet) {
-        // Check if this benchmark has no events
-        if (nextCG instanceof IntChoiceFromSet) {
-          IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
+      // 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();
-          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();
+          // 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();
         }
       }
     }
-- 
2.34.1