No edit summary |
mNo edit summary |
||

(10 intermediate revisions by 3 users not shown) | |||

Line 2: | Line 2: | ||

We assume that you have completed [[Tutorial First Model Checking]]. There we | 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> | ||

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 | 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 | 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]] | ||

== Deferred Sets == | |||

Let us now use the following simple machine: | |||

<Pre> | |||

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

</Pre> | |||

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

[[file:ProBModelCheckNoCounterExampleFound_Unbounded.png|center]] | |||

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

[[file:ProBSimpleCountDefSet_BeforeInit.png|center]] | |||

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

<Pre> | |||

DEFINITIONS scope_ID == 10 | |||

</Pre> | |||

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

[[file:ProBSimpleCountDefSet_InvViol.png|center]] | |||

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

<Pre> | |||

PROPERTIES card(ID) = 5 | |||

</Pre> | |||

ProB will give you the message we have already seen: | |||

[[file:ProBModelCheckNoCounterExampleFound.png|center]] | |||

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

<Pre> | |||

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

</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]] |

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.

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.

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:

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:

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:

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}

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).

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