Sr-3-wyk-1.0-Slajd7
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.
