Pr-1st-1.1-m07-Slajd21

Modele stanów globalnych – przykład 1 (2)

Po wysłaniu znacznika $toke{n}_1$ będącego konkretną wiadomością typu TOKEN (każda wiadomość, a więc również każdy znacznik, ma swój unikalny identyfikator mId ) w kierunku procesu $P_2$, znacznik przez pewien czas znajduje się w kanale $C_{1,2}$ (przypomnijmy, że w ogólności czas przebywania wiadomości w kanale jest skończony, lecz nie znany a priori ). Tak więc w chwili $\tau 1$ stan globalny można opisać następująco:

$\mathrm{\Sigma }({\tau }_1)=$	$⟨⟨presen{t}_1({\tau }_1)=False$	$outLo{g}_1({\tau }_1)=\{toke{n}_1\}$	$inLo{g}_1({\tau }_1)=\mathrm{\varnothing }⟩$
	$⟨presen{t}_2({\tau }_1)=False$	$outLo{g}_2({\tau }_1)=\mathrm{\varnothing }$	$inLo{g}_2({\tau }_1)=\mathrm{\varnothing }⟩$
	$⟨presen{t}_3({\tau }_1)=False$	$outLo{g}_3({\tau }_1)=\mathrm{\varnothing }$	$inLo{g}_3({\tau }_1)=\mathrm{\varnothing }⟩⟩$

Zauważmy, że znajomość stanów lokalnych procesów $P_1$ oraz $P_2$ w chwili ${\tau }_1$ pozwala łatwo wyznaczyć stan kanału $C_{1,2}$ jako różnicę mnogościową $outLo{g}_1({\tau }_1)$ oraz $inLo{g}_2(\tau 1)$.

Po odebraniu znacznika $toke{n}_1$ przez proces $P_2$ system osiąga stan ${\mathrm{\Sigma }}^2$:

$\mathrm{\Sigma }({\tau }_2)=$	$⟨⟨presen{t}_1({\tau }_2)=False$	$outLo{g}_1({\tau }_2)=\{toke{n}_1\}$	$inLo{g}_1({\tau }_2)=\mathrm{\varnothing }⟩$
	$⟨presen{t}_2({\tau }_2)=True$	$outLo{g}_2({\tau }_2)=\mathrm{\varnothing }$	$inLo{g}_2({\tau }_2)=\{toke{n}_1\}⟩$
	$⟨presen{t}_3({\tau }_2)=False$	$outLo{g}_3({\tau }_2)=\mathrm{\varnothing }$	$inLo{g}_3({\tau }_2)=\mathrm{\varnothing }⟩⟩$

Jak widać, w chwili ${\tau }_2$ kanał jest już pusty i istotnie $outLo{g}_1({\tau }_2)\setminus inLo{g}_2({\tau }_2)=\mathrm{\varnothing }$.

Po wysłaniu przez $P_2$ znacznika do procesu $P_3$ osiągany jest kolejny stan, $\mathrm{\Sigma }({\tau }_3)$:

$\mathrm{\Sigma }({\tau }_3)=$	$⟨⟨presen{t}_1({\tau }_3)=False$	$outLo{g}_1({\tau }_3)=\{toke{n}_1\}$	$inLo{g}_1({\tau }_3)=\mathrm{\varnothing }⟩$
	$⟨presen{t}_2({\tau }_3)=False$	$outLo{g}_2({\tau }_3)=\{toke{n}_2\}$	$inLo{g}_2({\tau }_3)=\{toke{n}_1\}⟩$
	$⟨presen{t}_3({\tau }_3)=False$	$outLo{g}_3({\tau }_3)=\mathrm{\varnothing }$	$inLo{g}_3({\tau }_3)=\mathrm{\varnothing }⟩⟩$

Następnie znacznik jest odbierany przez $P_3$ i osiągany jest kolejny stan, a potem w analogiczny sposób następne.

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