From: rtrimana <rtrimana@uci.edu>
Date: Fri, 19 Jun 2020 16:42:07 +0000 (-0700)
Subject: A few hacks to make the list circular: this lets the CG not signal the JPF that the... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=15a430755720be88420508141246ea4909cb4ade

A few hacks to make the list circular: this lets the CG not signal the JPF that the end of the list is the end of the CG execution.
---

diff --git a/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java b/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java
index 4a7b442..ee3d36e 100644
--- 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++;*/
   }
 
   /**