1. (10 points) Answer problems 1(a) through 1(e) from the SPIN Verification Examples and Exercises

2. (30 points) Model the following mutual exclusion algorithm with PROMELA (25 points) and prove its correctness or incorrectness with SPIN (5 points).

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. (30 points) Write a Promela model for the below problem (25 point) and use SPIN to find a solution (5 points).

A farmer wants to cross a river and take with him a wolf, a goat, and a cabbage. There is a boat that can fit himself plus either the wolf, the goat, or the cabbage. If the wolf and the goat are alone on one shore, the wolf will eat the goat. If the goat and the cabbage are alone on the shore, the goat will eat the cabbage. How can the farmer bring the wolf, the goat, and the cabbage across the river?