Бросок кубиков для b-метода в Ателье B

Question

Домашнее задание требует, чтобы я разработал спецификацию B настольной игры Snakes & Ladders с помощью Atelier B.

Цель игры - бросить один кубик и продвинуться вверх по доске. Цель состоит в том, чтобы завершить игру, приземлившись на последнюю клетку, то есть 100.

Таким образом, у меня должен быть кубик, который выпадает случайным образом от 1 до 6. Тем не менее, я не уверен, как сгенерировать число или выпадать кубик случайным образом от 1 до 6… На данный момент он просто выпадает только до 2.

Может, кто-нибудь поможет мне, так как я новичок в B-программировании и B-инструментах в целом.

      Machine 
     new 

     VARIABLES
         dice 

     INVARIANT
         dice : NAT1 

     INITIALISATION
         dice := 0 

     OPERATIONS 
         //rolling the dice 
         rollDice <-- throwDice =
         BEGIN 
             dice := 2 ||
             rollDice := Rolled
         END;
END