Tutorial Complete Model Checking: Difference between revisions

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.

Successful Model Checking

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. (In this case there are 4 states and one root node.)

Does this mean that the B machine is guaranteed to be correct? Does this mean that the AtelierB provers will be able to prove the B machine correct? In this case yes, but in general we have to be very careful about interpreting a completed model check. Below we examine several issues that have to be considered.

Computing All Transitions

Let us now adapt the above B machine by changing the DEFINITION of MAX to 6. Now repeat the model checking exercise above. This time ProB will produce the following message:

Again no invariant violations or deadlocks were found, but this time ProB warns us that not all transitions were computed. Indeed, the SET_PREF_MAX_OPERATIONS definition tells ProB to compute at most 5 ways to execute an operation. In this case, there are 6 ways to execute the Reset operation. As such, ProB may have missed certain states and thus may have missed an invariant violation.

Indeed, when you double click on the "INITIALISATION(1)" entry in the "EnabledOperations" pane, you will see the following:

The orange "max" button tells us that not all operations were computed.

In this case, there was no error, but assume we change the definition of the Reset operation to

  Reset = BEGIN count :: 1..MAX+1 END

and repeat the model checking. We will get the exact same result as above, but this time the machine is actually incorrect. The only way to solve ensure that ProB checks the entire state space is to increase the "MAX_OPERATIONS" preference to a suitably large value, e.g., SET_PREF_MAX_OPERATIONS==8 in this case. Now model checking will find a counter example:

Deferred Sets

Let us now use the following simple machine:

MACHINE SimpleCountDefSet
SETS ID
VARIABLES s
INVARIANT s <: ID & card(s)<10
INITIALISATION s := {}
OPERATIONS
  Add(x) = PRE x:ID & x/:s THEN s := s\/{x} END;
  Remove(x) = PRE x:s THEN s:= s - {x} END
END

Here model checking with ProB will give you the following message:

Unfortunately this does not guarantee that your machine is correct. Indeed, ProB has checked your machine only for one specific cardinality of the deferred set ID (probably 2 or 3). Indeed, if you look at the ProB window after loading the above machine you will see:

In the "State Properties" pane you can see that the cardinality of ID was set to 3. There are various ways you can influence the cardinality chosen by ProB; one is by adding a DEFINITION of the form:

DEFINITIONS  scope_ID == 10

If you add this definition, ProB will now find an invariant violation: