Sr-3-wyk-2.0-Slajd7

From Studia Informatyczne

Predykaty (2)

Predykaty (2)


Predykat wysyła_w jest prawdziwy, gdy proces p wyśle wiadomość m w konkretnym obrazie V .

Predykat instaluje zostaje spełniony, gdy proces p zmieni obraz grupy na V .

Predykat instaluje_w oznacza zmianę obrazu z dotychczasowego V na nowy, V . Zmiana obrazu może być spowodowana dołączeniem lub odłączeniem pewnego zbioru procesów do- lub z grupy. Należy pamiętać, że odłączenie procesu modeluje jego faktyczne odłączenie po zakończeniu obliczeń albo awarię, wykrytą i zgłoszoną przez detektor uszkodzeń.

Ponieważ predykat instaluje_w uwzględnia poprzedni obraz grupy, jest szczególnie przydatny w tych własnościach, które uwzględniają historyczne obrazy w procesie (najczęściej tylko poprzedni); przykładem takiej własności jest wirtualna synchronizacja, omówiona w dalszej części.


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