Information Technology Reference
In-Depth Information
the other predicate yields the oldest open state (for breadth-first traversal). This
approach allowed us to implement a mixed depth-first / breadth-first approach
by randomly selecting either an element from the front or the end of the pending
list of open states.
We have implemented a priority queue in C++ using the STL (Standard
Template Library) multimap data structure. One can thus e ciently add new
open states with a particular weight, and then either chose the state with the
lowest or highest weight.
We now describe the various heuristic functions we have investigated, as well
as the result of the empirical investigation. In this paper we evaluate some strate-
gies to assign weights to newly encountered states. In particular we describe a
random search, a search based on the number of successor states, a search based
on the (term) size of the state as well as some custom heuristic functions written
by the modeler for a particular model. The latter approach is used for models
where a specific goal was known, e.g., puzzles.
Random Hash. The idea is simply to use the hash value of a state as the weight
for the priority queue. The hope is that the hash value distributes uniformly,
i.e., that this would provide a good way to randomize the treatment of pending
states. The hash value is computed anyway for every state, using SICStus Prolog
term hash predicate.
The purpose was to use this heuristic as a base-line: a heuristic that is worse
or not markedly better than this one is not worth the effort. We also want to
compare this heuristic with the mixed depth-first/breadth-first approach from
Section 3 and see whether there any notable differences. Indeed, the mixed depth-
first/breadth-first search does not randomize the order of the states in the list,
and this could have an influence on the model checking performance.
Results. For finding deadlocks (Table 5) and goals (Table 6) the random hash
heuristic is markedly better than the reference settings of ProB (except for the
Bosch cruise control model; but runtimes there are very low anyway). For finding
invariant violations, however, (Table 4) it is worse (its geometric mean is greater
than 1 (1.07) and in two examples it is markedly worse).
Overall, it seems to perform slightly better than our mixed DF/BF search.
We have also experimented with truly random approach, where we use a
random number generator rather than the hash value for the priority. The results
are rather similar, except for Alstom ex7 where it systematically outperforms
Random Hash.
Out Degree. The idea is to use the out degree of a state as priority, i.e., the
number of outgoing transitions. The motivation is that if we have found a state
with an out degree of 0, i.e., the highest priority, we have found a deadlock.
Intuitively, the less transitions are enabled for a state, the closer we may be to
a deadlock. In the implementation we actually do not know the out degree of
a state until it has been processed. Hence, we use the out degree of the (first)
predecessor state for the priority.
 
Search WWH ::




Custom Search