PROCESSUS == print(compteur+"\n"); compteur := compteur - 1; [ compteur = 0 -> skip [] compteur /= 0 -> [ processus :: PROCESSUS ] ] MAIN == compteur : integer := 4; [ processus :: PROCESSUS ]