define NE 4 define NL 11 ECRIVAIN == *[ true -> sleep (random(10,10000)); ctrl!acces (); ressource := ressource + 1; sleep (1000); ctrl!libere () ] LECTEUR == *[ true -> ctrl!acces (); print ("ressource : " + ressource + "\n"); ctrl!libere () ] CTRL == nl : integer := 0; *[ (i:1..NL) lecteur[i]?acces() -> nl := nl + 1; print("(" + nl + ")" + "\n") [] (i:1..NL) lecteur[i]?libere () -> nl := nl - 1 [] (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 ]