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: * 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 DEPTH_CONSTRAINT = "DEPTH";
28: public static final String QUEUE_CONSTRAINT = "QUEUE";
29: public static final String 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:
38: void removeProperty(Property property);
39:
40: /**
41: * return the search results (property violations)
42: */
43: ErrorList getErrors();
44:
45: /**
46: * do we have a next state (after advancing it)
47: */
48: boolean hasNextState();
49:
50: /**
51: * has this state already been visited (only useful after advancing it)
52: */
53: boolean isNewState();
54:
55: boolean isEndState();
56:
57: /**
58: * get current search depth
59: */
60: int getSearchDepth();
61:
62: /**
63: * get the Transition that brought us into this state
64: */
65: Transition getTransition();
66:
67: /**
68: * get a unique numeric id for this state
69: */
70: int getStateNumber();
71:
72: /**
73: * answer the last hit search constraint code
74: */
75: String getSearchConstraint();
76:
77: /**
78: * request a single backtrack step as the next transition
79: */
80: boolean requestBacktrack();
81:
82: /**
83: * does the search strategy allow listeners to do explicit backtracking
84: */
85: boolean supportsBacktrack();
86:
87: /**
88: * does this search strategy support state restoration
89: */
90: boolean supportsRestoreState();
91:
92: /**
93: * start the search process - this is the main driver for the VirtualMachine
94: */
95: void search();
96:
97: }
|