Pr-1st-1.1-m10-Slajd49

Dowód warunku C1

Dowód warunku C1

Z konstrukcji algorytmu wynika, że zakończy się on w chwili ${\tau }_e^{k+1}$ z $sTerminationDetected[{\tau }_e^{k+1}]=True$, tylko wówczas, gdy każdy proces $P_i$ był pasywny w czasie między ${\tau }_i^j$ a ${\tau }_i^{k+1}$. Skoro jednak ${\tau }_i^k\le {\tau }^x\le {\tau }_i^{k+1}$, więc możemy zatem wnosić, że dla każdego $P_i\in {𝒫}$, $passiv{e}_i[{\tau }^x]=True$.

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