KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > search > DFSearch


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.search;
20
21
22 import gov.nasa.jpf.*;
23 import gov.nasa.jpf.util.Debug;
24
25
26 /**
27  * standard depth first model checking (but can be bounded by search depth
28  * and/or explicit Verify.ignoreIf)
29  */
30 public class DFSearch extends AbstractSearch {
31   
32   public DFSearch (Config config, VM vm) {
33     super(config,vm);
34     
35     Debug.println(Debug.MESSAGE, "MC Search");
36   }
37   
38   public boolean requestBacktrack () {
39     doBacktrack = true;
40     
41     return true;
42   }
43   
44   /**
45    * state model of the search
46    * next new -> action
47    * T T forward
48    * T F backtrack, forward
49    * F T backtrack, forward
50    * F F backtrack, forward
51    *
52    * end condition
53    * backtrack failed (no saved states)
54    * | property violation (currently only checked in new states)
55    * | search constraint (depth or memory or time)
56    *
57    * <2do> we could split the properties into forward and backtrack properties,
58    * the latter ones being usable for liveness properties that are basically
59    * condition accumulators for sub-paths of the state space, to be checked when
60    * we backtrack to the state where they were introduced. I think that could be
61    * actually much simpler (to implement) and more powerful than our currently
62    * broken LTL based scheme.
63    * But then again - at some point the properties and the searches will probably
64    * be unified into VM listeners, anyway
65    */
66   
67   public void search () {
68     int maxDepth = getMaxSearchDepth();
69     
70     depth = 0;
71     
72     notifySearchStarted();
73     
74     while (!done) {
75       if ( !isNewState || isEndState) {
76         if (!backtrack()) { // backtrack not possible, done
77 break;
78         }
79         
80         depth--;
81         notifyStateBacktracked();
82       }
83       
84       if (forward()) {
85         notifyStateAdvanced();
86         
87         if (hasPropertyTermination()) {
88           break;
89         }
90         
91         if (isNewState) {
92           depth++;
93                     
94           if (depth >= maxDepth) {
95             isEndState = true;
96             notifySearchConstraintHit(QUEUE_CONSTRAINT);
97           }
98           
99           if (!checkStateSpaceLimit()) {
100             notifySearchConstraintHit(SIZE_CONSTRAINT);
101             // can't go on, we exhausted our memory
102 break;
103           }
104         }
105       } else { // state was processed
106 notifyStateProcessed();
107       }
108     }
109     
110     notifySearchFinished();
111   }
112   
113   
114   public boolean supportsBacktrack () {
115     return true;
116   }
117 }
118
Popular Tags