The behaviour of a railway level crossing is depicted in the following labelled transition system. down green DRT URT train train down green DR UR DG train tcross DGT up red ccross ccross car car URC DRC up train Ppu red train URCT DGC train tcross DGCT DRCT car up red The system has 12 states, according to whether the barrier for cars is up (U) or down (D); the signal for trains is red (R) or green (G) - also depicted by the colour of the state; and whether or not there is a car (C) or a train (T) waiting to cross. The actions are as introduced in the level-crossing example in the lectures. 1. Let TW(x) and CW(x) be the following predicates defined on the states of the system. TW(x) = "a train is waiting at a red signal" CW(x) "a car is waiting as the barrier is down" List the states for which TW(x) is true; and the states for which CW(x) is true; and the states for which TW(x) and CW(x) are both true. 2. Does this system satisfy the desired safety property of a level crossing? Explain why or why not. 3. Now consider the liveness properties again. (a) Is it now the case that, if the signal is red when a train arrives, then the signal will eventually turn green? Explain your answer. (b) Is it now the case that, if the barrier is down when a car arrives, then the barrier will eventually go up? Explain your answer.