--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java	Fri Jan 23 10:14:01 2015 -0800
@@ -0,0 +1,230 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.vm.choice;
+
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.JPFException;
+import gov.nasa.jpf.vm.ChoiceGeneratorBase;
+import gov.nasa.jpf.vm.StackFrame;
+import gov.nasa.jpf.vm.ThreadInfo;
+
+import java.util.Arrays;
+import java.util.Comparator;
+
+/** 
+ * common root for list based number choice generators
+ */
+public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGeneratorBase<T> {
+
+  // int values to choose from stored as Strings or Integers
+  protected T[] values;
+  protected int count = -1;
+  
+  /**
+   *  super constructor for subclasses that want to configure themselves
+   * @param id name used in choice config
+   */
+  protected NumberChoiceFromList(String id){
+    super(id);
+  }
+
+  protected NumberChoiceFromList (String id, T[] vals){
+    super(id);
+    values = vals;
+    count = -1;
+  }
+  
+  protected abstract T[] createValueArray(int len);
+  protected abstract T getDefaultValue();
+  protected abstract T parseLiteral (String literal, int sign);
+  protected abstract T newValue (Number num, int sign);
+  
+  /**
+   * @param conf JPF configuration object
+   * @param id name used in choice config
+   */
+  public NumberChoiceFromList(Config conf, String id) {
+    super(id);
+
+    String[] vals = conf.getCompactStringArray(id + ".values");
+    if (vals == null || vals.length == 0) {
+      throw new JPFException("no value specs for IntChoiceFromList " + id);
+    }
+
+    // get the choice values here because otherwise successive getNextChoice()
+    // calls within the same transition could see different values when looking
+    // up fields and locals
+    values = createValueArray(vals.length);
+    StackFrame resolveFrame = ThreadInfo.getCurrentThread().getLastNonSyntheticStackFrame();
+    for (int i=0; i<vals.length; i++){
+      values[i] = parse(vals[i], resolveFrame);
+    }
+  }
+  
+
+  @Override
+  public void reset () {
+    count = -1;
+
+    isDone = false;
+  }
+      
+  /** 
+   * @see gov.nasa.jpf.vm.IntChoiceGenerator#getNextChoice()
+   **/
+  @Override
+  public T getNextChoice() {
+
+    if ((count >= 0) && (count < values.length)) {
+      return values[count];
+    }
+
+    return getDefaultValue();
+  }
+
+  /**
+   * @see gov.nasa.jpf.vm.ChoiceGenerator#hasMoreChoices()
+   **/
+  @Override
+  public boolean hasMoreChoices() {
+    if (!isDone && (count < values.length-1))  
+      return true;
+    else
+      return false;
+  }
+
+  /**
+   * @see gov.nasa.jpf.vm.ChoiceGenerator#advance()
+   **/
+  @Override
+  public void advance() {
+    if (count < values.length-1) count++;
+  }
+
+  /**
+   * get String label of current value, as specified in config file
+   **/
+  public String getValueLabel(){
+    return values[count].toString();
+  }
+
+  @Override
+  public int getTotalNumberOfChoices () {
+    return values.length;
+  }
+
+  @Override
+  public int getProcessedNumberOfChoices () {
+    return count+1;
+  }
+  
+  @Override
+  public boolean supportsReordering(){
+    return true;
+  }
+  
+  
+  protected T parse (String varSpec, StackFrame resolveFrame){
+    int sign = 1;
+
+    char c = varSpec.charAt(0);
+    if (c == '+'){
+      varSpec = varSpec.substring(1);
+    } else if (c == '-'){
+      sign = -1;
+      varSpec = varSpec.substring(1);
+    }
+
+    if (varSpec.isEmpty()){
+      throw new JPFException("illegal value spec for IntChoiceFromList " + id);
+    }
+
+    c = varSpec.charAt(0);
+    if (Character.isDigit(c)){ // its an integer literal
+      return parseLiteral(varSpec, sign);
+
+    } else { // a variable or field name
+      Object o = resolveFrame.getLocalOrFieldValue(varSpec);
+      if (o == null){
+        throw new JPFException("no local or field '" + varSpec + "' value found for NumberChoiceFromList " + id);
+      }
+      if (o instanceof Number){
+        return newValue( (Number)o, sign);
+      } else {
+        throw new JPFException("non-numeric local or field '" + varSpec + "' value for NumberChoiceFromList " + id);
+      }
+    }
+  }
+
+  
+  @Override
+  public NumberChoiceFromList<T> reorder (Comparator<T> comparator){
+    
+    T[] newValues = values.clone();
+    Arrays.sort( newValues, comparator);
+    
+    // we can't instantiate directly
+    try {
+    NumberChoiceFromList<T> clone = (NumberChoiceFromList<T>)clone();
+    clone.values = newValues;
+    clone.count = -1;
+    return clone;
+    
+    } catch (CloneNotSupportedException cnsx){
+      // can't happen
+      throw new JPFException("can't clone NumberChoiceFromList " + this);
+    }
+  }
+  
+  @Override
+  public String toString() {
+    StringBuilder sb = new StringBuilder(getClass().getName());
+    sb.append("[id=\"");
+    sb.append(id);
+    sb.append('"');
+
+    sb.append(",isCascaded:");
+    sb.append(isCascaded);
+
+    sb.append(",");
+    for (int i=0; i<values.length; i++) {
+      if (i > 0) {
+        sb.append(',');
+      }
+      if (i == count) {
+        sb.append(MARKER);
+      }
+      sb.append(values[i]);
+    }
+    sb.append(']');
+    return sb.toString();
+  }
+  
+  
+  @Override
+  public NumberChoiceFromList<T> randomize () {
+    for (int i = values.length - 1; i > 0; i--) {
+      int j = random.nextInt(i + 1);
+      T tmp = values[i];
+      values[i] = values[j];
+      values[j] = tmp;
+    }
+    return this;
+  }
+
+}