Pr-1st-1.1-m10-Slajd51

Dowód warunku C3 (1)

Dowód warunku C3

Z konstrukcji algorytmu wynika, że w każdym cyklu detekcyjnym odpowiedź jest opóźniana do momentu uzyskania przez predykat $\neg activate({\mathcal {AV}}_{i})$ wartości True . Skoro algorytm kończy się w chwili $\tau _{i}^{k+1}$, to predykat $activate({\mathcal {AV}}_{i})[\tau _{'}i^{k+1}]$ miał wartość False . Ponieważ w przedziale $\left\langle \tau _{i}^{k},\tau _{i}^{k+1}\right\rangle$ proces $P_{i}$ był przez cały czas pasywny, żadna wiadomość nie została w tym czasie odebrana.

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