Tutorial Model Checking, Proof and CBC

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