predicate round_robin(array[int] of var bool: nbhs) =
      let { int: N = length(nbhs);
            var -1..N-1: select; % Neighbourhood selection
      } in  if status()=START then select= -1
            else select= (lastval(select) + 1) mod N
            endif /\
            forall(i in 1..N) (select=i-1 -> nbhs[i]);@\Vlabel{line:6:roundrobin:post}@