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 $\mathrm{\neg }activate({{𝒜}{𝒱}}_i)$ wartości True . Skoro algorytm kończy się w chwili ${\tau }_i^{k+1}$, to predykat $activate({{𝒜}{𝒱}}_i)[{\tau }_{\text{'}}{i}^{k+1}]$ miał wartość False . Ponieważ w przedziale $⟨{\tau }_i^k,{\tau }_i^{k+1}⟩$ 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 >>