2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm.choice;
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;
26 import java.util.Arrays;
27 import java.util.Comparator;
30 * common root for list based number choice generators
32 public abstract class NumberChoiceFromList<T extends Number> extends ChoiceGeneratorBase<T> {
34 // int values to choose from stored as Strings or Integers
36 protected int count = -1;
39 * super constructor for subclasses that want to configure themselves
40 * @param id name used in choice config
42 protected NumberChoiceFromList(String id){
46 protected NumberChoiceFromList (String id, T[] vals){
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);
58 * @param conf JPF configuration object
59 * @param id name used in choice config
61 public NumberChoiceFromList(Config conf, String id) {
64 String[] vals = conf.getCompactStringArray(id + ".values");
65 if (vals == null || vals.length == 0) {
66 throw new JPFException("no value specs for IntChoiceFromList " + id);
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);
80 public T getChoice (int idx){
81 if (idx >=0 && idx < values.length){
84 throw new IllegalArgumentException("choice index out of range: " + idx);
89 public void reset () {
96 * @see gov.nasa.jpf.vm.IntChoiceGenerator#getNextChoice()
99 public T getNextChoice() {
101 if ((count >= 0) && (count < values.length)) {
102 return values[count];
105 return getDefaultValue();
109 * @see gov.nasa.jpf.vm.ChoiceGenerator#hasMoreChoices()
112 public boolean hasMoreChoices() {
113 if (!isDone && (count < values.length-1))
120 * @see gov.nasa.jpf.vm.ChoiceGenerator#advance()
123 public void advance() {
124 if (count < values.length-1) count++;
128 * get String label of current value, as specified in config file
130 public String getValueLabel(){
131 return values[count].toString();
135 public int getTotalNumberOfChoices () {
136 return values.length;
140 public int getProcessedNumberOfChoices () {
145 public boolean supportsReordering(){
150 protected T parse (String varSpec, StackFrame resolveFrame){
153 char c = varSpec.charAt(0);
155 varSpec = varSpec.substring(1);
156 } else if (c == '-'){
158 varSpec = varSpec.substring(1);
161 if (varSpec.isEmpty()){
162 throw new JPFException("illegal value spec for IntChoiceFromList " + id);
165 c = varSpec.charAt(0);
166 if (Character.isDigit(c)){ // its an integer literal
167 return parseLiteral(varSpec, sign);
169 } else { // a variable or field name
170 Object o = resolveFrame.getLocalOrFieldValue(varSpec);
172 throw new JPFException("no local or field '" + varSpec + "' value found for NumberChoiceFromList " + id);
174 if (o instanceof Number){
175 return newValue( (Number)o, sign);
177 throw new JPFException("non-numeric local or field '" + varSpec + "' value for NumberChoiceFromList " + id);
184 public NumberChoiceFromList<T> reorder (Comparator<T> comparator){
186 T[] newValues = values.clone();
187 Arrays.sort( newValues, comparator);
189 // we can't instantiate directly
191 NumberChoiceFromList<T> clone = (NumberChoiceFromList<T>)clone();
192 clone.values = newValues;
196 } catch (CloneNotSupportedException cnsx){
198 throw new JPFException("can't clone NumberChoiceFromList " + this);
203 public String toString() {
204 StringBuilder sb = new StringBuilder(getClass().getName());
209 sb.append(",isCascaded:");
210 sb.append(isCascaded);
213 for (int i=0; i<values.length; i++) {
220 sb.append(values[i]);
223 return sb.toString();
228 public NumberChoiceFromList<T> randomize () {
229 for (int i = values.length - 1; i > 0; i--) {
230 int j = random.nextInt(i + 1);
232 values[i] = values[j];
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) {