Traffic Lights

We will only model one traffic light per each direction (the second one just repeats the same behaviour). For instance, in the picture above, the vertical light is green and the horizontal one is red. Initially, both directions are red. When a car arrives, it is detected by a sensor and its corresponding light turns to green. However, this only happens if the other direction is still in red; otherwise, it will wait until the other direction is closed. Once any direction is in green, it will turn next to orange (there is a timer, but we will not model the delay) and then it will turn to red again.

What to do

Using the initial marking depicted above:

• Formalise the problem in Promela
• Deadlock: check that your encoding does not generate a deadlock
  
• Safety: check that a situation in which both traffic lights are not red is not reachable. Explain the obtained result.
  
• Liveness: check whether both traffic lights can reach each color infinitely often. Explain the obtained result.

For formalising the problem, you must create two processes, P[0] and P[1] and the corresponding variables light[0] and light[1]. Each process P[i] will contain an infinite loop where light[i] makes the cyclic changes green -> orange -> red, but waiting when needed. You will have to model some kind of synchronisation to avoid situations in which both directions are open (i.e. they are not in red at the same time).