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;
20:
21: import gov.nasa.jpf.Path;
22: import java.io.Writer;
23:
24: import java.io.PrintWriter;
25:
26: /**
27: * abstraction for state producers (VMs).
28: * <2do> - seems to be superfluous now that we target only JVMs, and there is a suitable
29: * base
30: */
31: public interface VM {
32: // pcm - my favourite canidate to get scrubbed
33: int getAbstractionNonDeterministicThreadCount();
34:
35: int getAliveThreadCount();
36:
37: boolean isBoringState();
38:
39: boolean isDeadlocked();
40:
41: Exception getException();
42:
43: // these are used for heuristic searches, should be either a generalized
44: // attribution, or scrubbed
45: boolean isInterestingState();
46:
47: Transition getLastTransition();
48:
49: Path getPath();
50:
51: int getPathLength();
52:
53: int getRunnableThreadCount();
54:
55: /**
56: * return a object describing the current execution state of the VM. Note
57: * that history information for this state has to be explicitly requested
58: * by means of 'makeRestorable()' and 'makeForwardRestorable()' calls, because
59: * of the involved costs
60: */
61: VMState getState();
62:
63: String getThreadName();
64:
65: boolean initialize();
66:
67: boolean backtrack();
68:
69: boolean forward();
70:
71: boolean isNewState();
72:
73: boolean isEndState();
74:
75: int getStateId();
76:
77: void printStatus();
78:
79: void restoreState(VMState state);
80:
81: void rewind(); // <?> pcm either reset or rewind, but not both
82:
83: void savePath(Path path, Writer w);
84:
85: void addListener(VMListener listener);
86:
87: void printResults(PrintWriter pw);
88: }
|