3 Коммуникационные протоколы. Ошибки, возникающие при передаче сообщений. Задача надежного обмена сообщениями

ÐàñïðåäåëåííûåàëãîðèòìûËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 3.Êîììóíèêàöèîííûå ïðîòîêîëû.Îøèáêè, âîçíèêàþùèå ïðè ïåðåäà÷å ñîîáùåíèé.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà.Óñòðîéñòâî ïðîòîêîëà ðàçäâèæíîãî îêíà.Ïðèíöèïû îáîñíîâàíèÿ êîððåêòíîñòè ïðîòîêîëîâÎáîñíîâàíèå êîððåêòíîñòè ïðîòîêîëà ðàçäâèæíîãî îêíà.Ìîäèôèêàöèè ïðîòîêîëà.Êîììóíèêàöèîííûå ïðîòîêîëûÎñíîâíîå íàçíà÷åíèå êîììóíèêàöèîííîãî ïðîòîêîëà ïåðåäà÷à äàííûõ , ò.å. ïîëó÷åíèå èíôîðìàöèè îò îäíîãî óçëàñåòè è äîñòàâêà åå ïî íàçíà÷åíèþ äðóãîìó óçëó ñåòè.Ïðè ïåðåäà÷å äàííûõ âîçìîæíû îøèáêè (ïîòåðÿ,äóáëèðîâàíèå, èñêàæåíèå).Ýòè îøèáêè íóæíî îáíàðóæèâàòü è èñïðàâëÿòü.Äëÿ ýòîãî â ïðîòîêîëå âåäåòñÿ ó÷åò ñîñòîÿíèÿ èíôîðìàöèè.Äëÿ èñïîëüçîâàíèÿ ñîñòîÿíèÿ èíôîðìàöèè ïðèìåíÿåòñÿóïðàâëåíèå ñîåäèíåíèåì èíèöèàëèçàöèÿ è àííóëèðîâàíèåñîñòîÿíèÿ èíôîðìàöèè.Èíèöèàëèçàöèÿ íàçûâàåòñÿ óñòàíîâëåíèåì ñîåäèíåíèÿ, ààííóëèðîâàíèå çàâåðøåíèåì ñîåäèíåíèÿ.Êîììóíèêàöèîííûå ïðîòîêîëûÌû ðàññìîòðèì îäèí èç òàêèõ ïðîòîêîëîâ (Balanced Sliding WindowProtocol).Îí ïðåäíàçíà÷åí äëÿ îáìåíà äàííûìè ìåæäó äâóìÿ óçëàìèñåòè, êîòîðûå èìåþò ïðÿìîå ôèçè÷åñêîå ñîåäèíåíèå(íàïðèìåð, ïî îïòîâîëîêîííîìó êàáåëþ).Ýòî âïîëíå àñèíõðîííûé ïðîòîêîë, îòíîñÿùèéñÿ ê óðîâíþóïðàâëåíèÿ ïåðåäà÷åé äàííûõ âòîðîìó óðîâíþ ýòàëîííîéìîäåëè OSI.Ìû íå áóäåì ðàññìàòðèâàòü óïðàâëåíèå ñîåäèíåíèåì äëÿ ýòîãîïðîòîêîëà.

Ïðåäïîëàãàåòñÿ, ÷òî ôèçè÷åñêîå ñîåäèíåíèå îáû÷íîôóíêöèîíèðóåò íåïðåðûâíî â òå÷åíèå î÷åíü äîëãîãî âðåìåíè, àíå óñòàíàâëèâàåòñÿ è çàâåðøàåòñÿ ïåðèîäè÷åñêè.ñèììåòðè÷íûéïðîòîêîë ðàçäâèæíîãî îêíàÎøèáêè, âîçíèêàþùèå ïðè ïåðåäà÷åñîîáùåíèéÏðè ôèçè÷åñêîì ñîåäèíåíèè ñîîáùåíèÿ íå ìîãóò îáãîíÿòü äðóãäðóãà, è îíè òàêæå íå ìîãóò äóáëèðîâàòüñÿ. Ïîýòîìóðàññìàòðèâàþòñÿ òîëüêî îøèáêè ïîòåðè ñîîáùåíèÿ.Ñîäåðæàíèå ñîîáùåíèÿ, ïåðåäàâàåìîãî ïî ôèçè÷åñêîìó êàíàëóñâÿçè, ìîæåò áûòü ïîâðåæäåíî.

