From: rtrimana <rtrimana@uci.edu>
Date: Tue, 19 Jan 2021 00:09:59 +0000 (-0800)
Subject: Adding a handler in the listener to check if the benchmark has no event (in this... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=c1a4d7c56d0b0f380240319b056398f74c5ab0d1

Adding a handler in the listener to check if the benchmark has no event (in this case we don't do DPOR).
---

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) {