1. (40 points) Write algorithms to compute EG and EU as fix-point calculations using either the Cudd or your library from Homework 12. Include tests that automatically check the correctness of your implementation. 20 points are allocated to the algorithms and the other 20 points are allocated to the quality of the tests.

2. (40 points) Verify the Hyman's Mutual Exclusion protocol below for two threads using the EG and EU code from the first problem. Check for mutual exclusion (e.g., there is no path where the protocol does not work) and the absence of starvation (e.g., every request for the critical section is eventually granted). Be sure to clearly indicate the CTL formulas for each property.

Hyman's Mutual Exclusion

void lock (int i) {
      int j = 1 - i;
      signal[i] = 1;
      while (turn != i) {
         while (signal[j]);
         turn = i;
      }
 }
 
void unlock(int i) {
   signal[i] = 0;
}

3. (40 points) Verify the Peterson's mutual exclusion protocol below for two threads using the EG and EU code from the first problem. Check for mutual exclusion (e.g., there is no path where the protocol does not work) and the absence of starvation (e.g., every request for the critical section is eventually granted). Be sure to clearly indicate the CTL formulas for each property.

Peterson's Mutual Exclusion

void lock (int i) {
      int j = 1 - i;
      signal[i] = 1;
      turn = j;
      while (signal[j] && turn != i);
 }
 
void unlock(int i) {
   signal[i] = 0;
}