Pr-1st-1.1-m10-Slajd65

Dowód twierdzenia 10.4 (3)

Ponieważ ten ostatni predykat ma wartość False od chwili $\tau ^{t}$, a $\tau ^{t}\leq \tau _{i}^{k}<\tau _{i}^{k+1}$, więc w cyklu k+1 wszystkie zmienne $replyIn.contPassive$ będą miały wartość True, i w efekcie algorytm detekcji dynamicznego zakończenia przetwarzania aplikacyjnego zakończy się.

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