Write UCLID5 code to complete the following task.

> Model a design of a beverage vending machine. The machine can either deliver beer or soda. It counts the number of soda and beer bottles and returns inserted coins if the vending machine is empty. The vending machine is represented by the two locations start and select, and has variables that store the number of soda bottles (nsoda), and the number of beer bottles (nbeer). The following conditional transitions model the insertion of a coin and refilling the vending machine: start --(true:coin)-> select start --(true:refill)-> start  Labels of conditional transitions are of the form (g : a ) where g is a Boolean condition (called guard), and a is an action that is possible once g holds. As the condition for both conditional transitions above always holds, the action coin is always enabled in the starting location. To keep things simple, we assume that by refill both storages are entirely refilled. The following transitions model that soda (or beer) can be obtained if there is some soda (or beer) left in the vending machine: select --(nsoda > 0:sget)-> start select --(nbeer > 0:bget)-> start Finally, the vending machine automatically switches to the initial start location while returning the inserted coin once there are no bottles left: select --(nsoda=0 & nbeer=0: ret_coin) -> start Let the maximum capacity of both bottle repositories be max. The insertion of a coin (by action coin) leaves the number of bottles unchanged. The same applies when a coin is returned (by action ret coin). The effect of the other actions is as follows: refill : nsoda:=max & nbeer:=max sget: nsoda:=nsoda-1 bget: nbeer:=nbeer-1 You may use boolean variables to indicate when an action is enabled. Use the variable names nsoda, nbeer, sget, bget, refill, coin.

Reply with your UCLID5 code inside one unique code block.

I can definitely do that! Here is the UCLID5 code:
```
