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

Results. Indeed, for finding deadlocks this heuristic obtained the best geometric
mean of 0.5. So, this simple heuristic works surprisingly well. For finding goals,
this heuristic still obtains geometric mean of 0.63, but it is worse than the
random hash function. For finding invariant violations it does not work at all;
its geometric mean is 1.56.
A further refinement of this heuristic is to combine the out degree with the
random hash heuristic, i.e., if two states have the same out degree (which can
happen quite often) we use the hash value as heuristic to avoid a degeneration
into depth-first search. This refinement leads to a further performance improve-
ment for deadlock finding (geometric mean of 0.34 compared to 0.50), and for
goal finding. But it is markedly worse for invariant violation finding.
In conclusion, the out degree heuristic, especially when combined with random
hash, works surprisingly well for its intended purpose of finding deadlocks. In
future work, we plan to further refine this approach, by using a static flow
analysis to guide model checker into deadlocks and/or particular enablings for
events.
Term Size. The idea of this heuristic is to use the term size of the state (i.e.,
the number of constant and function symbols appearing in its representation)
as priority. The motivation for this heuristic is that the larger the state is, the
more complicated it will be to process (for checking invariants and computing
outgoing transitions). Hence, the idea is to process simpler states first, in an
attempt to maximise the number of states processed per time unit.
Results. For finding goals this heuristic has a geometric mean of 0.85, i.e., it is
better than the reference setting of ProB, but worse than random hash. For
deadlock and invariant checking, it also performs worse than random hash. In
summary, this heuristic does not seem worth pursuing further.
Effectiveness of Custom Heuristic Function: In order to experiment eas-
ily with other heuristic functions, we have added the possibility for the user
to define a custom heuristic function for a B model. Basically, this function
can be introduced in the DEFINITIONS part of a B machine by defining
HEURISTIC FUNCTION . ProB now evaluates the expression HEURISTIC FUNCTION
in every state, and uses its value as the priority of the state. Note, the expression
must return an integer value. For the BlocksWorld benchmark, we have written
the following custom heuristic function:
ongoal == {a|->b, b|->c, c|->d, d|->e};
DIFF(A,TARGET) == (card(A-TARGET) - card(TARGET /\ A));
HEURISTIC_FUNCTION == DIFF(on,ongoal);
Note the machine has a variable on is of type Objects +-> Objects and the
GOAL for the model checker is to find a state where on = ongoal is true.
In the benchmarks, we have mainly written heuristic functions which esti-
mate the distance between a target goal state and the current state. In future,