Tiago's solution to problem 1

/* DTU Course 02158 Concurrent Programming
 *   Lab 2
 *   spin5.pml
 *     Skeleton PROMELA model of mutual exlusion by coordinator
 */

#define N 5

bool enter[N];  /* Request to enter flags */
bool ok[N];     /* Entry granted flags    */

int incrit = 0; /* For easy statement of mutual exlusion */

/*
 * Below it is utilised that the first N process instances will get 
 * pids from 0 to (N-1).  Therefore, the pid can be directly used as 
 * an index in the flag arrays.
 */

active [N] proctype P()
{
	do
	::	/* First statement is a dummy to allow a label at start */
		skip; 

entry:	
		enter[_pid] = true;
		/*await*/ ok[_pid] ->

crit:	/* Critical section */
		incrit++;
		assert(incrit == 1);
		incrit--;
  	
exit: 
		/* Your code here */
		enter[_pid] = false;
		
		/* Non-critical setion (may or may not terminate) */
		do :: true -> skip :: break od

	od;
}

active proctype Coordinator() {	
	short t1 = 0;
	short total_incrit = 0;
	do
	::	
		
		if
		:: t1 >= N -> t1=0;
		:: t1 < N ->		
			if
         			:: atomic{(enter[t1] && !ok[t1])} ->  // Grant access if no one is in the critical section
               			if
				:: total_incrit == 0 ->
					ok[t1] = true;
               				total_incrit++;
				fi;
          			:: atomic{(!enter[t1] && ok[t1])} ->  // Revoke access if the process has left the critical section
               			ok[t1] = false;
               			total_incrit--;
         			fi;
		fi;
		t1++;
	od;
}

ltl fair0 { []( (P[0]@entry) -> <> (P[0]@crit) ) }