Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
-1:000000000000 0:61d41facf527
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
80 @Override
81 public void reset () {
82 count = -1;
83
84 isDone = false;
85 }
86
87 /**
88 * @see gov.nasa.jpf.vm.IntChoiceGenerator#getNextChoice()
89 **/
90 @Override
91 public T getNextChoice() {
92
93 if ((count >= 0) && (count < values.length)) {
94 return values[count];
95 }
96
97 return getDefaultValue();
98 }
99
100 /**
101 * @see gov.nasa.jpf.vm.ChoiceGenerator#hasMoreChoices()
102 **/
103 @Override
104 public boolean hasMoreChoices() {
105 if (!isDone && (count < values.length-1))
106 return true;
107 else
108 return false;
109 }
110
111 /**
112 * @see gov.nasa.jpf.vm.ChoiceGenerator#advance()
113 **/
114 @Override
115 public void advance() {
116 if (count < values.length-1) count++;
117 }
118
119 /**
120 * get String label of current value, as specified in config file
121 **/
122 public String getValueLabel(){
123 return values[count].toString();
124 }
125
126 @Override
127 public int getTotalNumberOfChoices () {
128 return values.length;
129 }
130
131 @Override
132 public int getProcessedNumberOfChoices () {
133 return count+1;
134 }
135
136 @Override
137 public boolean supportsReordering(){
138 return true;
139 }
140
141
142 protected T parse (String varSpec, StackFrame resolveFrame){
143 int sign = 1;
144
145 char c = varSpec.charAt(0);
146 if (c == '+'){
147 varSpec = varSpec.substring(1);
148 } else if (c == '-'){
149 sign = -1;
150 varSpec = varSpec.substring(1);
151 }
152
153 if (varSpec.isEmpty()){
154 throw new JPFException("illegal value spec for IntChoiceFromList " + id);
155 }
156
157 c = varSpec.charAt(0);
158 if (Character.isDigit(c)){ // its an integer literal
159 return parseLiteral(varSpec, sign);
160
161 } else { // a variable or field name
162 Object o = resolveFrame.getLocalOrFieldValue(varSpec);
163 if (o == null){
164 throw new JPFException("no local or field '" + varSpec + "' value found for NumberChoiceFromList " + id);
165 }
166 if (o instanceof Number){
167 return newValue( (Number)o, sign);
168 } else {
169 throw new JPFException("non-numeric local or field '" + varSpec + "' value for NumberChoiceFromList " + id);
170 }
171 }
172 }
173
174
175 @Override
176 public NumberChoiceFromList<T> reorder (Comparator<T> comparator){
177
178 T[] newValues = values.clone();
179 Arrays.sort( newValues, comparator);
180
181 // we can't instantiate directly
182 try {
183 NumberChoiceFromList<T> clone = (NumberChoiceFromList<T>)clone();
184 clone.values = newValues;
185 clone.count = -1;
186 return clone;
187
188 } catch (CloneNotSupportedException cnsx){
189 // can't happen
190 throw new JPFException("can't clone NumberChoiceFromList " + this);
191 }
192 }
193
194 @Override
195 public String toString() {
196 StringBuilder sb = new StringBuilder(getClass().getName());
197 sb.append("[id=\"");
198 sb.append(id);
199 sb.append('"');
200
201 sb.append(",isCascaded:");
202 sb.append(isCascaded);
203
204 sb.append(",");
205 for (int i=0; i<values.length; i++) {
206 if (i > 0) {
207 sb.append(',');
208 }
209 if (i == count) {
210 sb.append(MARKER);
211 }
212 sb.append(values[i]);
213 }
214 sb.append(']');
215 return sb.toString();
216 }
217
218
219 @Override
220 public NumberChoiceFromList<T> randomize () {
221 for (int i = values.length - 1; i > 0; i--) {
222 int j = random.nextInt(i + 1);
223 T tmp = values[i];
224 values[i] = values[j];
225 values[j] = tmp;
226 }
227 return this;
228 }
229
230 }