Tutorial First Model Checking

Revision as of 14:37, 18 January 2010 by Michael Leuschel (talk | contribs) (Created page with 'Category:User Manual 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 …')
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)


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:

ProBWinModelCheckCommand.png

This brings up the following dialog box:

ProBWinModelCheckDialog.png

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

ProBWinModelCheckCounterExampleFound.png

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

ProB LiftAfterModelCheck.png