001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.jvm;
020:
021: import gov.nasa.jpf.Config;
022: import gov.nasa.jpf.JPFException;
023:
024: import java.io.BufferedReader;
025: import java.io.IOException;
026: import java.io.InputStreamReader;
027:
028: import java.util.BitSet;
029:
030: /**
031: * a scheduler that exlicitly asks the user for the next thread to pick
032: */
033: public class InteractiveScheduler extends Scheduler {
034: private static BufferedReader br = new BufferedReader(
035: new InputStreamReader(System.in));
036: private static boolean quit = false;
037: private int thread;
038: private int random;
039: private boolean lastRandom;
040:
041: public InteractiveScheduler(Config config) {
042: initialize();
043: }
044:
045: public int getRandom() {
046: return random;
047: }
048:
049: public int getThread() {
050: return thread;
051: }
052:
053: public void initialize() {
054: thread = 0;
055: random = -1;
056: lastRandom = true;
057: }
058:
059: public ThreadInfo locateThread(SystemState ss) {
060: if (quit) {
061: return null;
062: }
063:
064: int nthreads = ss.getThreadCount();
065: int nrunnable = 0;
066: BitSet runnable = new BitSet();
067:
068: for (int i = 0; i < nthreads; i++) {
069: ThreadInfo th = ss.getThreadInfo(i);
070:
071: if (th.isRunnable()) {
072: runnable.set(i);
073: nrunnable++;
074: }
075: }
076:
077: if (nrunnable == 0) {
078: System.out.println("Deadlock: backing up");
079:
080: return null;
081: }
082:
083: System.out.print("Runnable threads [" + nrunnable + "]: ");
084:
085: for (int i = 0; i < nthreads; i++) {
086: if (runnable.get(i)) {
087: if (i == thread) {
088: System.out.print("[" + i + "] ");
089: } else {
090: System.out.print(i + " ");
091: }
092: }
093: }
094:
095: System.out.println();
096:
097: while (true) {
098: try {
099: System.out.print("> ");
100:
101: String s = br.readLine();
102:
103: if (s.equals("quit") || s.equals("q")) {
104: quit = true;
105:
106: return null;
107: } else if (s.equals("backtrack") || s.equals("back")
108: || s.equals("b")) {
109: return null;
110: } else if (s.equals("show") || s.equals("s")) {
111: while (true) {
112: System.out.print("show> ");
113: s = br.readLine();
114:
115: if (s.equals("")) {
116: break;
117: }
118:
119: try {
120: int l = Integer.parseInt(s);
121:
122: if (runnable.get(l)) {
123: ThreadInfo th = (ThreadInfo) ss
124: .getThreadInfo(l);
125: System.out.println(th.getMethod()
126: .getCompleteName()
127: + ":"
128: + th.getPC().getPosition()
129: + " " + th.getPC());
130:
131: break;
132: }
133: } catch (NumberFormatException e) {
134: }
135: }
136: } else if (s.equals("random") || s.equals("r")) {
137: while (true) {
138: System.out.println("Current random: " + random);
139: System.out.print("random> ");
140: s = br.readLine();
141:
142: if (s.equals("")) {
143: break;
144: }
145:
146: try {
147: random = Integer.parseInt(s);
148:
149: break;
150: } catch (NumberFormatException e) {
151: }
152: }
153: } else if (s.equals("help") || s.equals("h")
154: || s.equals("?")) {
155: System.out.println("command:");
156: System.out.println(" quit");
157: System.out.println(" random");
158: System.out.println(" backtrack");
159: System.out.println(" help");
160: } else {
161: if (runnable.get(thread) && s.equals("")) {
162: break;
163: }
164:
165: try {
166: int i = Integer.parseInt(s);
167:
168: if (runnable.get(i)) {
169: thread = i;
170:
171: break;
172: }
173: } catch (NumberFormatException e) {
174: }
175: }
176: } catch (IOException e) {
177: throw new JPFException(e.getMessage());
178: }
179: }
180:
181: System.out.println("Running thread " + thread);
182:
183: return ss.getThreadInfo(thread);
184: }
185:
186: public void next() {
187: if (lastRandom) {
188: random = -1;
189: thread++;
190: } else {
191: random++;
192: }
193: }
194:
195: public int random(int max) {
196: if (random == -1) {
197: random = 0;
198: }
199:
200: lastRandom = (random == max - 1);
201:
202: return random;
203: }
204: }
|