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: /**
22: * abstraction for VM state snapshots
23: * <2do> pcm - the API of this interface suffers from the fact that
24: * there are different requirements with varying degrees of history
25: * information, which is very expensive to store. This might change in
26: * the future, by means of a different state representation (linked
27: * states with 'sparse' backtracking points at the nondeterministic
28: * choice states -> POR, Verify)
29: */
30: public interface VMState {
31: Transition getLastTransition();
32:
33: int getThread();
34:
35: /**
36: * make this state fully restorable, i.e. preserve all VM information
37: * about its path plus the backtracking info to roll back above this state
38: */
39: void makeRestorable();
40:
41: /**
42: * did we make this restorable (by means of a 'makeRestorable()'
43: * call) when we obtained the state
44: */
45: boolean isRestorable();
46:
47: /**
48: * a reduced restorability that just saves the path, but does not allow
49: * backtracking above this state
50: */
51: void makeForwardRestorable();
52:
53: /**
54: * did we make this partially restorable (with reduced backtracking) by
55: * means of 'makeForwardRestorable()' when we obtained the state
56: */
57: boolean isForwardRestorable();
58: }
|