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     if (!isDone && (count < values.length-1))
 114       return true;
 115     else
 116       return false;
 117   }
 118
 119   /**
 120    * @see gov.nasa.jpf.vm.ChoiceGenerator#advance()
 121    **/
 122   @Override
 123   public void advance() {
 124     if (count < values.length-1) count++;
 125   }
 126
 127   /**
 128    * get String label of current value, as specified in config file
 129    **/
 130   public String getValueLabel(){
 131     return values[count].toString();
 132   }
 133
 134   @Override
 135   public int getTotalNumberOfChoices () {
 136     return values.length;
 137   }
 138
 139   @Override
 140   public int getProcessedNumberOfChoices () {
 141     return count+1;
 142   }
 143
 144   @Override
 145   public boolean supportsReordering(){
 146     return true;
 147   }
 148
 149
 150   protected T parse (String varSpec, StackFrame resolveFrame){
 151     int sign = 1;
 152
 153     char c = varSpec.charAt(0);
 154     if (c == '+'){
 155       varSpec = varSpec.substring(1);
 156     } else if (c == '-'){
 157       sign = -1;
 158       varSpec = varSpec.substring(1);
 159     }
 160
 161     if (varSpec.isEmpty()){
 162       throw new JPFException("illegal value spec for IntChoiceFromList " + id);
 163     }
 164
 165     c = varSpec.charAt(0);
 166     if (Character.isDigit(c)){ // its an integer literal
 167       return parseLiteral(varSpec, sign);
 168
 169     } else { // a variable or field name
 170       Object o = resolveFrame.getLocalOrFieldValue(varSpec);
 171       if (o == null){
 172         throw new JPFException("no local or field '" + varSpec + "' value found for NumberChoiceFromList " + id);
 173       }
 174       if (o instanceof Number){
 175         return newValue( (Number)o, sign);
 176       } else {
 177         throw new JPFException("non-numeric local or field '" + varSpec + "' value for NumberChoiceFromList " + id);
 178       }
 179     }
 180   }
 181
 182
 183   @Override
 184   public NumberChoiceFromList<T> reorder (Comparator<T> comparator){
 185
 186     T[] newValues = values.clone();
 187     Arrays.sort( newValues, comparator);
 188
 189     // we can't instantiate directly
 190     try {
 191     NumberChoiceFromList<T> clone = (NumberChoiceFromList<T>)clone();
 192     clone.values = newValues;
 193     clone.count = -1;
 194     return clone;
 195
 196     } catch (CloneNotSupportedException cnsx){
 197       // can't happen
 198       throw new JPFException("can't clone NumberChoiceFromList " + this);
 199     }
 200   }
 201
 202   @Override
 203   public String toString() {
 204     StringBuilder sb = new StringBuilder(getClass().getName());
 205     sb.append("[id=\"");
 206     sb.append(id);
 207     sb.append('"');
 208
 209     sb.append(",isCascaded:");
 210     sb.append(isCascaded);
 211
 212     sb.append(",");
 213     for (int i=0; i<values.length; i++) {
 214       if (i > 0) {
 215         sb.append(',');
 216       }
 217       if (i == count) {
 218         sb.append(MARKER);
 219       }
 220       sb.append(values[i]);
 221     }
 222     sb.append(']');
 223     return sb.toString();
 224   }
 225
 226
 227   @Override
 228   public NumberChoiceFromList<T> randomize () {
 229     for (int i = values.length - 1; i > 0; i--) {
 230       int j = random.nextInt(i + 1);
 231       T tmp = values[i];
 232       values[i] = values[j];
 233       values[j] = tmp;
 234     }
 235     return this;
 236   }
 237
 238   // TODO: Fix for Groovy's model-checking
 239   // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
 240   public void setNewValues(T[] vals) {
 241     values = vals;
 242   }
 243 }