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.vm.ChoiceGeneratorBase;
21 import gov.nasa.jpf.vm.ThreadChoiceGenerator;
22 import gov.nasa.jpf.vm.ThreadInfo;
24 import java.io.PrintWriter;
25 import java.util.Arrays;
26 import java.util.Comparator;
28 public class ThreadChoiceFromSet extends ChoiceGeneratorBase<ThreadInfo> implements ThreadChoiceGenerator {
30 protected boolean isSchedulingPoint;
31 protected ThreadInfo[] values;
34 protected ThreadChoiceFromSet (String id){
37 // all other fields have to be computed by subclass ctor
41 public ThreadChoiceFromSet (String id, ThreadInfo[] set, boolean isSchedulingPoint) {
47 this.isSchedulingPoint = isSchedulingPoint;
50 if (isSchedulingPoint){
51 // do a sanity check to see if the candidates are acutally runnable
52 for (int i = 0; i < set.length; i++) {
53 if (!set[i].isTimeoutRunnable()) {
54 throw new JPFException("trying to schedule non-runnable: " + set[i]);
62 public ThreadInfo getChoice (int idx){
63 if (idx >= 0 && idx < values.length){
66 throw new IllegalArgumentException("choice index out of range: " + idx);
72 public void reset () {
79 public ThreadInfo getNextChoice () {
80 if ((count >= 0) && (count < values.length)) {
83 // we don't raise an exception here because this might be (mis)used
84 // from a listener, which shouldn't produce JPFExceptions
90 public boolean hasMoreChoices () {
91 return (!isDone && (count < values.length-1));
96 * this has to handle timeouts, which we do with temporary thread status
97 * changes (i.e. the TIMEOUT_WAITING threads are in our list of choices, but
98 * only change their status to TIMEDOUT when they are picked as the next choice)
100 * <2do> this should be in SystemState.nextSuccessor - there might be
101 * other ThreadChoiceGenerators, and we should handle this consistently
104 public void advance () {
105 if (count < values.length-1) { // at least one choice left
111 public int getTotalNumberOfChoices () {
112 return values.length;
116 public int getProcessedNumberOfChoices () {
120 public Object getNextChoiceObject () {
121 return getNextChoice();
124 public ThreadInfo[] getChoices(){
129 public boolean supportsReordering(){
134 public ThreadChoiceGenerator reorder (Comparator<ThreadInfo> comparator){
135 ThreadInfo[] newValues = values.clone();
136 Arrays.sort(newValues, comparator);
138 return new ThreadChoiceFromSet( id, newValues, isSchedulingPoint);
142 public void printOn (PrintWriter pw) {
143 pw.print(getClass().getName());
148 pw.append(",isCascaded:");
149 pw.append(Boolean.toString(isCascaded));
152 for (int i=0; i<values.length; i++) {
153 if (i > 0) pw.print(',');
157 pw.print(values[i].getName());
163 public ThreadChoiceFromSet randomize () {
164 for (int i = values.length - 1; i > 0; i--) {
165 int j = random.nextInt(i + 1);
166 ThreadInfo tmp = values[i];
167 values[i] = values[j];
173 public ThreadInfo[] getAllThreadChoices() {
178 public boolean contains (ThreadInfo ti){
179 for (int i=0; i<values.length; i++){
180 if (values[i] == ti){
188 public Class<ThreadInfo> getChoiceType() {
189 return ThreadInfo.class;
193 public boolean isSchedulingPoint() {
194 return isSchedulingPoint;