# TD 2 -- Théorie et pratique de la concurrence

###### tags `TD` `M1 S1` `Concurrence`
[Sommaire](/bAJa0viuQp68XN74HxpVJA)
> [time= 6 oct 2020]

[TOC]

## Exercice 1
### Enoncé

### Réponse

byte N = 0;
bool fin1 = false;
bool fin2 = false;
proctype P1(){
	byte i = 1;
	byte temp = 0;
	
	do
		:: i < 5 -> temp = N + 1; N = temp; i++
		:: else -> break;
	od;
	printf("processus 1 %b", N);
	fin1 = true;
}
	
proctype P2(){
	byte i = 1;
	byte temp = 0;
	do
		:: i < 5 -> temp = N + 1; N = temp; i++
		:: else -> break;
	od;
	printf("processus 1 %b", N);
	fin2 = true;
}

init{
	run P1(); run P2();
	(fin1 && fin2);
	printf("%b", N)
	assert(N >= 2 && N <= 10)
}

## Exercice 2
### Enoncé

### Réponse

#define cs1 (P1@CS) 
#define cs2 (P2@CS) 
#define pre1 (P1@PRE) 
#define pre2 (P2@PRE)

bool D1=false, D2=false; 
byte turn=1;
byte nbcs = 0;
active proctype P1() {
 do ::
		if
			:: true;
			:: true -> false;
		fi;

PRE: 	D1=true;
		turn=2;
		(D2==false || turn==1);

CS:		skip; 
POST: 	D1=false
 od
}

active proctype P2() {
 do ::
		if
			:: true;
			:: true -> false;
		fi;

PRE: 	D2=true;
		turn=2;
		(D1==false || turn==2)

CS:		skip;
POST: 	D2=false
 od
}

## Exercice 3
### Enoncé

### Réponse

#define cs1 P[1]@CS
#define cs2 P[2]@CS
#define pre1 P[1]@CS
#define pre2 P[2]@CS

byte req = 0;
byte autorisation = 0;
bool fin = true;

proctype Pi(byte i)
{
do::
	if 
		:: true 
		:: true -> false; goto END
	fi;
PRE:	do
			:: (autorisation == i) -> break
			:: true -> req = i;  skip
		od

CS:		skip

POST:	fin = true
		req = 0

od;
END: skip;
}

active proctype S(){
	do::
		(req != 0);
		fin = false;
		autorisation = req;
		(fin == true);
		autorisation = 0;
	od;
}

init {
run Pi(1); run Pi(2);
}

## Exercice 4
### Enoncé

### Réponse