Pr-1st-1.1-m10-Slajd68

Dowód warunku C5 (1)

Dowód warunku C5

Z konstrukcji algorytmu wynika, że algorytm ten zakończy się w chwili ${\tau }_e^{k+1}$ pod warunkiem, że predykat $activat{e}_i({{𝒜}{𝒱}}_i\cup {{𝒜}{ℐ}{𝒯}}_i)$ miał wartość False w chwili ${\tau }_e^{k+1}$ dla każdego $i\in \{1,2,...,n\}$.Ponieważ każdy proces był pasywny w przedziale $⟨{\tau }_i^k,{\tau }_i^{k+1}⟩$, dla każdego zachodzi:

C6. ${{𝒜}{𝒱}}_i[{\tau }^x]\subseteq {{𝒜}{𝒱}}_i[{\tau }_i^{k+1}]$

oraz $vSentN{o}_i[j][{\tau }_i^k]=vSentN{o}_i[j][{\tau }^x]$

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