Adding a way for JPF to be informed that this is DPOR; otherwise number the hacked...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 13061d8aa03d5559ba740e64bd8fb5079c561d21..a8e93675828204be6e36918143903b0240568173 100644 (file)
--- 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 ee3d36e00aca05fcac5ce2e9716f575d104e5f70..e9e406ab70d0b952c334af1a3c750416e2fda335 100644 (file)
--- 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;
+  }
 }