Fixing bug due to refactoring/moving of code in the previous commit to handle apps...

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducerWithSummary.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index bdf17a78848ed8a70dff3bf0a57b92d43e6d653b..2bc18a9f83a5e0210a577be66959cec9bd9294f8 100755 (executable)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -80,6 +80,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   // Boolean states
   private boolean isBooleanCGFlipped;
   private boolean isEndOfExecution;
+  private boolean isNotCheckedForEventsYet;
 
   // Statistics
   private int numOfTransitions;
@@ -100,6 +101,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       }
     }
     isBooleanCGFlipped = false;
+    isNotCheckedForEventsYet = true;
     mainSummary = new MainSummary();
     numOfTransitions = 0;
     nonRelevantClasses = new HashSet<>();
@@ -188,6 +190,18 @@ 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) {
       // Initialize with necessary information from the CG
       if (nextCG instanceof IntChoiceFromSet) {