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

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


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

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