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 in all versions of ProB:

• 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,

As of version 1.5.1, the following options are also available:

• 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.

To illustrate the effect of the search strategy we use the following simple example:

MACHINE phonebook7
SETS
	Name  ; Code = {c1,c2,c3,c4}
VARIABLES db, active, activec
DEFINITIONS
    scope_Name == 1..4
INVARIANT
		db : Name +-> Code & active:POW(Name) & activec:POW(Code) &
                dom(db) = active & ran(db) = activec
ASSERTIONS
  card(active) >= card(activec)
INITIALISATION  
	db := {} || active := {} || activec := {}
OPERATIONS
dd <-- getdom = dd:= dom(db);
cc <-- lookup(nn) =
	PRE
		nn : Name & nn : active 
	THEN
		cc:=db(nn)
	END;
add(nn,cc) =
	PRE
		nn:Name & cc:Code  & nn /: active 
	THEN
		db := db \/ { nn |-> cc} || active := active \/ {nn} || activec := activec \/ {cc}
	END;
delete(nn,cc) =
        PRE
                nn:Name & cc:Code & nn: active & cc: activec & db(nn) = cc
        THEN
               db := db - { nn |-> cc} || active := active - {nn} || activec := db[(active - {nn})] 
        END	
END

We will illustrate the state space that ProB generates using the various search strategies when limiting the search to 10 nodes. For this we use the command-line version as follows (as there we can provide exactly how many states should be explored):

$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode <MODE>

However, you can also obtain a similar effect with the Tcl/Tk version by starting the model checker and then quickly pressing the Cancel button and then inspecting the state space (Statespace command in the Visualise menu; see Tutorial_First_Model_Checking). Below we show the output of the above command for the various choices of <MODE>.

Breadth-First

$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode bf

Depth-First

$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode df

Mixed DF/BF

$ probcli phonebook7.mch -p MAX_OPERATIONS 200 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode mixed

The result will vary from one run of ProB to another:

It is interesting to compare this result with the random search strategy, which we show next.

Random

$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode random

Here are two sample results:

Compared to the mixed option one can notice that the mixed option has more of a tendency to explore certain branches in depth.

Hash

$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode hash

The difference with the random option is that this will always return the same result, as the hash value of the states do not change from one run of ProB to another.

Out-Degree

$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode dlk

One can notice that ProB here has a tendency to go into depth, as the number of enabled operations decreases: if we add a name to the phonebook, four enabled operations disappear and only two appear (lookup and delete). Note: here it is important to set the MAX_OPERATIONS high enough, otherwise the resulting state space could be different.