Pr-1st-1.1-m07-Slajd21: Różnice pomiędzy wersjami

Aktualna wersja na dzień 22:15, 11 wrz 2023

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

Po wysłaniu znacznika $t o k e 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 $τ 1$ stan globalny można opisać następująco:

$Σ (τ_{1}) =$	$⟨ ⟨ p r e s e n t_{1} (τ_{1}) = F a l s e$	$o u t L o g_{1} (τ_{1}) = {t o k e n_{1}}$	$i n L o g_{1} (τ_{1}) = \emptyset ⟩$
	$⟨ p r e s e n t_{2} (τ_{1}) = F a l s e$	$o u t L o g_{2} (τ_{1}) = \emptyset$	$i n L o g_{2} (τ_{1}) = \emptyset ⟩$
	$⟨ p r e s e n t_{3} (τ_{1}) = F a l s e$	$o u t L o g_{3} (τ_{1}) = \emptyset$	$i n L o g_{3} (τ_{1}) = \emptyset ⟩ ⟩$

Zauważmy, że znajomość stanów lokalnych procesów $P_{1}$ oraz $P_{2}$ w chwili $τ_{1}$ pozwala łatwo wyznaczyć stan kanału $C_{1, 2}$ jako różnicę mnogościową $o u t L o g_{1} (τ_{1})$ oraz $i n L o g_{2} (τ 1)$ .

Po odebraniu znacznika $t o k e n_{1}$ przez proces $P_{2}$ system osiąga stan $Σ^{2}$ :

$Σ (τ_{2}) =$	$⟨ ⟨ p r e s e n t_{1} (τ_{2}) = F a l s e$	$o u t L o g_{1} (τ_{2}) = {t o k e n_{1}}$	$i n L o g_{1} (τ_{2}) = \emptyset ⟩$
	$⟨ p r e s e n t_{2} (τ_{2}) = T r u e$	$o u t L o g_{2} (τ_{2}) = \emptyset$	$i n L o g_{2} (τ_{2}) = {t o k e n_{1}} ⟩$
	$⟨ p r e s e n t_{3} (τ_{2}) = F a l s e$	$o u t L o g_{3} (τ_{2}) = \emptyset$	$i n L o g_{3} (τ_{2}) = \emptyset ⟩ ⟩$

Jak widać, w chwili $τ_{2}$ kanał jest już pusty i istotnie $o u t L o g_{1} (τ_{2}) ∖ i n L o g_{2} (τ_{2}) = \emptyset$ .

Po wysłaniu przez $P_{2}$ znacznika do procesu $P_{3}$ osiągany jest kolejny stan, $Σ (τ_{3})$ :

$Σ (τ_{3}) =$	$⟨ ⟨ p r e s e n t_{1} (τ_{3}) = F a l s e$	$o u t L o g_{1} (τ_{3}) = {t o k e n_{1}}$	$i n L o g_{1} (τ_{3}) = \emptyset ⟩$
	$⟨ p r e s e n t_{2} (τ_{3}) = F a l s e$	$o u t L o g_{2} (τ_{3}) = {t o k e n_{2}}$	$i n L o g_{2} (τ_{3}) = {t o k e n_{1}} ⟩$
	$⟨ p r e s e n t_{3} (τ_{3}) = F a l s e$	$o u t L o g_{3} (τ_{3}) = \emptyset$	$i n L o g_{3} (τ_{3}) = \emptyset ⟩ ⟩$

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 >>

@@ Linia 6: / Linia 6: @@
 {|
-|<math> \mathit\Sigma(\tau _1) = </math>
+|<math>\mathit\Sigma(\tau _1) =</math>
-|<math> \langle  \langle present_1(\tau _1) = False </math>
+|<math>\langle  \langle present_1(\tau _1) = False</math>
-|<math> outLog_1 (\tau _1) = \{token_1\} </math>
+|<math>outLog_1 (\tau _1) = \{token_1\}</math>
-|<math> inLog_1(\tau _1) = \emptyset \rangle </math>
+|<math>inLog_1(\tau _1) = \emptyset \rangle</math>
 |-
 |
-|<math> \langle present_2(\tau _1) = False </math>
+|<math>\langle present_2(\tau _1) = False</math>
-|<math> outLog_2(\tau _1) = \emptyset </math>
+|<math>outLog_2(\tau _1) = \emptyset</math>
-|<math> inLog_2(\tau _1) = \emptyset \rangle </math>
+|<math>inLog_2(\tau _1) = \emptyset \rangle</math>
 |-
 |
-|<math> \langle present_3 (\tau _1) = False </math>
+|<math>\langle present_3 (\tau _1) = False</math>
-|<math> outLog_3 (\tau _1) = \emptyset </math>
+|<math>outLog_3 (\tau _1) = \emptyset</math>
-|<math> inLog_3(\tau _1) = \emptyset \rangle \rangle </math>
+|<math>inLog_3(\tau _1) = \emptyset \rangle \rangle</math>
 |}
