define Nproc 4

P ==
    [
            i = 1 -> 
                   sem!init(1)
            []
            i /= 1 ->	skip
    ];
	*[ true ->
		sem!P ();
		print ("ressource : " + ressource + "\n");
		ressource := ressource + i;
		sleep(10000);
		sem!V ()
	]

SEMAPHORE ==
	val : integer := 0;
	*[
		(i:1..Nproc) proc[i]?V() -> val := val+1  /*print("(" + val + ")" + "\n")*/
	[]
		(i:1..Nproc) val >0; proc[i]?P () -> val := val -1 
	[]
		(i:1..Nproc) proc[i]?init (val) -> skip
	]

MAIN == 
	ressource : integer := 0;
	[
		proc [i:1..Nproc] :: P
	||
		sem :: SEMAPHORE
	]