1

Table de synchronisation

Formule LTL

\varphi = G\neg (\text{Sur1} \wedge \text{Sur2})

2

 0 process P1() {
 1   while (true) {
 2     non_critique_1;
 3     wantP1 = 1:
 4     while (wantP2 == 1) {
 5       if (turn == 2) {
 6         wantP1 = 0;
 7         while (turn != 1);
 8         wantP1 = 1; } }
 9     critique_1;
10    turn = 2;
11    wantP1 = 0; } }

Table de synchronisation