Chapter 9 of the course text.

1. (5 points) Create fairness constraints for the system in Homework 3 that limits the verification to paths that release fork1 and fork2 in a finite amount of time.
2. (15 points) Perform on-the-fly model checking to see if our system satisfies the property on fair paths(i.e., check the intersection of the model with fairness and the never claim). Please show the entire search graph as we did in class.
3. (5 points) Write the dining philosophers model in Promela and verify the same properties in SPIN. Submit the Promela for the model and the SPIN output. Some simple instructions for installing and using Spin are in the Tools page. Use the atomic keyword to make it so each location is a single atomic step so the state space is smaller than 15 states.
4. (5 points) Implement mutex 1 from Homework 1 in PROMELA and verify mutual exclusion and deadlock freedom with SPIN. Attach the output from the verification to the homework. The PROMELA should have two processes both using Mutex 1 to arbitrate access to the critical section.
5. (5 points) Repeat the previous problem for mutex 2.