Tutorial Complete Model Checking: Difference between revisions

No edit summary
mNo edit summary
 
(5 intermediate revisions by 3 users not shown)
Line 2: Line 2:




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


In this part we use the following B Machine:
In this part we use the following B Machine:
<pre>
<pre>
DEFINITIONS
MACHINE SimpleCounterForMC
MACHINE SimpleCounterForMC
DEFINITIONS MAX==4; SET_PREF_MAX_OPERATIONS==5
DEFINITIONS MAX==4; SET_PREF_MAX_OPERATIONS==5
Line 23: Line 22:
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.
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.
Note that the <tt>DEFINITION SET_PREF_MAX_OPERATIONS==5</tt> means that ProB will compute at most 5 possible ways to execute any given operation (i.e., Increase and Reset in this case). We return to this issue below.


== Successful Model Checking ==
== Successful Model Checking ==
Line 35: Line 34:


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?
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.
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.
Below we examine several issues that have to be considered.


Line 44: Line 43:
[[file:ProBModelCheckNoCounterExampleFoundTrans.png|center]]
[[file:ProBModelCheckNoCounterExampleFoundTrans.png|center]]


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.
Again no invariant violations or deadlocks were found, but this time ProB warns us that not all transitions were computed. Indeed, the <tt>SET_PREF_MAX_OPERATIONS</tt> 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:
Indeed, when you double click on the "INITIALISATION(1)" entry in the "EnabledOperations" pane, you will see the following:
Line 56: Line 55:
</Pre>
</Pre>
and repeat the model checking. We will get the exact same result as above, but this time the machine is actually incorrect.
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.
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., <tt>SET_PREF_MAX_OPERATIONS==8</tt> in this case.
Now model checking will find a counter example:
Now model checking will find a counter example:
[[file:ProBSimpleCounterForMC_InvViol.png|center]]
[[file:ProBSimpleCounterForMC_InvViol.png|center]]
Line 82: Line 81:
[[file:ProBSimpleCountDefSet_BeforeInit.png|center]]
[[file:ProBSimpleCountDefSet_BeforeInit.png|center]]
In the "State Properties" pane you can see that the cardinality of ID was set to 3.
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:
There are various ways you can influence the cardinality chosen by ProB. One is by adding a DEFINITION of the form:
<Pre>
<Pre>
DEFINITIONS  scope_ID == 10
DEFINITIONS  scope_ID == 10
Line 99: Line 98:
SETS ID={id1,id2,id3,id4,id5}
SETS ID={id1,id2,id3,id4,id5}
</Pre>
</Pre>
== Infinite Types ==
It could be that your B machine makes use of the mathematical integers (<tt>INTEGER</tt>) or infinite subsets thereof (<tt>NATURAL</tt>, <tt>NATURAL1</tt>). Note that some derived types (such as seq(.)) are defined in terms of INTEGER.
In this case there could be no way to explore all states of your system.
For example, the following operation
<Pre>
Choose = BEGIN x :: NATURAL END
</Pre>
can be executed in infinitely many ways. ProB will in this case only find values between 0 and <tt>MAXINT</tt> for x. As such, a complete model checking does not indicate that your machine's state space has been fully explored.
Note: ProB prints a warning on the console when an infinite type (like <tt>NATURAL</tt>) was "expanded" into a finite subset of it. This information is not yet fed back to the graphical user interface (but we are working on it).
== Model Checking and Proof ==
Finally, even if ProB was able to successfully check the entire state space of your model, this does not imply that you can prove your machine correct with AtelierB (or Rodin).
We dedicate another tutorial page to this: [[Tutorial Model Checking, Proof and CBC|Model Checking, Proof and CBC]]

Latest revision as of 08:47, 17 June 2022


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

In this part we use the following B Machine:

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 given 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:

ProBWinModelCheckDialog.png

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

ProBModelCheckNoCounterExampleFound.png

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:

ProBModelCheckNoCounterExampleFoundTrans.png

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:

ProBSimpleCounterForMC Max.png

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:

ProBSimpleCounterForMC InvViol.png

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:

ProBModelCheckNoCounterExampleFound Unbounded.png

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:

ProBSimpleCountDefSet BeforeInit.png

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:

ProBSimpleCountDefSet InvViol.png

However, if you remove the above DEFINITION and add the following instead:

PROPERTIES card(ID) = 5

ProB will give you the message we have already seen:

ProBModelCheckNoCounterExampleFound.png

Indeed, you have now explicitly declare ID to be of size 5, and ProB has checked all states for that instantiation of ID. Another solution is to replace the deferred set ID by an enumerated set (this will, however, reduce the potential for symmetry reduction):

SETS ID={id1,id2,id3,id4,id5}

Infinite Types

It could be that your B machine makes use of the mathematical integers (INTEGER) or infinite subsets thereof (NATURAL, NATURAL1). Note that some derived types (such as seq(.)) are defined in terms of INTEGER. In this case there could be no way to explore all states of your system. For example, the following operation

 Choose = BEGIN x :: NATURAL END

can be executed in infinitely many ways. ProB will in this case only find values between 0 and MAXINT for x. As such, a complete model checking does not indicate that your machine's state space has been fully explored. Note: ProB prints a warning on the console when an infinite type (like NATURAL) was "expanded" into a finite subset of it. This information is not yet fed back to the graphical user interface (but we are working on it).

Model Checking and Proof

Finally, even if ProB was able to successfully check the entire state space of your model, this does not imply that you can prove your machine correct with AtelierB (or Rodin). We dedicate another tutorial page to this: Model Checking, Proof and CBC