Pamef/tp/lecteurEcrivain_famineEcrivain.csp

define NE 1
define NL 111

ECRIVAIN ==
	*[ true ->
		sleep (random(10,10000));
		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 ==
	nl : integer := 0;
	*[
		(i:1..NL) 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) nl = 0; ecrivain[i] ? acces () -> ecrivain[i] ? libere ()
	]

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