Òåì íå ìåíåå ìîæíîïðåäïîëàãàòü, ÷òî ïðîöåññ-ïîëó÷àòåëü ñïîñîáåí îáíàðóæèâàòüèñêàæåíèÿ ñîîáùåíèé, íàïðèìåð, ïðè ïîìîùè ñ÷åò÷èêîâ÷åòíîñòè èëè êîäèðîâàíèÿ ñ èñïðàâëåíèåì îøèáîê (êîäûÕýììèíãà, Ðèäà-Ìàëëåðà è äð.).Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÏîñòàíîâêà çàäà÷è.inpABCD..YZp?inq à á â . . þ ÿ. . . . . . . . . Q.

p. . . . . . . . . . . .. . . . . . . . . . Q. q. . . . . . . . . . -.?outpoutq?q?Ïðîöåññàì p è q òðåáóåòñÿ ïåðåäàòü ïîòîêè äàííûõ inp è inqäðóã äðóãó è çàïèñàòü ïîëó÷åííûå äàííûå â ìàññèâû outp è outq . êàíàëå ñâÿçè âîçìîæíû ïîìåõè, ïðèâîäÿùèå ê ïîòåðå ñîîáùåíèé.Îáùàÿ èäåÿ àëãîðèòìàIIÂõîäíûå äàííûå îäíîãî ïðîöåññà ñëóæàò äëÿïîäòâåðæäåíèÿ ïîëó÷åíèÿ ñîîáùåíèé îò äðóãîãî ïðîöåññà.Ñîîáùåíèÿ ýòî íàáîðû âèäà h , w , ii, ãäåw ,àiïàêåòà.Ïàêåò h , w , ii, îòïðàâëåííûé ïðîöåññîì p , ïåðåäàåòñëîâî w = inp [i] ïðîöåññó q è ïîäòâåðæäàåò óñïåøíîåïîëó÷åíèå ðÿäà ïàêåòîâ, îòïðàâëåííûõ ïðîöåññîì q .Ïðîöåññ p ìîæåò ¾îïåðåæàòü¿ ïðîöåññ q íà íåêîòîðîåçàäàííîå ÷èñëî ïàêåòîâ `p , åñëè ìû ïîñòàíîâèì, ÷òîîòïðàâëåíèå ïàêåòà h , w , ii ïðîöåññîì p ïîäòâåðæäàåòïîëó÷åíèå ñëîâ ñ íîìåðàìè 0, 1, .

. . , (i − `p ) îò ïðîöåññà q .Êîíñòàíòû îïåðåæåíèÿ `p è `q èçâåñòíû ïðîöåññàì p è q .ïàêåòûèíôîðìàöèîííîå ñëîâîIIpackpackIpackïîðÿäêîâûé íîìåðÎáùàÿ èäåÿ àëãîðèòìàÒàêèì îáðàçîì, â ïðîòîêîëå ñîáëþäàþòñÿ äâà ïðèíöèïà:1. Ïðîöåññ p ìîæåò îòïðàâèòü ñëîâî inp [i] (â ïàêåòåh, inp [i], ii) òîëüêî ïîñëå òîãî, êàê áóäóò çàíåñåíû âïàìÿòü âñå ñëîâà, íà÷èíàÿ ñ outp [0] è îêàí÷èâàÿoutp [i − `p ] , ò.å. êîãäà áóäåò âûïîëíÿòüñÿ íåðàâåíñòâîi < sp + `p , ãäå sp = min{j : outp [j] = udef } .2.

Êàê òîëüêî p ïîëó÷àåò ïàêåò h , w , ii, îòïàäàåòíåîáõîäèìîñòü â ïîâòîðíîé ïåðåäà÷å ñëîâ, íà÷èíàÿ ñ inp [0]è îêàí÷èâàÿ inp [i − `q ] .packpackÑèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàvarSpsp , apinpoutp:: array of word: array of word: { ap ≤ i < sp + `p }Rp: {hinitinitbegin}send hpackreceive(*endelse}, w , ii ∈ QpQp := Qp \ hpack, w , iipackbeginto qend;èãíîðèðîâàòü ïîâòîðíîå ïîëó÷åíèå ïàêåòà *)end: {h, inp [i], ii;;Lp0, 0, w , ii ∈ Qphpack, w , iiif outp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }packbegin;(* Data to be sent *) ;udef , udef , .

