Rozwiazanie zadania 2
A( i : 1 .. N ) :: gram : boolean; s : ( wolny, odpadl, koniec ); moja_liczba, jego_liczba, i : integer; z_kim : integer; gram := true; *[ gram -> z_kim := losuj; Sedzia ! chce_walczyc_z( z_kim ); Sedzia ? odp( s ); [ s = koniec -> gram := false [] s = odpadl -> skip [] s = wolny -> moja_liczba := losuj; [ (i:1..M) i = z_kim -> B(i) ! moja_liczba; B(i) ? jego_liczba; ] [ moja_liczba >= jego_liczba -> Sedzia ! pokonalem( z_kim ) [] moja_liczba < jego_liczba -> gram := false; ] ] ] || B( j : 1 .. N ) :: gram : boolean; moja_liczba, jego_liczba, i : integer; gram := true; *[(i:1..N) gram; A(i) ? jego_liczba -> moja_liczba := losuj; A(i) ! moja_liczba; [ moja_liczba > jego_liczba -> Sedzia ! pokonalem( i ) [] moja_liczba <= jego_liczba -> gram := false; ] ] || Sedzia :: ilu_B : integer; comment ilu jeszcze pozostalo w grze i, j, k : integer; stan_A : (1..N) integer; comment na kogo czeka proces A stan_B : (1..M) (wolny, walczy, odpadl); ilu_B := N; *[ (i:1..N) stan_A(i) <> 0 -> stan_A(i) := 0 ] comment na nikogo nie czeka *[ (i:1..M) stan_B(i) <> wolny -> stan_B(i) := wolny ] *[ (i:1..N) A(i) ? chce_walczyc_z( j ) -> [ stan_B(j) = wolny -> A(i) ! odp(wolny); stan_B(j) := walczy; [] stan_B(j) = odpadl -> [ ilu_B > 0 -> A(i) ! odp( odpadl ); [] ilu_B = 0 -> A(i) ! odp( koniec ); ] [] stan_B(j) = walczy -> stan_A(i) := j; ] [] (i:1..N) A(i) ? pokonalem(j) -> stan_B(j) := odpadl; ilu_B--; *[ (i:1..N) stan_A(i) = j -> A(i) ! odp( odpadl ); stan_A(i) := 0; ] [] (i:1..M) B(i) ? pokonalem(j) -> stan_A(j) := -1; comment odpadl stan_B(i) := wolny; *[ (k:1..N) stan_B(i) = wolny; stan_A(k) = i -> A(k) ! odp( wolny ); stan_A(k) := 0; stan_B(i) := walczy; ] ]
Istnieja rowniez rozwiazania bez wyroznionego centralnego procesu
Sedzia; znalezienie takowego rozwiazania pozostawiamy jednak Czytelnikowi...