Tutorial Complete Model Checking

We assume that you have completed Tutorial First Model Checking. There we have seen how to find invariant violations using the model checker.

In this part we use the following B Machine:

DEFINITIONS
MACHINE SimpleCounterForMC
DEFINITIONS MAX==4; SET_PREF_MAX_OPERATIONS==5
VARIABLES count
INVARIANT
 count: 1..MAX
INITIALISATION count := 1
OPERATIONS
  Increase(y) = PRE y: 1..(MAX-count) THEN
     count := count+y
  END;
  Reset = BEGIN count :: 1..MAX END
END

To load this machine into ProB you can select "New..." from the "File" menu, choose a file name (e.g., "SimpleCounterForMC.mch") and then paste the text above into the ProB source pane and choose "Save and Reopen" from the "File" menu.

Note that the DEFINITION SET_PREF_MAX_OPERATIONS==5 means that ProB will compute at most 5 possible ways to execute any give operation (i.e., Increase and Reset in this case). We return to this issue below.

Now select the "Model Check..." command in the "Verify" menu which brings up the model checking dialog box:

Now click the "Model Check" button. After a short while, ProB will give you the following message:

This message means that ProB has examine all possible states of your B model and has found no invariant violation and no deadlock.