Pr-1st-1.1-m10-Slajd44

Algorytm detekcji zakończenia statycznego: Dowód poprawności – oznaczenia (1)

Twierdzenie o poprawności przedstawionego algorytmu używać będzie następujących oznaczeń:

${\tau }_i^k$ - czas globalny wysłania odpowiedzi przez monitor $Q_i$ w k-tym cyklu detekcji.

${\tau }_b^k$ - czas globalny rozpoczęcia k-tego cyklu detekcji

${\tau }_e^k$ - czas globalny zakończenia k-tego cyklu detekcji

Zachodzi:

${\tau }_b^k<{\tau }_i^k<{\tau }_e^k$

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