Pr-1st-1.1-m10-Slajd64

Dowód twierdzenia 10.4 (2)

Tak więc każdy cykl zainicjowany po ${\tau }^t$, powiedzmy cykl k, nada wszystkim zmiennym $contPassiv{e}_i$ wartość True, i odbierze od monitorów $Q_i$ wektor końcowych wartości liczników $vSentN{o}_i$. Dlatego, w chwili ${\tau }_b^{k+1}$ rozpoczęcia kolejnego cyklu detekcyjnego, wysłane zostaną ostateczne wartości liczników wiadomości wysłanych, a stąd ${{𝒜}{ℐ}{𝒯}}_i[{\tau }_i^{k+1}]={{ℐ}{𝒯}}_i[{\tau }_i^{k+1}]$. W efekcie otrzymujemy, że:

$activat{e}_i({{𝒜}{𝒱}}_i\cup {{𝒜}{ℐ}{𝒯}}_i)[{\tau }_i^{k+1}]=activat{e}_i({{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i)[{\tau }_i^{k+1}]$

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