define NE 100
define NL 100

ECRIVAIN ==
	*[ true ->
		sleep (random(10,10000));
		ctrl ! block ();
		ctrl ! acces ();
		print("Writing ");
		ressource := ressource + 1;
		print(ressource);
		sleep (1000);
		print(" done.\n");
		ctrl ! libere ()
	]


LECTEUR ==
	*[ true ->
		ctrl ! acces ();
		print ("Read : " + ressource + "\n");
		ctrl ! libere ()
	]

CTRL ==
	lock : boolean := false;
	nl : integer := 0;
	*[
		(i:1..NL) not lock; lecteur[i] ? acces() -> nl := nl + 1; print("+ 1 : " + nl + " readers\n")
	[]
		(i:1..NL) lecteur[i] ? libere () -> nl := nl - 1 ; print("- 1 : " + nl + " readers\n")
	[]
		(i:1..NE) not lock; ecrivain[i] ? block () -> lock := true
	[]
		(i:1..NE) lock & nl = 0; ecrivain[i] ? acces () ->
			ecrivain[i] ? libere();
			lock := false
	]

MAIN ==
	ressource : integer := 0;
	[
		ecrivain [i:1..NE] :: ECRIVAIN
	||
		lecteur [i:1..NL] :: LECTEUR
	||
		ctrl :: CTRL
	]