Write UCLID5 code to complete the following task.

> Consider a street junction with 4 incoming roads. Each of the 4 roads has a traffic light, which are L1, L2, L3, L4. The traffic light has 4 states: green, yellow, red, and amber which happen in that order. Write a model of this junction with 4 traffic lights, showing a reasonable controller C that switches the green traffic lights in the following order: L1 and L3 together, then L2, then L4. Use the variable names L1, L2, L3, L4, green, yellow, red, amber.

Reply with your UCLID5 code inside one unique code block.

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