Write UCLID5 code to complete the following task.

> Model a beverage vending machine which dispenses drinks on receipt of coins. Add a safety property that checks that the number of inserted coins is always at least the number of dispensed drinks. You may add auxiliary variables. Use the variable names coin and dispensed_drinks.

Reply with your UCLID5 code inside one unique code block.

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