buffer: (0..9) portion; in, out: integer; in := 0; out := 0; * [ in < out + 10; producer?buffer(in mod 10) --> in := in + 1; [] out < in; consumer?more() --> consumer!buffer(out mod 10); out := out + 1; ]