Pr-1st-1.1-m10-Slajd40

Algorytm detekcji zakończenia statycznego (3)

W celu stwierdzenia zakończenia statycznego przetwarzania aplikacyjnego określonego przez predykat

$Sterm({𝒫})\equiv \mathrm{\forall }{P}_i::P_i\in \in {𝒫}::(passiv{e}_i\wedge ({{ℐ}{𝒯}}_i\ne \mathrm{\varnothing })\mathrm{\neg }activat{e}_i({{𝒜}{𝒱}}_i))$

inicjator $Q_{\alpha }$ rozpoczyna detekcję przez wysłanie do wszystkich monitorów, w tym do siebie, wiadomości kontrolnej typu QUERY.

Po otrzymaniu wszystkich odpowiedzi, inicjator wyznacza iloczyn logiczny otrzymanych zmiennych contPassive jako wartość zmiennej $sTermDetecte{d}_{\alpha }$.

• Jeżeli $sTermDetecte{d}_{\alpha }$ przyjmuje wartość True, to $Q_{\alpha }$ stwierdza zakończenie
• W przeciwnym przypadku inicjator wysyła ponownie zapytanie QUERY

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