Examples A traffic light system to be installed to control the movement of cars on two crossing roads (see the below Figure). oo. 00 +000 Figure: Traffic light system Each traffic light has Red, Yellow and Green colours. The colour signals of the traffic lights that are located on the same road are identical all the time. The signals of the traffic lights that are located on the crossing ronds are always opposite (e.g. if one traffic light shows the Green signal, another must show the Red signal). After the Red signal, a traffic light always shows an intermedinte Yellow colour. (a) Draw a state chart diagram to represent behaviour of the traffic light system. (b) Write TLA specification to model the behaviour and check safety and liveness properties of the traffic light system. TLA specification should have: i. Correct structure (declaration of constants and variables; initial and next state predicates, a type invariant and a theorem; meaningful comments). ii. Actions of the traffic light system, defining its infinite (no deadlock) behaviour. (a) With IF-THEN-ELSE operator. iii. Invariants. (a)After the Green state, a traffic light will have the Red state. (b)The signals of the traffic lights that are located on the crossing roads are always opposite iv. Liveness properties. (a) Showing Red signal leads to the Yellow signal. (b)Traffic light system eventually often shows both Green and Red signals