Oto dwa przykladowe rozwiazania:
Sedzia( i: 0..N-1 ) :: [ i = 0 -> skip; [] i <> 0 -> Sedzia(i-1 mod N) ? token(); ] *[ Kolarz(i) ? start() -> Sedzia(i+1 mod N) ! token(); [ Sedzia(i-1 mod N) ? token() -> Kolarz(i) ? meta(); [] Kolarz(i) ? meta() -> Sedzia(i-1 mod N) ? token(); ] ]
Sedzia( i: 0..N-1 ) :: [ i = N-1 -> Sedzia(0) ? token(); [] i <> N-1 -> skip; ] *[ true -> Sedzia( i-1 mod N ) ! token(); Kolarz(i) ? start(); [ Sedzia(i+1 mod N) ? token() -> Kolarz(i) ? meta(); [] Kolarz(i) ? meta() -> Sedzia(i+1 mod N) ? token(); ] ]
Jedyna trudnosc w tym zadaniu polegala na takim zaprojektowaniu komunikacji miedzy procesami Sedzia(i), aby nie ograniczala ona DOWOLNOSCI kolejnosci konczenia wyscigow przez kolarzy.
Typowy blad popelnili autorzy takiego rozwiazania:
Sedzia( i: 0..N-1 ) :: [ i = N-1 -> Sedzia(0) ! token(); [] i <> N-1 -> skip; ] *[ Sedzia( i-1 mod N ) ? token() -> Kolarz(i) ? start(); (*) Sedzia(i+1 mod N) ! token(); (**) Kolarz(i) ? meta(); (***) ]
Rozpatrzmy np. sytuacje, gdy proces Sedzia(N-1) jest po wykonaniu instrukcji (*), a wszyscy pozostali sedziowie po wykonaniu instrukcji (**), co oznacza, m. in., ze wszyscy kolarze rozpoczeli (kolejno) jazde, a zaden dotychczas nie zakonczyl. Kolarz(N-1) nie moze zakonczyc jazdy zanim nie zakonczy Kolarz(0), ze wzgledu na komunikacje procesu Sedzia(N-1) w (**), do ktorej Sedzia(0) nie jest gotowy.
Blad ten kosztowal 4.5 pkt...