Tutorial First Model Checking

We assume that you have loaded the "Lift.mch" B machine from the ProB Examples folder, as outlined in [[Tutorial First Steps]. There we have also seen how to execute operations on a B machine by double clicking on the items in the "Enabled Operations" pane.

The model checker can be used to systematically execute the operations and tries to find an erroneous state (e.g., where the invariant is violated). Select the "Model Check..." command in the "Verify" menu:

This brings up the following dialog box:

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

The lower half of the ProB window should now look as follows: