X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerWithSummary.java;h=6422b7dad5fb464860896adf2f0e65ca2e2289fa;hb=c1a4d7c56d0b0f380240319b056398f74c5ab0d1;hp=bdf17a78848ed8a70dff3bf0a57b92d43e6d653b;hpb=2d80346e5b60963ba456411fde0a288c6bf2e321;p=jpf-core.git

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index bdf17a7..6422b7d 100755
--- 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,17 @@ 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) {