src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.vm.choice;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPFException;
  22 import gov.nasa.jpf.vm.ChoiceGeneratorBase;
  23 import gov.nasa.jpf.vm.StackFrame;
  24 import gov.nasa.jpf.vm.ThreadInfo;
  25
  26 import java.util.Arrays;
  27 import java.util.Comparator;
  28
  29 /**
  30  * common root for list based number choice generators
  31  */
  32 public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGeneratorBase<T> {
  33
  34   // int values to choose from stored as Strings or Integers
  35   protected T[] values;
  36   protected int count = -1;
  37
  38   /**
  39    *  super constructor for subclasses that want to configure themselves
  40    * @param id name used in choice config
  41    */
  42   protected NumberChoiceFromList(String id){
  43     super(id);
  44   }
  45
  46   protected NumberChoiceFromList (String id, T[] vals){
  47     super(id);
  48     values = vals;
  49     count = -1;
  50   }
  51
  52   protected abstract T[] createValueArray(int len);
  53   protected abstract T getDefaultValue();
  54   protected abstract T parseLiteral (String literal, int sign);
  55   protected abstract T newValue (Number num, int sign);
  56
  57   /**
  58    * @param conf JPF configuration object
  59    * @param id name used in choice config
  60    */
  61   public NumberChoiceFromList(Config conf, String id) {
  62     super(id);
  63
  64     String[] vals = conf.getCompactStringArray(id + ".values");
  65     if (vals == null || vals.length == 0) {
  66       throw new JPFException("no value specs for IntChoiceFromList " + id);
  67     }
  68
  69     // get the choice values here because otherwise successive getNextChoice()
  70     // calls within the same transition could see different values when looking
  71     // up fields and locals
  72     values = createValueArray(vals.length);
  73     StackFrame resolveFrame = ThreadInfo.getCurrentThread().getLastNonSyntheticStackFrame();
  74     for (int i=0; i<vals.length; i++){
  75       values[i] = parse(vals[i], resolveFrame);
  76     }
  77   }
  78
  79   @Override
  80   public T getChoice (int idx){
  81     if (idx >=0 && idx < values.length){
  82       return values[idx];
  83     } else {
  84       throw new IllegalArgumentException("choice index out of range: " + idx);
  85     }
  86   }
  87
  88   @Override
  89   public void reset () {
  90     count = -1;
  91
  92     isDone = false;
  93   }
  94
  95   /**
  96    * @see gov.nasa.jpf.vm.IntChoiceGenerator#getNextChoice()
  97    **/
  98   @Override
  99   public T getNextChoice() {
 100
 101     if ((count >= 0) && (count < values.length)) {
 102       return values[count];
 103     }
 104
 105     return getDefaultValue();
 106   }
 107
 108   /**
 109    * @see gov.nasa.jpf.vm.ChoiceGenerator#hasMoreChoices()
 110    **/
 111   @Override
 112   public boolean hasMoreChoices() {
 113     // TODO: Fix for Groovy's model-checking
 114     // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
 115     if (!isDone)
 116       return true;
 117     else
 118       return false;
 119
 120     /* TODO: ORIGINAL CODE
 121     if (!isDone && (count < values.length-1))
 122       return true;
 123     else
 124       return false;*/
 125   }
 126
 127   /**
 128    * @see gov.nasa.jpf.vm.ChoiceGenerator#advance()
 129    **/
 130   @Override
 131   public void advance() {
 132     // TODO: Fix for Groovy's model-checking
 133     // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
 134
 135     // TODO: We make this circular
 136     if (count < values.length-1) count++;
 137     else count = 0;
 138
 139     /* TODO: ORIGINAL CODE
 140     if (count < values.length-1) count++;*/
 141   }
 142
 143   /**
 144    * get String label of current value, as specified in config file
 145    **/
 146   public String getValueLabel(){
 147     return values[count].toString();
 148   }
 149
 150   @Override
 151   public int getTotalNumberOfChoices () {
 152     return values.length;
 153   }
 154
 155   @Override
 156   public int getProcessedNumberOfChoices () {
 157     return count+1;
 158   }
 159
 160   @Override
 161   public boolean supportsReordering(){
 162     return true;
 163   }
 164
 165
 166   protected T parse (String varSpec, StackFrame resolveFrame){
 167     int sign = 1;
 168
 169     char c = varSpec.charAt(0);
 170     if (c == '+'){
 171       varSpec = varSpec.substring(1);
 172     } else if (c == '-'){
 173       sign = -1;
 174       varSpec = varSpec.substring(1);
 175     }
 176
 177     if (varSpec.isEmpty()){
 178       throw new JPFException("illegal value spec for IntChoiceFromList " + id);
 179     }
 180
 181     c = varSpec.charAt(0);
 182     if (Character.isDigit(c)){ // its an integer literal
 183       return parseLiteral(varSpec, sign);
 184
 185     } else { // a variable or field name
 186       Object o = resolveFrame.getLocalOrFieldValue(varSpec);
 187       if (o == null){
 188         throw new JPFException("no local or field '" + varSpec + "' value found for NumberChoiceFromList " + id);
 189       }
 190       if (o instanceof Number){
 191         return newValue( (Number)o, sign);
 192       } else {
 193         throw new JPFException("non-numeric local or field '" + varSpec + "' value for NumberChoiceFromList " + id);
 194       }
 195     }
 196   }
 197
 198
 199   @Override
 200   public NumberChoiceFromList<T> reorder (Comparator<T> comparator){
 201
 202     T[] newValues = values.clone();
 203     Arrays.sort( newValues, comparator);
 204
 205     // we can't instantiate directly
 206     try {
 207     NumberChoiceFromList<T> clone = (NumberChoiceFromList<T>)clone();
 208     clone.values = newValues;
 209     clone.count = -1;
 210     return clone;
 211
 212     } catch (CloneNotSupportedException cnsx){
 213       // can't happen
 214       throw new JPFException("can't clone NumberChoiceFromList " + this);
 215     }
 216   }
 217
 218   @Override
 219   public String toString() {
 220     StringBuilder sb = new StringBuilder(getClass().getName());
 221     sb.append("[id=\"");
 222     sb.append(id);
 223     sb.append('"');
 224
 225     sb.append(",isCascaded:");
 226     sb.append(isCascaded);
 227
 228     sb.append(",");
 229     for (int i=0; i<values.length; i++) {
 230       if (i > 0) {
 231         sb.append(',');
 232       }
 233       if (i == count) {
 234         sb.append(MARKER);
 235       }
 236       sb.append(values[i]);
 237     }
 238     sb.append(']');
 239     return sb.toString();
 240   }
 241
 242
 243   @Override
 244   public NumberChoiceFromList<T> randomize () {
 245     for (int i = values.length - 1; i > 0; i--) {
 246       int j = random.nextInt(i + 1);
 247       T tmp = values[i];
 248       values[i] = values[j];
 249       values[j] = tmp;
 250     }
 251     return this;
 252   }
 253
 254   // TODO: Fix for Groovy's model-checking
 255   // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
 256   public void setNewValues(T[] vals) {
 257     values = vals;
 258   }
 259
 260   public int getNextChoiceIndex() {
 261     return count;
 262   }
 263
 264   public void setChoice(int idx, T value) {
 265     if ((idx >= 0) && (idx < values.length)) {
 266       values[idx] = value;
 267     } else {
 268       throw new JPFException("illegal value " + idx + " for array index");
 269     }
 270   }
 271 }