KickJava   Java API By Example, From Geeks To Geeks.

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


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  * Interface for a Strategy class to encapsulate the state space search algorithm.
23  * This is one of the two major JPF abstractions (the other one being the VM)
24  */
25 public interface Search {
26
27   public static final String JavaDoc DEPTH_CONSTRAINT = "DEPTH";
28   public static final String JavaDoc QUEUE_CONSTRAINT = "QUEUE";
29   public static final String JavaDoc SIZE_CONSTRAINT = "SIZE";
30   
31   /**
32    * add a listener for state changes
33    */
34   void addListener (SearchListener listener);
35
36   void addProperty (Property property);
37   void removeProperty (Property property);
38   
39   /**
40    * return the search results (property violations)
41    */
42   ErrorList getErrors ();
43   
44   /**
45    * do we have a next state (after advancing it)
46    */
47   boolean hasNextState();
48   
49   /**
50    * has this state already been visited (only useful after advancing it)
51    */
52   boolean isNewState ();
53
54   boolean isEndState ();
55     
56   /**
57    * get current search depth
58    */
59   int getSearchDepth();
60
61   /**
62    * get the Transition that brought us into this state
63    */
64   Transition getTransition();
65   
66   /**
67    * get a unique numeric id for this state
68    */
69   int getStateNumber();
70   
71   /**
72    * answer the last hit search constraint code
73    */
74   String JavaDoc getSearchConstraint();
75   
76   /**
77    * request a single backtrack step as the next transition
78    */
79   boolean requestBacktrack ();
80
81   /**
82    * does the search strategy allow listeners to do explicit backtracking
83    */
84   boolean supportsBacktrack ();
85
86   /**
87    * does this search strategy support state restoration
88    */
89   boolean supportsRestoreState ();
90   
91   /**
92    * start the search process - this is the main driver for the VirtualMachine
93    */
94   void search ();
95
96 }
97
Popular Tags