Please email me your completed SMV program, including your specifications and fairness constraints, as well as an intuitive description of any bugs you found.

I hope this is an easy and fun exposure to CTL model checking, as well as an intro to the NuSMV or nuXmv model checkers. NuSMV is a not super-old re-creation and extension of SMV, which was the original symbolic model checker. nuXmv is an even newer system from the same group, so NuSMV is no longer actively maintained, but it's open-source and nuXmv isn't. Therefore, in the past, I've used NuSMV for this assignment. However, recently, I've had trouble building NuSMV from source, so you may as well use the pre-compiled binaries for either tool (which are free for non-commercial use). Both will work equally well for this assignment.

Mutual exclusion is a classic problem from concurrent programming, operating systems, distributed systems, etc. The basic problem is to write code for two programs that execute at the same time, and you don't want both of them to execute a special part of the code (called the "critical section") at the same time. In practice, the critical section would be the code required to access a shared resource (shared variable, data file, printer, etc.).

One correct solution (based on Leslie Lamport's Bakery Algorithm) is as follows:

-- Global variables:  n1, n2, both initialized to 0.
-- Process P1
--	1: n1 = 1
--	2: n1 = n2+1;
--	3: if (n2!=0)&(n2<n1) goto 3	-- waiting for critical section
--	4: /* this line is the critical section */
--	5: n1 = 0
--	6: goto 1
-- Process P2
--	1: n2 = 1
--	2: n2 = n1+1;
--	3: if (n1!=0)&(n1<n2) goto 3	-- waiting for critical section
--	4: /* this line is the critical section */
--	5: n2 = 0
--	6: goto 1

In an attempt to get around this problem, I've inserted an extra loop between statements 1 and 2, which waits in case the global variables get too large. Your job is to use SMV to determine if my attempted fix was successful or not. (Hint: It's not!)

My SMV description of this protocol contains additional details about exactly what properties a correct solution must obey, and what assumptions you can make about the process scheduling. You will need to add CTL (or LTL) specifications to tell SMV what properties you want to check, as well as fairness constraints to eliminate vacuous error traces (e.g. P1 never gets to the critical section because it never gets to execute at all).

For the assignment, you'll need to get NuSMV or nuXmv. You can download and build NuSMV yourself. However, as mentioned above, I'm finding that the newest version that used to build easily on our department Linux machines isn't building correctly anymore (apparently problems between Python 2 and 3). Fortunately, they also have pre-compiled binaries for Linux, Windows, and MacOS, so you all should be in good shape. Or on the CS department Linux machines, I put the pre-compiled binaries in /isd/users/software/NuSMV-2.6.0-Linux/bin/NuSMV and /isd/users/software/nuXmv-2.0.0-Linux/bin/nuXmv

You'll also definitely want to browse the manuals for NuSMV and/or nuXmv. There's also a nice tutorial for NuSMV that should work equally well to get started with nuXmv.