--- /dev/null
+/*
+ * 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 T getChoice (int idx){
+ if (idx >=0 && idx < values.length){
+ return values[idx];
+ } else {
+ throw new IllegalArgumentException("choice index out of range: " + idx);
+ }
+ }
+
+ @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;
+ }
+
+}