#define NOMBRE_PHILO 5 
/* Les ressources = fourchettes */ 
#define FOURCHETTE_LIBRE 1
bsem fourchettes[NOMBRE_PHILO] = FOURCHETTE_LIBRE;
#define FOURCHETTE_GAUCHE(p) ((p == 0) -> 4 : p-1) 
#define FOURCHETTE_DROITE(p) ((p == 4) -> 0 : p+1) 
/* L'etat des philosophes */ 
#define PENSE -1
#define FAIM   0
#define MANGE  1
int etat[NOMBRE_PHILO] = PENSE; 
inline PENSER(p)  {etat[p] = -1} 
inline AFAIM(p)   {etat[p] = 0} 
inline MANGER(p)  {etat[p] = 1} 
inline PRENDRE(f) { /** a completer **/ }
inline LIBERER(f)  { /** a completer **/ } 
/* Les philosophes */ 
active [NOMBRE_PHILO] proctype Philosophe() 
{ int fourchette_gauche = FOURCHETTE_GAUCHE(_pid); 
  int fourchette_droite = FOURCHETTE_DROITE(_pid); 
  do :: 1 ->
     PENSER(_pid); 
     AFAIM(_pid); 
     PRENDRE(fourchette_droite); 
     PRENDRE(fourchette_gauche); 
     MANGER(_pid);
     LIBERER(fourchette_droite); 
     LIBERER(fourchette_gauche)
  od 
}