|
|
@@ -0,0 +1,48 @@
|
|
|
+define NE 4
|
|
|
+define NL 11
|
|
|
+
|
|
|
+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
|
|
|
+ ]
|
