Project 3:

I hope this is an easy and fun exposure to the SMV model checker. I have written an SMV description of the overused Dining Philosopher's Problem. However, my description is buggy. Your job is to fix it.

You will need to add a fairness constraint to specify that no one eats forever. More importantly, though, the current version is prone to deadlock (where no one can make progress) and also starvation (where a philosopher never gets to eat because the other philosophers always beat him to the forks). You will need to add some code to prevent this. I think the most simple solution is to add a token that gets pass around among the philosophers to break symmetry and grant priority. (See the Synchronous Arbiter example for a similar problem in circuits.)

Unlike the previous assignments, SMV is a self-contained program, so you don't need David Long's BDD and memory management packages. Instead, what you need are the SMV executable. The version I'm linking to is precompiled for SPARC Solaris 2.5.1 (on Columbia). If you want to build your own, let me know, or grab the tar file from the SMV directory. The directory is worth browsing in general, especially for the SMV manual and the examples subdirectory. This is a link to the buggy dining philosophers program I'm giving you.