Pr-1st-1.1-m02-Slajd44: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 8: | Linia 8: | ||
# jeżeli <math>\mathcal{X} \subset \mathcal{D}_i</math> i | # jeżeli <math>\mathcal{X} \subset \mathcal{D}_i</math> i | ||
<math>\mathcal{X} \ne \emptyset</math>, to: | <math>\mathcal{X} \ne \emptyset</math>, to: | ||
:<math>activate_i(\mathcal{X}) \equiv \exists\mathcal{X}' :: \mathcal{X}' \ne \emptyset \land \mathcal{X}' \subseteq \mathcal{X} \land (\mathcal{P}_i^A = \mathcal{X}' \Rightarrow ( passive_i \leftrightsquigarrow \neg passive_i ))</math> | :<math>activate_i(\mathcal{X}) \equiv \exists\mathcal{X}' :: \mathcal{X}' \ne \emptyset \land \mathcal{X}' \subseteq \mathcal{X} \land (\mathcal{P}_i^A = \mathcal{X}' \Rightarrow ( passive_i | ||
gdzie <math>passive_i \leftrightsquigarrow \neg passive_i</math> oznacza, że pasywny proces <math>P_i</math> zmieni swój stan na aktywny w skończonym choć nieprzewidywalnym czasie. | \leftrightsquigarrow \neg passive_i ))</math> | ||
gdzie <math>passive_i \leftrightsquigarrow \neg passive_i</math> | |||
oznacza, że pasywny proces <math>P_i</math> zmieni swój stan na aktywny w skończonym choć nieprzewidywalnym czasie. | |||
Predykat <math>activate_i(\mathcal{X})</math> zachodzi zatem wtedy i tylko wtedy, gdy w związku z nadejściem (dostępnością) wiadomości od procesów tworzących zbiór <math>\mathcal{X}' \subseteq \mathcal{X} </math> (<math>\mathcal{P}_i^A = \mathcal{X}'</math>) gotowe stanie się którekolwiek z dopuszczalnych zdarzeń odbioru. Innymi słowy predykat <math>activate_i(\mathcal{X})</math> zachodzi, jeżeli dostarczenie wiadomości od wszystkich procesów <math>P_j \in \mathcal{X}</math> umożliwia uaktywnienie procesu <math>P_i</math>Jak łatwo zauważyć, predykat ten posiada właściwość monotoniczności: jeżeli | Predykat <math>activate_i(\mathcal{X})</math> zachodzi zatem wtedy i tylko wtedy, gdy w związku z nadejściem (dostępnością) wiadomości od procesów tworzących zbiór <math>\mathcal{X}' \subseteq \mathcal{X} </math> (<math>\mathcal{P}_i^A = \mathcal{X}'</math>) gotowe stanie się którekolwiek z dopuszczalnych zdarzeń odbioru. Innymi słowy predykat <math>activate_i(\mathcal{X})</math> zachodzi, jeżeli dostarczenie wiadomości od wszystkich procesów <math>P_j \in \mathcal{X}</math> umożliwia uaktywnienie procesu <math>P_i</math>Jak łatwo zauważyć, predykat ten posiada właściwość monotoniczności: jeżeli | ||
Wersja z 15:49, 7 wrz 2006
Predykat activate
Z kolei predykat zdefiniowany jest w sposób następujący:
- jeżeli , to
- jeżeli , to
- jeżeli i
, to:
gdzie oznacza, że pasywny proces zmieni swój stan na aktywny w skończonym choć nieprzewidywalnym czasie.
Predykat zachodzi zatem wtedy i tylko wtedy, gdy w związku z nadejściem (dostępnością) wiadomości od procesów tworzących zbiór () gotowe stanie się którekolwiek z dopuszczalnych zdarzeń odbioru. Innymi słowy predykat zachodzi, jeżeli dostarczenie wiadomości od wszystkich procesów umożliwia uaktywnienie procesu Jak łatwo zauważyć, predykat ten posiada właściwość monotoniczności: jeżeli i , to .
