Sr-3-wyk-1.0-Slajd6

Predykaty (1)

Powyższe predykaty budowane są na podstawie elementarnych zdarzeń, przedstawionych wcześniej.

Predykat obraz_w_chwili definiuje obraz, jaki w procesie p istnieje w chwili zajścia zdarzenia ti.

Predykat odbiera zachodzi, gdy proces p odbierze wiadomość m w dowolnej chwili. Predykat odbiera_w określa dodatkowo, w jakim obrazie proces p odbiera wiadomość m .

Predykat wysyła jest prawdą, jeśli proces p wysłał wiadomość m w dowolnej chwili.

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