Tutorial Model Checking, Proof and CBC: Difference between revisions
No edit summary |
No edit summary |
||
| Line 8: | Line 8: | ||
INVARIANT | INVARIANT | ||
counter:NATURAL & counter<=128 | counter:NATURAL & counter<=128 | ||
INITIALISATION counter:= | INITIALISATION counter:=8 | ||
OPERATIONS | OPERATIONS | ||
Double = PRE counter<100 THEN counter := 2*counter END; | Double = PRE counter<100 THEN counter := 2*counter END; | ||
| Line 17: | Line 17: | ||
Now click the "Model Check" button. After a short while, ProB will give you the following message: | Now click the "Model Check" button. After a short while, ProB will give you the following message: | ||
[[file:ProBModelCheckNoCounterExampleFound.png|center]] | [[file:ProBModelCheckNoCounterExampleFound.png|center]] | ||
Is this model correct? | |||
If you look purely at the state space of the machine (choose the View State Space command in the Animate menu) you get the following picture: | |||
Indeed, all reachable states are correct, in the sense that the invariant counter:NATURAL & counter<=128 holds for all of those states. | |||
Revision as of 12:34, 1 March 2011
We assume that you have completed Tutorial Complete Model Checking.
Let us examine the following B machine:
MACHINE DoubleCounter VARIABLES counter INVARIANT counter:NATURAL & counter<=128 INITIALISATION counter:=8 OPERATIONS Double = PRE counter<100 THEN counter := 2*counter END; Halve = BEGIN counter := counter/2 END END
Now click the "Model Check" button. After a short while, ProB will give you the following message:
Is this model correct?
If you look purely at the state space of the machine (choose the View State Space command in the Animate menu) you get the following picture:
Indeed, all reachable states are correct, in the sense that the invariant counter:NATURAL & counter<=128 holds for all of those states.