| gov.nasa.jpf.jvm.TestJPF gov.nasa.jpf.mc.TestCrossingJPF
TestCrossingJPF | public class TestCrossingJPF extends TestJPF (Code) | | JPF driver for breadth first search test
|
suite | public static TestSuite suite()(Code) | | |
testCrossingBFSHeuristic | public void testCrossingBFSHeuristic()(Code) | | Tests running the Crossing example with BFS heuristic.
|
testCrossingNoHeuristic | public void testCrossingNoHeuristic()(Code) | | Tests running the Crossing example with no heuristics, i.e., with the
default DFS.
|
|
|