Pr-1st-1.1-m07-Slajd21: Różnice pomiędzy wersjami
Nie podano opisu zmian |
m Zastępowanie tekstu – „ </math>” na „</math>” |
||
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>: | 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> | ||
|} | |} | ||
Wersja z 10:45, 5 wrz 2023
Modele stanów globalnych – przykład 1 (2)
Po wysłaniu znacznika 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 , znacznik przez pewien czas znajduje się w kanale (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 stan globalny można opisać następująco:
Zauważmy, że znajomość stanów lokalnych procesów oraz w chwili pozwala łatwo wyznaczyć stan kanału jako różnicę mnogościową oraz .
Po odebraniu znacznika przez proces system osiąga stan :
Jak widać, w chwili kanał jest już pusty i istotnie .
Po wysłaniu przez znacznika do procesu osiągany jest kolejny stan, :
Następnie znacznik jest odbierany przez i osiągany jest kolejny stan, a potem w analogiczny sposób następne.