Pr-1st-1.1-m10-Slajd50

Dowód warunku C2

Dowód warunku C2

Zgodnie z konstrukcją algorytmu, w każdym cyklu detekcyjnym odpowiedź REPLY jest wstrzymywana aż do momentu nadejścia potwierdzeń od monitorów procesów przeznaczenia, dla wszystkich wysłanych wcześniej wiadomości aplikacyjnych.

Wówczas $notAc{k}_i$, przyjmie wartość 0. Z drugiej strony można jednak zauważyć, że od chwili ${\tau }_i^k$ do ${\tau }_i^{k+1}$ proces $P_i$ jest ciągle pasywny, a więc nie wysyła wiadomości. Stąd więc wnosimy, że dla każdego procesu $P_i\in {𝒫}$, ${{ℐ}{𝒯}}_i[{\tau }^x]=\mathrm{\varnothing }$

<< Poprzedni slajd | Spis treści | Następny slajd >>