EXERCISE 2.5. The following program is a mutual exclusion protocol for two processes due to Pnueli [118]. 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: 10: loop forever do begin 11: Noncritical section 12: (Yi, s) := (1, i); 13: wait until ((Y1-i = 0) V (s # i)); 14: Critical section 15: 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. 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. EXERCISE 2.5. The following program is a mutual exclusion protocol for two processes due to Pnueli [118]. 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: 10: loop forever do begin 11: Noncritical section 12: (Yi, s) := (1, i); 13: wait until ((Y1-i = 0) V (s # i)); 14: Critical section 15: 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. 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