A few hacks to make the list circular: this lets the CG not signal the JPF that the...

[jpf-core.git] / src / main / gov / nasa / jpf / vm / choice / NumberChoiceFromList.java

diff --git a/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java b/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java
index ceb53a52ab0539a4d32be176fbc6e7570c617058..ee3d36e00aca05fcac5ce2e9716f575d104e5f70 100644 (file)
--- a/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java
+++ b/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java
@@ -110,10 +110,18 @@ public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGener
    **/
   @Override
   public boolean hasMoreChoices() {
-    if (!isDone && (count < values.length-1))  
+    // 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;*/
   }
 
   /**
@@ -121,7 +129,15 @@ public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGener
    **/
   @Override
   public void advance() {
+    // TODO: Fix for Groovy's model-checking
+    // 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++;*/
   }
 
   /**
@@ -235,4 +251,21 @@ public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGener
     return this;
   }
 
+  // TODO: Fix for Groovy's model-checking
+  // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
+  public void setNewValues(T[] vals) {
+    values = vals;
+  }
+
+  public int getNextChoiceIndex() {
+    return count;
+  }
+
+  public void setChoice(int idx, T value) {
+    if ((idx >= 0) && (idx < values.length)) {
+      values[idx] = value;
+    } else {
+      throw new JPFException("illegal value " + idx + " for array index");
+    }
+  }
 }