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   // TODO: Fix for Groovy's model-checking
  39   // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
  40   protected boolean isDpor = false;
  41
  42   /**
  43    *  super constructor for subclasses that want to configure themselves
  44    * @param id name used in choice config
  45    */
  46   protected NumberChoiceFromList(String id){
  47     super(id);
  48   }
  49
  50   protected NumberChoiceFromList (String id, T[] vals){
  51     super(id);
  52     values = vals;
  53     count = -1;
  54     isDpor = false;
  55   }
  56
  57   protected abstract T[] createValueArray(int len);
  58   protected abstract T getDefaultValue();
  59   protected abstract T parseLiteral (String literal, int sign);
  60   protected abstract T newValue (Number num, int sign);
  61
  62   /**
  63    * @param conf JPF configuration object
  64    * @param id name used in choice config
  65    */
  66   public NumberChoiceFromList(Config conf, String id) {
  67     super(id);
  68
  69     String[] vals = conf.getCompactStringArray(id + ".values");
  70     if (vals == null || vals.length == 0) {
  71       throw new JPFException("no value specs for IntChoiceFromList " + id);
  72     }
  73
  74     // get the choice values here because otherwise successive getNextChoice()
  75     // calls within the same transition could see different values when looking
  76     // up fields and locals
  77     values = createValueArray(vals.length);
  78     StackFrame resolveFrame = ThreadInfo.getCurrentThread().getLastNonSyntheticStackFrame();
  79     for (int i=0; i<vals.length; i++){
  80       values[i] = parse(vals[i], resolveFrame);
  81     }
  82   }
  83
  84   @Override
  85   public T getChoice (int idx){
  86     if (idx >=0 && idx < values.length){
  87       return values[idx];
  88     } else {
  89       throw new IllegalArgumentException("choice index out of range: " + idx);
  90     }
  91   }
  92
  93   @Override
  94   public void reset () {
  95     count = -1;
  96
  97     isDone = false;
  98   }
  99
 100   /**
 101    * @see gov.nasa.jpf.vm.IntChoiceGenerator#getNextChoice()
 102    **/
 103   @Override
 104   public T getNextChoice() {
 105
 106     if ((count >= 0) && (count < values.length)) {
 107       return values[count];
 108     }
 109
 110     return getDefaultValue();
 111   }
 112
 113   /**
 114    * @see gov.nasa.jpf.vm.ChoiceGenerator#hasMoreChoices()
 115    **/
 116   @Override
 117   public boolean hasMoreChoices() {
 118     // TODO: Fix for Groovy's model-checking
 119     // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
 120     if (isDpor) {
 121       if (!isDone)
 122         return true;
 123       else
 124         return false;
 125     } else {
 126       /* TODO: ORIGINAL CODE*/
 127       if (!isDone && (count < values.length - 1))
 128         return true;
 129       else
 130         return false;
 131     }
 132   }
 133
 134   /**
 135    * @see gov.nasa.jpf.vm.ChoiceGenerator#advance()
 136    **/
 137   @Override
 138   public void advance() {
 139     // TODO: Fix for Groovy's model-checking
 140     // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
 141
 142     // TODO: We make this circular
 143     if (isDpor) {
 144       if (count < values.length - 1) count++;
 145       else count = 0;
 146     } else {
 147       /* TODO: ORIGINAL CODE*/
 148       if (count < values.length - 1) count++;
 149     }
 150   }
 151
 152   /**
 153    * get String label of current value, as specified in config file
 154    **/
 155   public String getValueLabel(){
 156     return values[count].toString();
 157   }
 158
 159   @Override
 160   public int getTotalNumberOfChoices () {
 161     return values.length;
 162   }
 163
 164   @Override
 165   public int getProcessedNumberOfChoices () {
 166     return count+1;
 167   }
 168
 169   @Override
 170   public boolean supportsReordering(){
 171     return true;
 172   }
 173
 174
 175   protected T parse (String varSpec, StackFrame resolveFrame){
 176     int sign = 1;
 177
 178     char c = varSpec.charAt(0);
 179     if (c == '+'){
 180       varSpec = varSpec.substring(1);
 181     } else if (c == '-'){
 182       sign = -1;
 183       varSpec = varSpec.substring(1);
 184     }
 185
 186     if (varSpec.isEmpty()){
 187       throw new JPFException("illegal value spec for IntChoiceFromList " + id);
 188     }
 189
 190     c = varSpec.charAt(0);
 191     if (Character.isDigit(c)){ // its an integer literal
 192       return parseLiteral(varSpec, sign);
 193
 194     } else { // a variable or field name
 195       Object o = resolveFrame.getLocalOrFieldValue(varSpec);
 196       if (o == null){
 197         throw new JPFException("no local or field '" + varSpec + "' value found for NumberChoiceFromList " + id);
 198       }
 199       if (o instanceof Number){
 200         return newValue( (Number)o, sign);
 201       } else {
 202         throw new JPFException("non-numeric local or field '" + varSpec + "' value for NumberChoiceFromList " + id);
 203       }
 204     }
 205   }
 206
 207
 208   @Override
 209   public NumberChoiceFromList<T> reorder (Comparator<T> comparator){
 210
 211     T[] newValues = values.clone();
 212     Arrays.sort( newValues, comparator);
 213
 214     // we can't instantiate directly
 215     try {
 216     NumberChoiceFromList<T> clone = (NumberChoiceFromList<T>)clone();
 217     clone.values = newValues;
 218     clone.count = -1;
 219     return clone;
 220
 221     } catch (CloneNotSupportedException cnsx){
 222       // can't happen
 223       throw new JPFException("can't clone NumberChoiceFromList " + this);
 224     }
 225   }
 226
 227   @Override
 228   public String toString() {
 229     StringBuilder sb = new StringBuilder(getClass().getName());
 230     sb.append("[id=\"");
 231     sb.append(id);
 232     sb.append('"');
 233
 234     sb.append(",isCascaded:");
 235     sb.append(isCascaded);
 236
 237     sb.append(",");
 238     for (int i=0; i<values.length; i++) {
 239       if (i > 0) {
 240         sb.append(',');
 241       }
 242       if (i == count) {
 243         sb.append(MARKER);
 244       }
 245       sb.append(values[i]);
 246     }
 247     sb.append(']');
 248     return sb.toString();
 249   }
 250
 251
 252   @Override
 253   public NumberChoiceFromList<T> randomize () {
 254     for (int i = values.length - 1; i > 0; i--) {
 255       int j = random.nextInt(i + 1);
 256       T tmp = values[i];
 257       values[i] = values[j];
 258       values[j] = tmp;
 259     }
 260     return this;
 261   }
 262
 263   // TODO: Fix for Groovy's model-checking
 264   // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
 265   public void setNewValues(T[] vals) {
 266     values = vals;
 267   }
 268
 269   public int getNextChoiceIndex() {
 270     return count;
 271   }
 272
 273   public void setChoice(int idx, T value) {
 274     if ((idx >= 0) && (idx < values.length)) {
 275       values[idx] = value;
 276     } else {
 277       throw new JPFException("illegal value " + idx + " for array index");
 278     }
 279   }
 280
 281   public void setDpor() {
 282     isDpor = true;
 283   }
 284 }