01: //
02: // Copyright (C) 2005 United States Government as represented by the
03: // Administrator of the National Aeronautics and Space Administration
04: // (NASA). All Rights Reserved.
05: //
06: // This software is distributed under the NASA Open Source Agreement
07: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
08: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
09: // directory tree for the complete NOSA document.
10: //
11: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18: //
19: package gov.nasa.jpf.jvm;
20:
21: import gov.nasa.jpf.JPFException;
22: import gov.nasa.jpf.Path;
23: import gov.nasa.jpf.Transition;
24:
25: /**
26: * this is just a pseudo scheduler that replays a previously saved path
27: * Note that it does not get configured, but automatically created in case
28: * we start JPF with a '*.xml' parameter instead of a main class name, hence
29: * it has a special ctor
30: */
31: public class PathScheduler extends Scheduler {
32: Path path;
33: int pos;
34:
35: PathScheduler(Path execPath) {
36: path = execPath;
37: pos = 0;
38: }
39:
40: public int getRandom() {
41: Transition t = path.get(pos);
42:
43: return t.getRandom();
44: }
45:
46: public int getThread() {
47: Transition t = path.get(pos);
48:
49: return t.getThread();
50: }
51:
52: public void initialize() {
53: }
54:
55: public ThreadInfo locateThread(SystemState ss) {
56: if (pos < path.length()) {
57: Transition t = path.get(pos);
58: int idx = t.getThread();
59:
60: if (idx < ss.getThreadCount()) {
61: ThreadInfo ti = ss.getThreadInfo(idx);
62:
63: if (ti.isRunnable()) {
64: return ti;
65: } else {
66: // error, path has always to be executable right to the end
67: throw new JPFException(
68: "no runnable thread in path transition: "
69: + t);
70: }
71: } else {
72: // error, path out of sync with VM
73: throw new JPFException("invalid thread list index: "
74: + idx);
75: }
76: }
77:
78: // done, no more transitions
79: return null;
80: }
81:
82: public void next() {
83: // move scheduler to next pos
84: pos++;
85: }
86:
87: public int random(int max) {
88: return getRandom();
89: }
90: }
|