. . ;integer{}endÑèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà1. Äåéñòâèå p îñóùåñòâëÿåò îòïðàâëåíèå i -ãî âõîäíîãîñëîâà ïðîöåññà p ,S2. ÄåéñòâèåRpîñóùåñòâëÿåò ïðèåì ñëîâà ïðîöåññîì p ,3. Äåéñòâèå p ìîäåëèðóåò ïîòåðþ ïàêåòà, àäðåñàòîìêîòîðîãî ÿâëÿåòñÿ ïðîöåññ p .LÑèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàvarSpsp , apinpoutp:: array of word: array of word: { ap ≤ i < sp + `p }Rp: {hinitinitbegin}send hpackreceive(*endelse}, w , ii ∈ QpQp := Qp \ hpack, w , iipackbeginto qend;èãíîðèðîâàòü ïîâòîðíîå ïîëó÷åíèå ïàêåòà *)end: {h, inp [i], ii;;Lp0, 0, w , ii ∈ Qphpack, w , iiif outp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }packbegin;(* Data to be sent *) ;udef , udef , . .

. ;integer{}endÑèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà: { ap ≤ i < sp + `p }send h , inp [i], ii to qÄàííûå äëÿ îòïðàâëåíèÿ âûáèðàþòñÿ èç ðàçäâèæíîãî îêíàSpbeginpackendap ≤ i < sp + `pÏðåäïîëàãàåòñÿ, ÷òîËåâàÿ ñòâîðêà : ap = min{i : outp [i + `q ] = udef } íàèìåíüøèé íîìåð òîãî ýëåìåíòà â ìàññèâå inp ,ïîëó÷åíèå êîòîðîãî åùå íå ïîäòâåðäèë ïðîöåññ q .Çíà÷èò, inp [ap ] åùå íóæíî îòïðàâëÿòü.Ïðàâàÿ ñòâîðêà : sp + `p − 1 , ãäå sp = min{j : outp [j] = udef } íàèìåíüøèé íîìåð òîãî ýëåìåíòà â ìàññèâå outp ,â êîòîðûé åùå íå çàïèñàíû ïîëó÷åííûå äàííûå.Çíà÷èò, inp [sp + `p ] åùå ðàíî îòïðàâëÿòü âêà÷åñòâå ïîäòâåðæäåíèÿ î ïîëó÷åíèè äàííûõ.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàRp:{hbegin}, w , ii ∈ Qphpack, w , iiif outp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }packreceive;;(*endelse;èãíîðèðîâàòü ïîâòîðíîå ïîëó÷åíèå ïàêåòà *)endÏîëó÷èâ ñîîáùåíèå, ïðîöåññ âíà÷àëå ïðîâåðÿåò, íå áûëî ëèèäåíòè÷íîå ñîîáùåíèå ïîëó÷åíî ðàíåå (â ýòîì ñëó÷àå ïðîöåññèìååò äåëî ñ ïîâòîðíûì ïîëó÷åíèåì ñîîáùåíèÿ).Åñëè ýòî íå òàê, òî ñëîâî, ñîäåðæàùååñÿ â ñîîáùåíèè,çàïèñûâàåòñÿ â âûõîäíîé ìàññèâ, è ïðè ýòîì çíà÷åíèÿïåðåìåííûõ ap è sp èçìåíÿþòñÿ.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàRp:{hbegin}, w , ii ∈ Qphpack, w , iiif outp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }packreceive;;(*endelse;èãíîðèðîâàòü ïîâòîðíîå ïîëó÷åíèå ïàêåòà *)endÏîëó÷èâ ñîîáùåíèå, ïðîöåññ âíà÷àëå ïðîâåðÿåò, íå áûëî ëèèäåíòè÷íîå ñîîáùåíèå ïîëó÷åíî ðàíåå (â ýòîì ñëó÷àå ïðîöåññèìååò äåëî ñ ïîâòîðíûì ïîëó÷åíèåì ñîîáùåíèÿ).Åñëè ýòî íå òàê, òî ñëîâî, ñîäåðæàùååñÿ â ñîîáùåíèè,çàïèñûâàåòñÿ â âûõîäíîé ìàññèâ, è ïðè ýòîì çíà÷åíèÿïåðåìåííûõ ap è sp èçìåíÿþòñÿ.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàRp:{hbegin}, w , ii ∈ Qphpack, w , iiif outp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }packreceive;;(*endelse;èãíîðèðîâàòü ïîâòîðíîå ïîëó÷åíèå ïàêåòà *)endÏîëó÷èâ ñîîáùåíèå, ïðîöåññ âíà÷àëå ïðîâåðÿåò, íå áûëî ëèèäåíòè÷íîå ñîîáùåíèå ïîëó÷åíî ðàíåå (â ýòîì ñëó÷àå ïðîöåññèìååò äåëî ñ ïîâòîðíûì ïîëó÷åíèåì ñîîáùåíèÿ).Åñëè ýòî íå òàê, òî ñëîâî, ñîäåðæàùååñÿ â ñîîáùåíèè,çàïèñûâàåòñÿ â âûõîäíîé ìàññèâ, è ïðè ýòîì çíà÷åíèÿïåðåìåííûõ ap è sp èçìåíÿþòñÿ.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàLp:{h}, w , ii ∈ QpQp := Qp \ hpack, w , iipackbegin{}endÌîäåëèðîâàíèå ïîòåðè ñîîáùåíèÿ ïðîâîäèòñÿ ïóòåì óäàëåíèÿïðîèçâîëüíîãî ñîîáùåíèÿ èç ìíîæåñòâà ñîîáùåíèé Qp ,ïðåáûâàþùèõ íà ýòàïå ïåðåñûëêè îò ïðîöåññà q ê ïðîöåññó p .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà×òî ïëîõîãî ìîæåò ñëó÷èòüñÿ?1.

