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.
