| java.lang.Object
 gov.nasa.jpf.search.AbstractSearch
gov.nasa.jpf.search.DFSearch
| DFSearch | | public class DFSearch extends AbstractSearch (Code) | | standard depth first model checking (but can be bounded by search depth
and/or explicit Verify.ignoreIf)
|
| Method Summary | |
| public boolean | requestBacktrack()
| | public void | search()
state model of the search
next new -> action
T T forward
T F backtrack, forward
F T backtrack, forward
F F backtrack, forward
end condition
backtrack failed (no saved states)
| property violation (currently only checked in new states)
| search constraint (depth or memory or time)
<2do> we could split the properties into forward and backtrack properties,
the latter ones being usable for liveness properties that are basically
condition accumulators for sub-paths of the state space, to be checked when
we backtrack to the state where they were introduced. | | public boolean | supportsBacktrack()
|
| requestBacktrack | | public boolean requestBacktrack()(Code) | | |
| search | | public void search()(Code) | | state model of the search
next new -> action
T T forward
T F backtrack, forward
F T backtrack, forward
F F backtrack, forward
end condition
backtrack failed (no saved states)
| property violation (currently only checked in new states)
| search constraint (depth or memory or time)
<2do> we could split the properties into forward and backtrack properties,
the latter ones being usable for liveness properties that are basically
condition accumulators for sub-paths of the state space, to be checked when
we backtrack to the state where they were introduced. I think that could be
actually much simpler (to implement) and more powerful than our currently
broken LTL based scheme.
But then again - at some point the properties and the searches will probably
be unified into VM listeners, anyway
|
| supportsBacktrack | | public boolean supportsBacktrack()(Code) | | |
|
|