Ñòâîðêè îêîí îáîèõ ïðîöåññîâ ìîãóò ¾çàõëîïíóòüñÿ¿, èïðîöåññû áóäóò îáðå÷åíû (áåçóñïåøíî) îæèäàòüñîîáùåíèé äðóã îò äðóãà (áëîêèðîâêà , deadlock );2. Ñòâîðêè îêîí ìîãóò ¾çàñòûòü¿, è ïðîöåññû áóäóòîáðå÷åíû ïåðåäàâàòü îäíè è òå æå ñîîáùåíèÿ (àêòèâíûéòóïèê , livelock );3. Äàííûå ìîãóò áûòü ïîòåðÿíû ïðè ïåðåäà÷å, è ïðîöåññ íåçàìåòèò ýòîãî;4. Ïðîöåññ ìîæåò ¾çàáûòü¿ ïåðåäàòü äàííûå;5. Ñòâîðêè îêíà ìîãóò ðàçäâèãàòüñÿ, îòäàëàÿÿñü äðóã îòäðóãà íåîãðàíè÷åííî øèðîêî.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÒðåáîâàíèÿ êîððåêòíîñòè.Íóæíî äîêàçàòü, ÷òî ïðîòîêîë ðàáîòàåò ïðàâèëüíî, ò.å. êàæäîåñëîâî èç âõîäíîãî ìàññèâà inp ïðîöåññà p áóäåò ðàíî èëèïîçäíî çàïèñàíî â âûõîäíîé ìàññèâ outq ïðîöåññà q , èíàîáîðîò.Áîëåå ñòðîãî ýòî âûðàæàåòñÿ äâóìÿ òðåáîâàíèÿìè.1. êàæäîé äîñòèæèìîéêîíôèãóðàöèè ïðîòîêîëà âûïîëíÿþòñÿ ñîîòíîøåíèÿoutp [0..sp −1] = inq [0..sp −1] è outq [0..sq −1] = inp [0..sq −1].2.Äëÿ êàæäîãî öåëîãî÷èñëà k ≥ 0 , â õîäå âûïîëíåíèÿ ïðîòîêîëà áóäåòäîñòèãíóòà êîíôèãóðàöèÿ, â êîòîðîé sp ≥ k è sq ≥ k .Áåçîïàñíàÿ äîñòàâêà ñîîáùåíèé.Íåèçáåæíàÿ äîñòàâêà ñîîáùåíèé.À êàê äîêàçûâàåòñÿêîððåêòíîñòüïðîòîêîëîâ?Êàê îáîñíîâûâàòü ñâîéñòâà ñèñòåì ïåðåõîäîâÊëàññèôèêàöèÿ ñâîéñòâÌíîãèå ñâîéñòâà ðàñïðåäåëåííûõ àëãîðèòìîâ, íóæäàþùèåñÿ âïðîâåðêå, îòíîñÿòñÿ ê îäíîìó èç äâóõ òèïîâ:è.Óñëîâèå áåçîïàñíîñòè òðåáóåò, ÷òîáû êàæäàÿ äîñòèæèìàÿêîíôèãóðàöèÿ â ëþáîì âûïîëíåíèè ñèñòåìû îáëàäàëàîïðåäåëåííûì ñâîéñòâîì.Óñëîâèå æèâîñòè òðåáóåò, ÷òîáû õîòÿ áû îäíà äîñòèæèìàÿêîíôèãóðàöèÿ â ëþáîì âûïîëíåíèè ñèñòåìû îáëàäàëàîïðåäåëåííûì ñâîéñòâîì.óñëîâèå áåçîïàñíîñòèóñëîâèå æèâîñòèÑâîéñòâà áåçîïàñíîñòèÑâîéñòâîì áåçîïàñíîñòè àëãîðèòìà ÿâëÿåòñÿ âñÿêîå ñâîéñòâî,êîòîðîå ìîæíî ñôîðìóëèðîâàòü â âèäå ñëåäóþùåãîïðåäëîæåíèÿ:¾Äëÿ ëþáîãî âûïîëíåíèÿ àëãîðèòìà óòâåðæäåíèå P èñòèííî âêàæäîé êîíôèãóðàöèè âûïîëíåíèÿ¿.Áîëåå êðàòêî ýòî ñâîéñòâî ìîæíî ñôîðìóëèðîâàòü òàê:¾Óòâåðæäåíèå P âñåãäà èñòèííî¿.Îñíîâíîé ïðèåì, ïðè ïîìîùè êîòîðîãî óäàåòñÿ ïîêàçàòü, ÷òîóòâåðæäåíèå P âñåãäà èñòèííî, çàêëþ÷àåòñÿ â äîêàçàòåëüñòâåòîãî, ÷òî P ÿâëÿåòñÿ.èíâàðèàíòîìÑâîéñòâà áåçîïàñíîñòèÏóñòü çàäàíà ñèñòåìà ïåðåõîäîâ S = (C, →, I) èðàññìàòðèâàþòñÿ íåêîòðûå ñâîéñòâà êîíôèãóðàöèé P è Q .Çàïèñü P(γ) , ãäå γ êîíôèãóðàöèÿ, áóäåò îáîçíà÷àòüëîãè÷åñêîå âûðàæåíèå (ôîðìóëó), ïðèíèìàþùåå èñòèííîåçíà÷åíèå â òîì ñëó÷àå, åñëè óòâåðæäåíèå P ñïðàâåäëèâî äëÿêîíôèãóðàöèè γ , è ëîæíîå çíà÷åíèå â ïðîòèâíîì ñëó÷àå.Çàïèñü {P} → {Q} áóäåò èñïîëüçîâàòüñÿ äëÿ îáîçíà÷åíèÿòîãî, ÷òî äëÿ êàæäîãî ïåðåõîäà γ → δ â ñèñòåìå S èñòèííîñòüP(γ) âëå÷åò èñòèííîñòü Q(δ) .Îïðåäåëåíèå 3.1.Óòâåðæäåíèå P íàçûâàåòñÿñèñòåìû S , åñëè1.

