Tutorial First Model Checking: Difference between revisions
(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 …') |
No edit summary |
||
| Line 3: | Line 3: | ||
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. | 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. | ||
== Simple Model Checking == | |||
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). | 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). | ||
| Line 15: | Line 17: | ||
[[file:ProB_LiftAfterModelCheck.png|center||700px]] | [[file:ProB_LiftAfterModelCheck.png|center||700px]] | ||
The red "'''KO'''" button in the "State Properties" pane tells us that the model checker has moved us into a state where the invariant is violated. The "History" pane tells us the sequence of operations that has led to this error. | |||
(Note that this sequence is not necessarily the shortest sequence that leads to an error or to this error. However, by selecting "Breadth First" in the model check dialog above, one can ensure that the shortest paths are found.) | |||
== Coverage Statistics == | |||
We can obtain some statistics about how many states ProB has explored by selecting the "Compute Coverage" command in the "Analyse" menu: | |||
[[file:ProB_LiftAfterModelCheck_Coverage.png|center||700px]] | |||
In the NODES section we can see that ProB has explored a total of 11 nodes (i.e., states of the B machine). | |||
None of these nodes are deadlocked, in the sense that no operations are applicable. | |||
We can also see that for one node the invariant is violated. | |||
Of these 11 nodes, 2 are '''open''', meaning that they have not been explored in the sense that: | |||
* the invariant has not been evaluated | |||
* the enabled operations have not been computed. | |||
As such, an open node may contain an invariant violation and/or could be a deadlocking node. | |||
A live node, is a node which is not deadlocked and not open. | |||
We can also see, that all in all there are 17 transitions among these 11 nodes. A transition is either an operation or an initialisation (there can be one more transition, which we will examine later in the tutorial). | |||
In the COVERED_OPERATIONS section, we can see more details about these transitions: we have one initialisation, 8 <tt>inc</tt> operations and 8 <tt>dec</tt> operations. | |||
Revision as of 14:56, 18 January 2010
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.
Simple Model Checking
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:
The red "KO" button in the "State Properties" pane tells us that the model checker has moved us into a state where the invariant is violated. The "History" pane tells us the sequence of operations that has led to this error. (Note that this sequence is not necessarily the shortest sequence that leads to an error or to this error. However, by selecting "Breadth First" in the model check dialog above, one can ensure that the shortest paths are found.)
Coverage Statistics
We can obtain some statistics about how many states ProB has explored by selecting the "Compute Coverage" command in the "Analyse" menu:
In the NODES section we can see that ProB has explored a total of 11 nodes (i.e., states of the B machine).
None of these nodes are deadlocked, in the sense that no operations are applicable.
We can also see that for one node the invariant is violated.
Of these 11 nodes, 2 are open, meaning that they have not been explored in the sense that:
- the invariant has not been evaluated
- the enabled operations have not been computed.
As such, an open node may contain an invariant violation and/or could be a deadlocking node. A live node, is a node which is not deadlocked and not open.
We can also see, that all in all there are 17 transitions among these 11 nodes. A transition is either an operation or an initialisation (there can be one more transition, which we will examine later in the tutorial).
In the COVERED_OPERATIONS section, we can see more details about these transitions: we have one initialisation, 8 inc operations and 8 dec operations.