Write UCLID5 code to complete the following task.

> Model a single traffic light as a simple transition system with two states, one state modeling a red light, the other one modeling a green light. Use the variable names red and green.

Reply with your UCLID5 code inside one unique code block.

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