KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > VMState


1 //
2 // Copyright (C) 2005 United States Government as represented by the
3 // Administrator of the National Aeronautics and Space Administration
4 // (NASA). All Rights Reserved.
5 //
6 // This software is distributed under the NASA Open Source Agreement
7 // (NOSA), version 1.3. The NOSA has been approved by the Open Source
8 // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
9 // 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 /**
23  * abstraction for VM state snapshots
24  * <2do> pcm - the API of this interface suffers from the fact that
25  * there are different requirements with varying degrees of history
26  * information, which is very expensive to store. This might change in
27  * the future, by means of a different state representation (linked
28  * states with 'sparse' backtracking points at the nondeterministic
29  * choice states -> POR, Verify)
30  */
31 public interface VMState {
32   Transition getLastTransition ();
33   
34   int getThread ();
35
36   /**
37    * make this state fully restorable, i.e. preserve all VM information
38    * about its path plus the backtracking info to roll back above this state
39    */
40   void makeRestorable ();
41   
42   /**
43    * did we make this restorable (by means of a 'makeRestorable()'
44    * call) when we obtained the state
45    */
46   boolean isRestorable ();
47   
48   /**
49    * a reduced restorability that just saves the path, but does not allow
50    * backtracking above this state
51    */
52   void makeForwardRestorable ();
53   
54   /**
55    * did we make this partially restorable (with reduced backtracking) by
56    * means of 'makeForwardRestorable()' when we obtained the state
57    */
58   boolean isForwardRestorable ();
59 }
60
Popular Tags