Directed Model Checking for B: An Evaluation and New Techniques - Formal Methods: Foundations and Applications - page 5

Pure Depth-First. In a considerable number of cases pure depth-first is the
fastest method, e.g., for the Peterson err, Abrial Earely3 v5, Alstom axl3, and
BlocksWorld benchmarks.
However, we can see in Table 1 that for some models Depth-First fares very
badly:
- In Alstom ex7 in Table 2, pure depth-first search even fails to find the dead-
lock when given an hour of cputime. This real-life example thus supports
our claim from [17] and subsection 2 that when state space is too large to
examine fully, depth-first will sometimes not find a counter example. This
is actually a quite common case for industrial models: they are typically (at
least before abstraction) too large to handle fully.
- Another similar example is Abrial Press m13 in Table 3, where pure depth-
first is about 900 times slower than ProB in the reference settings.
- Another bad example is Puzzle8, where depth-first is more than 7 times
slower or Simpson4Slot where it is 163 times slower than ProB in the ref-
erence settings. Finally, for the artificially constructed BFTest, depth-first
search fails to find the invariant violation.
For finding goals, the geometric mean of the relative runtimes was 0.92, i.e.,
slightly better than the reference setting. Overall, pure depth-first seemed to
fare best for the deadlocking models with a geometric mean of 0.43. For finding
invariant violations, however, the geometric mean was 1.03, i.e., slightly worse
than the reference setting.
The bad performance in the Huffman benchmark is actually not relevant:
here not all states were evaluated. As such, the time to examine 10,000 states
was measured. The pure-depth first search here encountered more complicated
states, than the other approaches, explaining the additional time required for
model checking.
In conclusion, the performance of pure depth-first alone can vary quite dra-
matically, from very good to very bad. A such, pure depth first search is not a
good choice as a default setting of ProB. Note, however, that we allow the user
to override the default setting and put ProB into pure depth-first mode.
Pure Breadth-First. In most cases pure Breadth-First is worse than the ref-
erence setting; in some cases considerably so. The geometric mean was always
above 1, i.e., worse than the reference setting.
For Alstom ex7 pure breadth-first also fails to find the deadlock.
Peterson err in Table 1 gives a similar picture, Breadth-First being 134 times
slower than DF and 11 times slower than the reference settings of ProB.
Other examples where BF is not so good: Abrial Earley3 v5, DiningPhil, Syste-
mOnChip Router, Wegenetz.
There are some more examples where it performs considerably better than
pure depth-first: Puzzle8, Simpson4Slot, Abrial Press m13 and the “artificial”
benchmarks BFTest and DFTest2.