====== Assignment 1 ======
Assignment 1 due date:before class on Wednesday March 18th.

The following is a Spin description of a mutual exclusion algorithm using a semaphore variable ''r''. You should be able to show (in JSpin) that the algorithm is safe (does not allow two processes in the critical area at the same time), and does not deadlock. However, it is not fair (i.e. there is no guarantee, under weak fairness, that processes will eventually get into the critical region). If using JSpin, make sure there are no spaces in the file names.

<code>

/* Mutex via semaphores 
   []<>p1 will fail even with weak fairness
   turned on
*/

int r = 1; /* semaphore */
bit p1, p2 = 0;


active proctype P1() {
do
:: 	atomic{r > 0 -> r = 0}; /* request(r)*/
	p1 = 1; /* critical section */
	p1 = 0;
	atomic { r = 1}; /*release(r) */
od
}

active proctype P2() {
do
:: 	atomic{r > 0 -> r = 0}; /* request(r)*/
	p2 = 1; /* critical section */
	p2 = 0;
	atomic { r = 1}; /*release(r)}*/
od
}
</code>

You must come up with an Event-B model for the above program. Prove that your model is safe and deadlock free.

Hint: In Event-B you have to think **events** rather than statements in a coding language.

Submit a Latex hardcopy of your work and a mutex.zip file via electonic submit:
   submit -l 6411 a1 mutex.zip mutex.tex mutex.pdf

The zip file can be created from the Rodin export facility (see Rodin Tutorial).