Program

Module process = 5;

flag[process]=0;
k[process]=0;
pc[process]=1;
inCR[process]=0;
turn1[process]=0;
turn2[process]=0;
turn3[process]=0;

p of process;

p: {

  pc[p]==1 -> k[p]=1, pc[p]=2;
  pc[p]==2 & k[p] < 3 -> pc[p]=3;
  pc[p]==3 -> flag[p]=k[p], pc[p]=4;
  pc[p]==4 & k[p]==1 -> ALL(q of process: turn1[q]=0), 
                            turn1[p]=1, pc[p]=5;
  pc[p]==4 & k[p]==2 -> ALL(q of process: turn2[q]=0), 
                            turn2[p]=1, pc[p]=5;
  pc[p]==4 & k[p]==3 -> ALL(q of process: turn3[q]=0), 
                            turn3[p]=1, pc[p]=5;
  pc[p]==5 & k[p]==1 & (ALL(q of process: p==q | (p!=q & flag[q]<k[p])) | 
                            turn1[p]==0) -> pc[p]=6;
  pc[p]==5 & k[p]==2 & (ALL(q of process: p==q | (p!=q & flag[q]<k[p])) | 
                            turn2[p]==0) -> pc[p]=6;
  pc[p]==5 & k[p]==3 & (ALL(q of process: p==q | (p!=q & flag[q]<k[p])) | 
                            turn3[p]==0) -> pc[p]=6;
  pc[p]==5 & k[p]==1 & (!(ALL(q of process: p==q | (p!=q & flag[q]<k[p]))
                            | turn1[p]==0)) -> pc[p]=5;
  pc[p]==5 & k[p]==2 & (!(ALL(q of process: p==q | (p!=q & flag[q]<k[p])) 
                            | turn2[p]==0)) -> pc[p]=5;
  pc[p]==5 & k[p]==3 & (!(ALL(q of process: p==q | (p!=q & flag[q]<k[p])) 
                            | turn3[p]==0)) -> pc[p]=5;
  pc[p]==6 -> k[p]=k[p]+1, pc[p]=2;
  pc[p]==2 & (!(k[p]<3)) -> pc[p]=7;
  pc[p]==7 -> ALL(q of process: inCR[q]=inCR[q] + 1), pc[p]=8;
  pc[p]==8 -> ALL(q of process: inCR[q]=inCR[q] - 1), pc[p]=9;
  pc[p]==9 -> flag[p]=0, pc[p]=1;

}