Import CSP examples

tp/calcul.csp

@@ -0,0 +1,38 @@
+CALCULATEUR ==
+	nb, coef : integer;
+	gestionnaire?calcul(nb, coef);
+	nb := nb * coef;
+	gestionnaire!resultat(nb)
+
+PROCESSUS ==
+	taille, init : integer;
+	actif : boolean := true;
+	*[
+		actif; lanceur?calcul(taille, init) ->
+			tab : [1..taille] integer := [1..taille] init;
+			[
+				calculateur [i:1..taille] :: CALCULATEUR
+			||
+				gestionnaire ::
+					*[
+						(i:1..taille) calculateur[i]!calcul (tab[i], i) -> skip
+					[]
+						(i:1..taille) calculateur[i]?resultat (tab[i]) -> skip
+					]
+			];
+			print (tab + "\n")
+	[]
+		actif; lanceur?fin() -> actif := false
+	]
+
+MAIN ==
+	[
+		processus :: PROCESSUS
+	||
+		lanceur :: 
+			processus!calcul(10,1); 
+			processus!calcul(10,2); 
+			processus!fin()
+	]
+	
+	

tp/deleg.csp

@@ -0,0 +1,17 @@
+PROCESSUS ==
+	print(compteur+"\n"); 
+	compteur := compteur - 1;
+	[
+		compteur = 0 -> skip
+	[]
+		compteur /= 0 -> 
+			[
+				processus :: PROCESSUS	
+			]		
+	]
+
+MAIN ==
+	compteur : integer := 4;
+	[
+		processus :: PROCESSUS
+	]

tp/dog.csp

@@ -0,0 +1,48 @@
+
+EMETTEUR ==
+	message : string; cpt : integer := 0;
+	alea : integer;
+	* [ true ->
+		cpt := cpt + 1;
+		message := "message " + cpt;
+		recepteur!message;
+		sleep(1000);
+		alea := random (1, 10); /* action aleatoire */
+		[ 
+			alea <= 2 -> recepteur?relance()
+		[]
+			alea > 2 -> skip
+		]
+	]
+	
+RECEPTEUR ==
+	message : string; alive : boolean := true;
+	*[ 
+		alive; emetteur?message -> dog!ack(); print (message + "\n")
+	[]
+		alive; dog?erreur() -> print("erreur\n"); emetteur!relance(); dog!ackErreur ()
+	]
+
+DOG ==
+	delai : integer := 4;
+	*[
+		recepteur?ack() -> delai := 4
+	[]
+		horloge?bip() -> delai := delai -1
+	[]
+		delai = 0 -> recepteur!erreur(); recepteur?ackErreur(); delai := 4
+	]
+
+HORLOGE ==
+	*[true -> dog!bip();sleep(1000)]
+
+MAIN ==
+	[ 
+		emetteur :: EMETTEUR 
+	|| 
+		recepteur :: RECEPTEUR 
+	|| 
+		dog :: DOG
+	||
+		horloge :: HORLOGE
+	]

tp/lecteurEcrivain0.csp

@@ -0,0 +1,39 @@
+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
+	]

tp/prodCons0.csp

@@ -0,0 +1,45 @@
+define NP 1
+define NC 4
+define N 4
+
+PRODUCTEUR ==
+		nb : integer := 0; message : string;
+		*[
+			true ->
+				message := "objet num " + nb;
+				liste!prod(message);
+				print ("production " + i + " : " + message + "\n");
+				nb := nb + 1
+		]
+		
+BUFFER ==
+		tampon : [0..N-1] string := [0..N-1] "";
+		dernier,premier,nb : integer := 0;
+		message : string := "";
+		*[
+			(i:1..NP) nb /= N ; producteur[i]?prod(tampon[dernier]) ->
+				dernier := (dernier +  1) mod N; nb:=nb+1;
+				print ("P - positions " + " : " + premier + dernier + " - nbr d'elements : " + nb + "\n")
+		[]
+			(i:1..NC) nb = N & true; consommateur[i]!cons(tampon[premier],(N+dernier-premier)mod N) ->
+				premier := (premier + 1) mod N; nb := nb-1;
+				print ("C - positions " + " : " + premier + dernier + " - nbr d'elements : " + nb + "\n")
+		]		
+
+CONSOMMATEUR ==
+		message : string; k: integer;
+		*[ 
+			true ->
+				liste?cons(message,k);
+				print ("consommateur " + i + " : " + message + "\n");
+				sleep(500*i)
+		]
+
+MAIN ==
+		[
+			producteur[i:1..NP] :: PRODUCTEUR
+		||
+			consommateur[i:1..NC] :: CONSOMMATEUR
+		||
+			liste :: BUFFER
+		]

