123456789101112131415161718192021222324252627282930313233343536373839404142434445464748 |
- 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
- ]
|