define N 20 PROCESSUS == [ i = 0 -> x : integer:= random(0,N); print (i + "? " + x + "\n"); processus[1]!couple(i,x) [] i /= 0 & i /= N -> x, j, k, val : integer; x := random(0,N); print (i + "? " + x + "\n"); k := i; *[ processus[i-1]?couple(j,val) -> [ x < val -> processus[i+1]!couple(k,x); x:=val; k:=j [] x >= val -> processus[i+1]!couple(j,val) ] ]; processus[i+1]!couple(k,x) [] i = N -> valeur, j : integer; *[ processus[N-1]?couple(j,valeur) -> print (j + ": " + valeur + "\n") ] ] MAIN == [ processus[i:0..N] :: PROCESSUS ]