@@ Linia 31: / Linia 31: @@
 {|
-|<math> \mathit\Sigma(\tau _2) = </math>
+|<math>\mathit\Sigma(\tau _2) =</math>
-|<math> \langle \langle present_1(\tau _2) = False </math>
+|<math>\langle \langle present_1(\tau _2) = False</math>
-|<math> outLog_1 (\tau _2) = \{token_1\} </math>
+|<math>outLog_1 (\tau _2) = \{token_1\}</math>
-|<math> inLog_1(\tau _2) = \emptyset \rangle </math>
+|<math>inLog_1(\tau _2) = \emptyset \rangle</math>
 |-
 |
-|<math> \langle present_2(\tau _2) = True </math>
+|<math>\langle present_2(\tau _2) = True</math>
-|<math> outLog_2(\tau _2) = \emptyset </math>
+|<math>outLog_2(\tau _2) = \emptyset</math>
-|<math> inLog_2(\tau _2) = \{ token_1 \} \rangle </math>
+|<math>inLog_2(\tau _2) = \{ token_1 \} \rangle</math>
 |-
 |
-|<math> \langle present_3 (\tau _2) = False </math>
+|<math>\langle present_3 (\tau _2) = False</math>
-|<math> outLog_3 (\tau _2) = \emptyset </math>
+|<math>outLog_3 (\tau _2) = \emptyset</math>
-|<math> inLog_3(\tau _2) = \emptyset \rangle \rangle </math>
+|<math>inLog_3(\tau _2) = \emptyset \rangle \rangle</math>
 |}
-Jak widać, w chwili <math>\tau _2</math> kanał jest już pusty i istotnie <math>outLog_1(\tau _2) \setminus inLog_2(\tau _2) = \emptyset </math>.
+Jak widać, w chwili <math>\tau _2</math> kanał jest już pusty i istotnie <math>outLog_1(\tau _2) \setminus inLog_2(\tau _2) = \emptyset</math>.
 Po wysłaniu przez <math>P_2</math> znacznika do procesu <math>P_3</math> osiągany jest kolejny stan, <math>\mathit\Sigma (\tau _3)</math>:
 {|
-|<math> \mathit\Sigma(\tau _3) = </math>
+|<math>\mathit\Sigma(\tau _3) =</math>
-|<math> \langle \langle present_1(\tau _3) = False </math>
+|<math>\langle \langle present_1(\tau _3) = False</math>
-|<math> outLog_1 (\tau _3) = \{token_1\} </math>
+|<math>outLog_1 (\tau _3) = \{token_1\}</math>
-|<math> inLog_1(\tau _3) = \emptyset \rangle </math>
+|<math>inLog_1(\tau _3) = \emptyset \rangle</math>
 |-
 |
-|<math> \langle present_2(\tau _3) = False </math>
+|<math>\langle present_2(\tau _3) = False</math>
-|<math> outLog_2(\tau _3) = \{ token_2 \} </math>
+|<math>outLog_2(\tau _3) = \{ token_2 \}</math>
-|<math> inLog_2(\tau _3) = \{ token_1 \} \rangle </math>
+|<math>inLog_2(\tau _3) = \{ token_1 \} \rangle</math>
 |-
 |
-|<math> \langle present_3 (\tau _3) = False </math>
+|<math>\langle present_3 (\tau _3) = False</math>
-|<math> outLog_3 (\tau _3) = \emptyset </math>
+|<math>outLog_3 (\tau _3) = \emptyset</math>
-|<math> inLog_3(\tau _3) = \emptyset \rangle \rangle </math>
+|<math>inLog_3(\tau _3) = \emptyset \rangle \rangle</math>
 |}

Pr-1st-1.1-m07-Slajd21: Różnice pomiędzy wersjami

Aktualna wersja na dzień 22:15, 11 wrz 2023

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

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia