random - 如何使用B语言生成1到6的随机数

Question

我正在做一个使用 B 语言的项目。我想从骰子中得到一个随机数。骰子由 6 个面组成。如何使用B语言生成1到6的随机数？

我从 B 中的规范中找到了这个随机数生成：使用 B 工具包的介绍，霍顿，霍华德，第 64-65 页。

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

我们声称这台机器是通过以下方式改进的：

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

有人有想法吗？

谢谢社区！