Pr-1st-1.1-m02-Slajd44

Predykat activate

Z kolei predykat $activate_{i}({\mathcal {X}})$ zdefiniowany jest w sposób następujący:

1. jeżeli ${\mathcal {X}}={\mathcal {D}}_{i}$, to $activate_{i}({\mathcal {X}})=True$
2. jeżeli ${\mathcal {X}}=\emptyset$, to $activate_{i}({\mathcal {X}})=False$
3. jeżeli ${\mathcal {X}}\subset {\mathcal {D}}_{i}$ i

${\mathcal {X}}\neq \emptyset$, to:

$activate_{i}({\mathcal {X}})\equiv \exists {\mathcal {X}}'::{\mathcal {X}}'\neq \emptyset \land {\mathcal {X}}'\subseteq {\mathcal {X}}\land ({\mathcal {P}}_{i}^{A}={\mathcal {X}}'\Rightarrow (passive_{i}\leftrightsquigarrow \neg passive_{i}))$

gdzie $passive_{i}\leftrightsquigarrow \neg passive_{i}$ oznacza, że pasywny proces $P_{i}$ zmieni swój stan na aktywny w skończonym choć nieprzewidywalnym czasie.

Predykat $activate_{i}({\mathcal {X}})$ 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 ${\mathcal {X}}'\subseteq {\mathcal {X}}$ (${\mathcal {P}}_{i}^{A}={\mathcal {X}}'$) gotowe stanie się którekolwiek z dopuszczalnych zdarzeń odbioru. Innymi słowy predykat $activate_{i}({\mathcal {X}})$ zachodzi, jeżeli dostarczenie wiadomości od wszystkich procesów $P_{j}\in {\mathcal {X}}$ umożliwia uaktywnienie procesu $P_{i}$Jak łatwo zauważyć, predykat ten posiada właściwość monotoniczności: jeżeli ${\mathcal {X}}\subseteq {\mathcal {Y}}$ i $activate_{i}({\mathcal {X}})=True$, to $activate_{i}({\mathcal {Y}})=True$.

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