P(γ) èñòèííî äëÿ êàæäîé íà÷àëüíîé êîíôèãóðàöèè γ ∈ I ,è2. {P} → {P} .èíâàðèàíòîìÑâîéñòâà áåçîïàñíîñòèÒåîðåìà 3.1.Åñëè óòâåðæäåíèå P ÿâëÿåòñÿ èíâàðèàíòîì ñèñòåìû ïåðåõîäîâS , òî äëÿ ëþáîãî âûïîëíåíèÿ E ñèñòåìû S óòâåðæäåíèå Páóäåò èñòèííî â êàæäîé êîíôèãóðàöèè ýòîãî âûïîëíåíèÿ.Ðàññìîòðåòü ïðîèçâîëüíîå âûïîëíåíèåE = (γ0 , γ1 , γ2 , . . .) ñèñòåìû S è âîñïîëüçîâàòüñÿ èíäóêöèåé.Äîêàçàòåëüñòâî:Òåîðåìà 3.2.Åñëè Q ÿâëÿåòñÿ èíâàðèàíòîì ñèñòåìû ïåðåõîäîâ S , è äëÿêàæäîé êîíôèãóðàöèè γ ∈ C âûïîëíÿåòñÿ Q(γ) =⇒ P(γ) , òîäëÿ ëþáîãî âûïîëíåíèÿ ñèñòåìû S óòâåðæäåíèå P áóäåòèñòèííî â êàæäîé êîíôèãóðàöèè âûïîëíåíèÿ.Ñâîéñòâà áåçîïàñíîñòèÇàäà÷è.1. Âåðíî ëè, ÷òî óòâåðæäåíèå, êîòîðîå ÿâëÿåòñÿ èñòèííûì âêàæäîé êîíôèãóðàöèè ëþáîãî âûïîëíåíèÿ, îáÿçàòåëüíîÿâëÿåòñÿ èíâàðèàíòîì?2.

