Pr-1st-1.1-m10-Slajd63

Dowód twierdzenia 10.4 (1)

Dowód

Cykl detekcyjny nie jest wstrzymywany przez monitory, awięc inicjator otrzyma odpowiedź od każdego $Q_{i}$ w skończonym czasie.

Zakładamy, że przetwarzanie aplikacyjne osiągnęło stan zakończenia dynamicznego w chwili $\tau ^{t}$ ($Dterm({\mathcal {P}})[\tau ^{t}]=True$). Od tego momentu zatem, wszystkie procesy pozostają ciągle pasywne:

$passive_{i}[\tau ^{x}]$ i $activate_{i}({\mathcal {AV_{i}}}\cup {\mathcal {IT}}_{i})[\tau ^{x}]=False$ , dla każdego $\tau ^{x}\geq \tau ^{x}$.

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