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({𝒫})[{\tau }^t]=True$). Od tego momentu zatem, wszystkie procesy pozostają ciągle pasywne:

$passiv{e}_i[{\tau }^x]$ i $activat{e}_i({𝒜}{{V}}_{{𝒾}}\cup {{ℐ}{𝒯}}_i)[{\tau }^x]=False$ , dla każdego ${\tau }^x\ge {\tau }^x$.

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