Tutorial Directed Model Checking

We assume that you have completed Tutorial First Model Checking and Complete model checking.

Here we will look a bit closer at the search strategy options of the ProB model checker. You can set the mode using the -mc_mode <M> command-line switch of probcli. In the Tcl/Tk version you can select the strategy in the model checking dialog box (which you obtain via the"Model Check..." command in the "Verify" menu):

The following values are possible:

• Mixed DF/BF (mixed for mc_mode) : mixed depth-first / breadth-first traversal with random choice; currently the default),
• Breadth First (bf for mc_mode): breadth-first traversal,
• Depth First (df) depth-first traversal,
• Heuristic Function / Random (heuristic) : try and use HEURISTIC_FUNCTION provided by user in DEFINITIONS clause. Some explanations can be found in an example about directed model checking.
• Random (random) : choosing next node to process completely at random,
• Hash-Random (hash) :similar to random, but uses the Prolog hash function of a node instead of a random number generator,
• Out-Degree for Deadlock Checking (out_degree_hash): prioritise nodes with fewer outgoing transitions; mainly useful for deadlock checking.