From e3029fe7a819a13b3753968460facfdeb92eb59b Mon Sep 17 00:00:00 2001
From: rtrimana <rtrimana@uci.edu>
Date: Mon, 22 Jun 2020 16:57:06 -0700
Subject: [PATCH] Adding a way for JPF to be informed that this is DPOR;
 otherwise number the hacked number CGs only work for DPOR and it creates an
 infinite loop for a normal execution without DPOR.

---
 .../nasa/jpf/listener/DPORStateReducer.java   |  2 +
 .../jpf/vm/choice/NumberChoiceFromList.java   | 43 ++++++++++++-------
 2 files changed, 30 insertions(+), 15 deletions(-)

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 13061d8..a8e9367 100644
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -196,6 +196,8 @@ public class DPORStateReducer extends ListenerAdapter {
       // 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();
diff --git a/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java b/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java
index ee3d36e..e9e406a 100644
--- a/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java
+++ b/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java
@@ -34,6 +34,10 @@ public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGener
   // int values to choose from stored as Strings or Integers
   protected T[] values;
   protected int count = -1;
+
+  // TODO: Fix for Groovy's model-checking
+  // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
+  protected boolean isDpor = false;
   
   /**
    *  super constructor for subclasses that want to configure themselves
@@ -47,6 +51,7 @@ public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGener
     super(id);
     values = vals;
     count = -1;
+    isDpor = false;
   }
   
   protected abstract T[] createValueArray(int len);
@@ -112,16 +117,18 @@ public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGener
   public boolean hasMoreChoices() {
     // TODO: Fix for Groovy's model-checking
     // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
-    if (!isDone)
-      return true;
-    else
-      return false;
-
-    /* TODO: ORIGINAL CODE
-    if (!isDone && (count < values.length-1))
-      return true;
-    else
-      return false;*/
+    if (isDpor) {
+      if (!isDone)
+        return true;
+      else
+        return false;
+    } else {
+      /* TODO: ORIGINAL CODE*/
+      if (!isDone && (count < values.length - 1))
+        return true;
+      else
+        return false;
+    }
   }
 
   /**
@@ -133,11 +140,13 @@ public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGener
     // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
 
     // TODO: We make this circular
-    if (count < values.length-1) count++;
-    else count = 0;
-
-    /* TODO: ORIGINAL CODE
-    if (count < values.length-1) count++;*/
+    if (isDpor) {
+      if (count < values.length - 1) count++;
+      else count = 0;
+    } else {
+      /* TODO: ORIGINAL CODE*/
+      if (count < values.length - 1) count++;
+    }
   }
 
   /**
@@ -268,4 +277,8 @@ public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGener
       throw new JPFException("illegal value " + idx + " for array index");
     }
   }
+
+  public void setDpor() {
+    isDpor = true;
+  }
 }
-- 
2.34.1