Mandatory 2 - Benjamin - Multialley

/* Mutual exclusion with a semaphore, implemented by channels. */

#define N_d 4  /* Number of processes in critical section */
#define N_u 4
#define P(S) do :: atomic { S > 0 -> S--;break } od
#define V(S) atomic { S++ }

int S_down = 1;
int S_up = 1;

int down = 0;
int up = 0;

byte critical = 0;
int incrit = 0;

active [N_d] proctype D () 
{	
do :: 
	skip;
entry:

//For cars with downsyndrome
P(S_down);

if
:: down == 0 -> P(S_up);
:: down != 0 -> skip;
fi;

down = down + 1;
V(S_down);

incrit:

	assert(down > 0 &&  up == 0);

leave:

	down = down - 1;
	if
	:: down == 0 -> V(S_up);
	:: down != 0 -> skip;
	fi;
	
od;
}

active [N_u] proctype U()
{ 
do ::
	skip; 

entry:

P(S_up);

if
:: up == 0 -> P(S_down);
:: up != 0 -> skip;
fi;

up = up + 1;
V(S_up);




incrit:
	assert(up > 0 &&  down == 0);

leave:

	up = up - 1;
	if
	:: up == 0 -> V(S_down);
	:: else -> skip
	fi;
od;
}



ltl fair1 { [] ((D[1]@entry) -> <> (D[1]@incrit))}