How to generate random numbers from 1 to 6 using the B language

Question

I'm working on a project using B language. I want to get a random number from a dice. Dice consist of 6 faces. How to generate random numbers from 1 to 6 using the B language?

I found this random number generation from the Specification in B: an introduction using the B toolkit by Haughton, Howard, pg 64-65.

MACHINE RandomNat
VARIABLES
rand 
INVARIANT
rand € N 
INITIALISATION
rand :€ N 
OPERATIONS
new_rand = 
BEGIN 
rand :€ N 
END;
nn <— choose =
nn := rand 
END

We claim that this machine is refined by:

REFINEMENT RandRef 
REFINES RandomNat
VARIABLES 
randl 
INVARIANT 
randl € N ^
rand = randl 
INITIALISATION 
randl :£ N 
OPERATIONS 
new_rand = 
ANY nn 
WHERE nn € N ^ 
nn > randl 
THEN 
randl := nn
END; 
nn <— choose = 
nn := randl 
END

Does anyone have an idea?

Thank you community!

Answer 1

A simple specification that meets your need would be

MACHINE dice
OPERATIONS
  face <-- roll = 
    BEGIN
       face :: 1..6
    END
END

However it does not take into account any randomness requirement...