Create a model of Mutex 1 (from the Mutex handout) in SPIN. Use that model to show that it is possible to have more than 1 process in the critical section at the same time. Strategically add printfs to your code so that the MSC contains meaningful information. Mail me (jones@cs.byu.edu) the msc.ps from a guided simulation that shows the error. Due last day of class.
Convert the expression (a /\ b) \/ (a /\ c) to a BDD. Use the algorithm we are developing in class. Show your results and BDD tables. Will be moved back to Wednesday if we don't get through an example on friday.
Translate a verse (or equivalent) from the religious text of your choice to CTL*. Due at the beginining of class Friday 9/26.
Two formulas that describe correct behaviors of mutex protocols.
Translate the behavior of two processes using Mutex1 into a Kripke structure. Find two traces in the Kripke Structure: one that allows two processes to enter the critical section and one that starves a process from access to the critical section. Turn in your traces only. Do not turn in, or even write (if you don't have to), the entire Kripke Structure. Due Friday, September 19 at the start of class.