/* Algorithme d'exclusion mutuelle du TD2 */ #define trans(garde,action,etat) d_step{garde -> action} goto etat bool b[2]; /* variables globales */ int k; proctype user(bit id) { depart: if :: trans(true,b[id]=false,demande) fi; demande: if :: trans(k!=id,skip,attente) :: trans(k==id,skip,section_critique) fi; section_critique: if :: trans(true,b[id]=true,depart) fi; attente: if :: trans(!b[1-id],skip,attente) :: trans(b[1-id],skip,retour_demande) fi; retour_demande: if :: trans(true,k=id,demande) fi; } init /* pid 0 */ { atomic { k=0; b[0]=false; b[1]=false; run user(1); /* pid 1 */ run user(0) /* pid 2 */ } } /* #define sc0 (user[1]@section_critique) #define sc1 (user[2]@section_critique) */ /* [] exclusion mutuelle [] (!sc0 || !sc1) ! <> (sc0 && sc1) */