Ïðèâåäèòå ïðèìåð òàêîé ñèñòåìû ïåðåõîäîâ S è òàêîãîóòâåðæäåíèÿ P , ÷òî P âñåãäà èñòèííî â ñèñòåìå S , íî ïðèýòîì íå ÿâëÿåòñÿ èíâàðèàíòîì S .3. Ïðåäïîëîæèì, ÷òî P1 è P2 ýòî èíâàðèàíòû ñèñòåìû S .Äîêàæèòå, ÷òî (P1 ∨ P2) è (P1 ∧ P2) òàêæå ÿâëÿþòñÿèíâàðèàíòàìè.Ñâîéñòâà æèâîñòèÑâîéñòâîì æèâîñòè àëãîðèòìà ÿâëÿåòñÿ âñÿêîå ñâîéñòâî,êîòîðîå ìîæíî ñôîðìóëèðîâàòü â âèäå ñëåäóþùåãîïðåäëîæåíèÿ:¾Äëÿ ëþáîãî âûïîëíåíèÿ àëãîðèòìà óòâåðæäåíèå P èñòèííî âíåêîòîðîé êîíôèãóðàöèè âûïîëíåíèÿ¿.Áîëåå êðàòêî ýòî ñâîéñòâî ìîæíî ñôîðìóëèðîâàòü òàê:¾Óòâåðæäåíèå P êîãäà-òî îáÿçàòåëüíî ñòàíîâèòñÿ èñòèííûì¿.Îñíîâíîé ïðèåì, ïðè ïîìîùè êîòîðîãî óäàåòñÿ ïîêàçàòü, ÷òîóòâåðæäåíèå P êîãäà-òî îáÿçàòåëüíî ñòàíîâèòñÿ èñòèííûì,çàêëþ÷àåòñÿ â èñïîëüçîâàíèèè.ôóíêöèé íîðìèðîâêèîòñóòñòâèÿ áëîêèðîâêèÑâîéñòâà æèâîñòèÐàññìîòðèì ñèñòåìó ïåðåõîäîâ S è ïðåäèêàò P .