Write UCLID5 code to complete the following task.

> Model a program that has two variables: request of type boolean and status of enumeration type {ready, busy}: 0 denotes 'false' and 1 represents 'true.' The initial and subsequent values of variable request are not determined within this program; this conservatively models that these values are determined by an external environment. This under-specification of request implies that the value of variable status is partially determined: initially, it is ready; and it becomes busy whenever request is true. If request is false, the next value of status is not determined. Write a property that checks that, if request is true, eventually status becomes busy. You can introduce auxiliary variables to do this. Use the variable names request and status.

Reply with your UCLID5 code inside one unique code block.

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