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

ProBModelCheckNoCounterExampleFound.png

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.