tp/prog.csp

@@ -0,0 +1,38 @@
+define N 20
+
+
+PROCESSUS ==
+[
+    i = 0 -> 
+       x : integer:= random(0,N); print (i + "? " + x + "\n");
+	   processus[1]!couple(i,x)
+
+  []
+     i /= 0 & i /= N ->	
+        x, j, k, val : integer;
+        x := random(0,N); print (i + "? " + x + "\n");
+        k := i;
+        *[
+            processus[i-1]?couple(j,val) ->
+				[
+				    x < val -> processus[i+1]!couple(k,x); x:=val; k:=j
+				[]
+				    x >= val -> processus[i+1]!couple(j,val)
+                ]
+          ];
+          processus[i+1]!couple(k,x)
+
+    []
+        i = N ->	
+            valeur, j : integer;
+            *[
+                processus[N-1]?couple(j,valeur) -> print (j + ": " + valeur + "\n")
+            ]
+]
+    
+MAIN ==
+	[
+		processus[i:0..N] :: PROCESSUS
+	]
+	
+	

tp/semaphore.csp

@@ -0,0 +1,34 @@
+define Nproc 4
+
+P ==
+    [
+            i = 1 -> 
+                   sem!init(1)
+            []
+            i /= 1 ->	skip
+    ];
+	*[ true ->
+		sem!P ();
+		print ("ressource : " + ressource + "\n");
+		ressource := ressource + i;
+		sleep(10000);
+		sem!V ()
+	]
+
+SEMAPHORE ==
+	val : integer := 0;
+	*[
+		(i:1..Nproc) proc[i]?V() -> val := val+1  /*print("(" + val + ")" + "\n")*/
+	[]
+		(i:1..Nproc) val >0; proc[i]?P () -> val := val -1 
+	[]
+		(i:1..Nproc) proc[i]?init (val) -> skip
+	]
+
+MAIN == 
+	ressource : integer := 0;
+	[
+		proc [i:1..Nproc] :: P
+	||
+		sem :: SEMAPHORE
+	]

tp/sieve.csp

@@ -0,0 +1,45 @@
+define MAX 1000
+define NS  10
+
+SIEVE ==
+	[
+		i = 0 ->
+			console!2;
+			n : integer := 3;
+			*[
+				n < MAX -> sieve[1]!n; n := n + 2
+			]
+	[]
+		i = NS + 1 ->
+			n : integer;
+			*[
+				sieve[NS]?n -> console!n
+			]
+	[]
+		(i/=0) & (i/=NS + 1) ->
+			p, mp : integer;
+			sieve [i-1]?p;
+			console!p;
+			mp := p;
+			m : integer;
+			*[
+				sieve[i-1]?m ->
+					* [ m > mp -> mp := mp + p];
+					[
+						m = mp -> skip
+					[]
+						m < mp -> sieve[i+1]!m
+					]
+			]
+	]
+
+MAIN ==
+	[
+		sieve [i:0..NS + 1] :: SIEVE
+	||
+		console ::
+			n : integer;
+			*[
+				(i:0..NS + 1) sieve[i]?n -> print (n + "\n")
+			]
+	]