Adding a handler in the listener to check if the benchmark has no event (in this...
authorrtrimana <rtrimana@uci.edu>
Tue, 19 Jan 2021 00:09:59 +0000 (16:09 -0800)
committerrtrimana <rtrimana@uci.edu>
Tue, 19 Jan 2021 00:09:59 +0000 (16:09 -0800)
src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java

index bdf17a7..6422b7d 100755 (executable)
@@ -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) {