A) Simplification des calculs

Pot B = PoT A B (avec A = True)
Inev B = Inev A B (avec A = True)

TH(Pot F ) = U n≥0 Xn 
où Xo = TH(F) et
et Xk = Pre(Xk−1) U Xk−1


TH(Inev F ) = U n≥0 Yn 
où Yo = TH(F) et
et Yk = PreTilde(Yk−1) U Xk−1

Systeme non equitable

B) All (A1 => Pot T1 )

Calcul de Pot T1

TH(T1) = {4,7} et Xo = {4,7}

Xk = Pre(Xk−1) U Xk−1}

X1 = X0 U Pre(X0)
X1 = {4,7} U Pre({4,7}) avec Pre({4,7} = {2,5}
X1 = {2,4,5,7}

X2 = {2,4,5,7} U Pre({2,4,5,7}) avec Pre({2,4,5,7}) = {1,2,3,5 8}
X2 = {1,2,3,4,5,7,8}

X3 = {2,3,4,5,7,8} U Pre({2,3,4,5,7,8}) avec Pre({2,3,4,5,7,8}) = {1,2,3,5,6,8}
X3 = S

TH(Pot T1) = S

Calcul TH(Inev T1)
TH(T1) = {4,7} et Y0 = {4,7}
et Yk = PreTilde(Yk−1) U Xk−1

Y1 = PreTilde(Y0) U Y0 avec Pretilde({4,7,})
        2 not in Pretilde({4,7,}) car 5 not in {4,7}
	5 not in Pretilde({4,7,}) car 8 not in {4,7}
	donc Pretilde({4,7,}) = {}
	et Y1 = Y0
	donc TH(Inev T1) ={4,7}
	
	
Systeme Equitable
TH(T1) = {4,8} et Y0 = {4,8}
et Yk = PreTilde(Yk−1) U Xk−1

Y1 = = PreTilde(Y0) U Y0 avec Pretilde({4,8,}) = {5}
Y1 = {4,5,8}

Pretilde({4,5,8) = {2,4,5,8}
Y2 = {2,4,5,8}

Pretilde({2,4,5,8) = {2,4,5,8,9 }
Y3 =  {2,4,5,8,9}

Pretilde{2,4,5,8,9} = {2,4,5,8,9, 6}
Y4 = {2,4,5,8,9, 6}

Y5 = Y4 U Pretilde({2,4,5,8,9, 6}} avec Pretilde({2,4,5,8,9, 6}} ={2,4,5,8,9, 6}
donc Y5 = Y4
et TH(Inev T1) = {2,4,5,8,9, 6} =  S \ {1,3,7}
et {1,3,7} = TH (O1)

TH( A1 => Inev T1)

TH(A1) = {2,5,6,9)

TH(A=>B) = TH (-A U B) = TH(-A) U TH(B) = S\TH(A) U TH(B)

S\TH(A1) U TH(Inev T1)  = {1,3,4,7,8} U {2,4,5,8,9, 6} = S
Finalement TH( A1 => Inev T1) = S


Leadsto Uppaal : phi --> Psi

 All( Phi => Inev Psi)
 [] ( Phi => <> Psi)


Exo 3:
======

rappel "A1 => Inev T1" caracterise absence de famine 

P1 : Caracteriser un etat ou un des processus (Proc 1 par ex)
est en situation de famine.

A1 /\ All (A1   => - Inev  T1)
All Trop fort 
- Inev T1 = Some - T1

Reponses : 
A1 /\ Some - T1 (En attente et un chemin ou on travaille jamais)
Some A1  (en attente "infinie")


 - (A1   =>  Inev  T1) ??
 - ( (-A1)  U Inev T1)
 -(-A1) /\ - Inev T1
 A1 /\ Some -T1


Version equitable

Evaluation de A1 /\ Some T1
= TH(A1 /\ Some T1) = TH( - (A1 => Inev T1)_
                    = S \ TH( (A1 => Inev T1)_
		    = S \ S = {}
		    
Version Non equitable

TH(Inev T1) = {4,7}
TH(A1 => Inev T1) = {1, 3, 6, 4, 7}
TH( - (A1 => Inev T1)) = S \ {1, 3, 6, 4, 7}
                       = {2,5,8}