Mercurial > hg > Members > kono > jpf-core
view src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java @ 0:61d41facf527
initial v8 import (history reset)
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Fri, 23 Jan 2015 10:14:01 -0800 |
parents | |
children | fdc263e5806b |
line wrap: on
line source
/* * 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; } }