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\le {\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 >>