Write UCLID5 code to complete the following task.

> Model a traffic light with the usual three phases "red", "green", and "yellow". Add assertions to check the safety property that every red phase is immediately preceded by a yellow phase. You may add auxiliary variables. Use the variable names red, green, yellow.

Reply with your UCLID5 code inside one unique code block.

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