So I came across this issue a colleague of mine was facing when he was using the NAT set in ProB. It's intuitive to assume that NAT is the set of natural numbers in ProB consisting of elements from 0 to infinity but a it revealed otherwise!

Here are my findings if you were to stumble on the same issue...

As per the ProB documentation of the B Machine syntax the NATURAL set of natural numbers, different to the NAT set of numbers (why? take a look below).

While NATURAL represents the set of natural numbers, NAT is set of implementable natural numbers.

Meaning that NAT is a configurable set which is a subset of NATURAL and the min and max numbers can be configured for the B Machine implementation.

The value min of NAT is -1, the max is 3. This is reflected in the State Properties panel of ProB of the uninitialised machine.

You change this default configuration by using:

to change the MAX, and:

to change the min.