. The following program is a mutual exclusion protocol for two processes due to Pnueli [1]. There is a single shared variable s which is either 0 or 1, and initially 1. Besides, each process has a local Boolean variable y that initially equals 0. The program text for process Pi (i = 0, 1) is as follows: loop forever do begin l1: Noncritical section l2: (yi, s) := (1, i); l3: wait until ((y1−i = 0) ∨ (s ≠ i)); l4: Critical section l5: yi := 0 end. Here, the statement (yi, s) := (1, i); is a multiple assignment in which variable yi := 1 and s := I is a single, atomic step. Please answer following questions: a) Define the program graph of a process in Pnueli’s algorithm. b) Determine the transition system for each process. c) Construct their parallel composition. d) Check whether the algorithm ensures mutual exclusion. e) Check whether the algorithm ensures starvation freedom. f) The last two questions may be answered by inspecting the transition system