6 Алгоритм Netchange. Разнообразие алгоритмов маршрутизации
Описание файла
PDF-файл из архива "6 Алгоритм Netchange. Разнообразие алгоритмов маршрутизации", который расположен в категории "". Всё это находится в предмете "распределенные алгоритмы" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
ÐàñïðåäåëåííûåàëãîðèòìûËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 5 (×àñòü 2).Àëãîðèòì ìàðøðóòèçàöèè Netchange.Îïèñàíèå àëãîðèòìà.Èíâàðèàíòû àëãîðèòìà Netchange.Êîððåêòíîñòü àëãîðèòìà Netchange.Ñõîäèìîñòü àëãîðèòìà Netchange.Îñîáåííîñòè ðåàëèçàöèè àëãîðèòìà.Äðóãèå âèäû ìàðøðóòèçàöèè:èíòåðâàëüíàÿ, ïðåôèêñíàÿ, èåðàðõè÷åñêàÿ.Àëãîðèòì ìàðøðóòèçàöèè NetchangeÀëãîðèòì Netchange, ïðåäëîæåííûéÒàäæèáíàïèñîì â 1977 ã, ñòðîèò îïòèìàëüíûå ïî÷èñëó çâåíüåâ òàáëèöû ìàðøðóòèçàöèè, à òàêæåñîáèðàåò äîïîëíèòåëüíóþ èíôîðìàöèþ, ÷òîáû âñëó÷àå âîçíèêíîâåíèÿ íåèñïðàâíîñòè â êàíàëå èëèâîññòàíîâëåíèÿ ðàáîòîñïîñîáíîñòè êàíàëàóòî÷íÿòü òàáëèöû ïóòåì èõïåðåâû÷èñëåíèÿ.÷àñòè÷íîãîÀëãîðèòì ìàðøðóòèçàöèè NetchangeÀëãîðèòì îïèðàåòñÿ íà ñëåäóþùèå äîïóùåíèÿ.N1. Êàæäûé óçåë îñâåäîìëåí î ðàçìåðå âñåé ñåòè(êîëè÷åñòâå óçëîâN).N2.
 êàíàëàõ ïîääåðæèâàåòñÿ î÷åðåäíîñòüñîîáùåíèé.N3. Óçëû ïîëó÷àþò óâåäîìëåíèÿ î âîçíèêíîâåíèèíåèñïðàâíîñòåé è âîññòàíîâëåíèèðàáîòîñïîñîáíîñòè ïðèìûêàþùèõ ê íèìêàíàëîâ.N4. Ñòîèìîñòü ïóòè ðàâíà ÷èñëó çâåíüåâ â ýòîìïóòè.Àëãîðèòì ìàðøðóòèçàöèè NetchangeÀëãîðèòì ìîæåò ñïðàâèòüñÿ ñ âîçíèêíîâåíèåìíåèñïðàâíîñòåé è âîññòàíîâëåíèåì ðàáîòîñïîñîáíîñòè êàíàëîâ, à òàêæå ñ äîáàâëåíèåìíîâûõ êàíàëîâ ñâÿçè, ïðè óñëîâèè, ÷òî âñÿêèéóçåë íåìåäëåííî óçíàåò î ïîâðåæäåíèè èëèâîññòàíîâëåíèè ïðèìûêàþùèõ ê íåìó êàíàëîâñâÿçè. êàæäîì óçëåuàëãîðèòì âû÷èñëÿåò èïîääåðæèâàåò òàáëèöóNbu [v ] , â êîòîðîé äëÿêàæäîé âåðøèíû-àäðåñàòà v óêàçûâàåòñÿ òîòñîñåä w = Nbu [v ] óçëà u , êîòîðîìó äîëæåí áûòüîòïðàâëåí ïàêåò, àäðåñîâàííûé âåðøèíå v .Àëãîðèòì ìàðøðóòèçàöèè NetchangeÒðåáîâàíèÿÊ àëãîðèòìó ïðåäúÿâëÿþòñÿ ñëåäóþùèå òðåáîâàíèÿ.R1.
Åñëè òîïîëîãèÿ ñåòè ïîñëå êîíå÷íîãî ÷èñëà èçìåíåíèéîñòàåòñÿ äàëåå íåèçìåííîé, òî àëãîðèòì çàâåðøàåò ðàáîòóïîñëå êîíå÷íîãî ÷èñëà øàãîâ.R2. Êîãäà àëãîðèòì çàâåðøàåò ðàáîòó, òàáëèöû Nbu [v ]óäîâëåòâîðÿþò ñëåäóþùèì óñëîâèÿì:a) åñëè v = u , òî Nbu [v ] = local ;b) åñëè ñóùåñòâóåò ïóòü èç âåðøèíû u â âåðøèíó v 6= u , òîNbu [v ] = w , ãäå w ýòî ïåðâàÿ âåðøèíà-ñîñåä óçëà u ,êîòîðûé ñëåäóåò çà u â êðàò÷àéøåì ïóòè èç u â v ;c) åñëè ïóòè èç âåðøèíû u â âåðøèíó v íåò, òî Nbu [v ] = udef.Îïèñàíèå àëãîðèòìà NetchangeÑòðóêòóðû äàííûõ àëãîðèòìàIIII ìíîæåñòâî âåðøèí, ñîñåäíèõ ñ óçëîì u ;Du öåëî÷èñëåííûé ìàññèâ ðàçìåðà 1 .
. . N ;ýëåìåíòû ìàññèâà Du [v ] îöåíêè ðàññòîÿíèÿ d(u, v )ìåæäó óçëàìè u è v ;Nbu ìàññèâ âåðøèí ðàçìåðà 1 . . . N ;ýëåìåíòû ìàññèâà Nbu [v ] èìåíà ñîñåäåé óçëà u ,êîòîðûì ïðåäïî÷òèòåëüíåå îòïðàâèòü ïàêåòû,àäðåñîâàííûå óçëó v ;ndisu äâóõìåðíûé öåëî÷èñëåííûé ìàññèâ ðàçìåðà1...N ;ýëåìåíòû ìàññèâà Du [w , v ] îöåíêè ðàññòîÿíèÿ d(w , v )ìåæäó óçëàìè w è v .NeighuÎïèñàíèå àëãîðèòìà NetchangeÑòðóêòóðû äàííûõ àëãîðèòìàÍà÷àëüíûå çíà÷åíèÿ ñòðóêòóð äàííûõ â êàæäîì óçëå u .IIIINeighu = {v :ñóùåñòâóåò êàíàë ñâÿçè ìåæäó óçëîì u è óçëîì v } ;Du [v ] = N äëÿ ëþáîãî óçëà v ;Nbu [v ] = udef äëÿ ëþáîãî óçëà v ;ndisu [v , w ] = N äëÿ ëþáîé ïàðû óçëîâ v , w .Îïèñàíèå àëãîðèòìà NetchangeÈíèöèàëèçàöèÿ óçëàbegin;u.;Du [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0isendto wendÍà÷èíàÿ ðàáîòó, êàæäûé óçåë u çíàåò ëèøü îäíî: êðàò÷àéøèéìàðøðóò èç u â u èìååò äëèíó 0 .È îí îïîâåùàåò îá ýòîì âñåõ ñâîèõ ñîñåäåé.Îïèñàíèå àëãîðèòìà NetchangeÏðîöåäóðà Update(v )begin ifv =uDu [v ] := 0 ; Nbu [v ] := local(* Îöåíèòü ðàññòîÿíèå äî âåðøèíû v *)d := 1 + min{ndisu [w , v ] : w ∈ Neighu } ;choose w : d = 1 + ndisu [u, v ];d <NDu [v ] := d ; Nbu [v ] := wDu [v ] := N ; Nbu [v ] := udefthen beginendelse beginifthen beginelse begin;ïåðåìåííàÿ Du [v ] èçìåíèëà çíà÷åíèåx ∈ Neighusend h, v , Du [v ]i to xendendifthenforalldomydistendÂû÷èñëåíèå îöåíîê Du [v ] ïðîâîäèòñÿ ñëåäóþùèì îáðàçîì.Åñëè u = v , òî d(u, v ) = 0 , è â ýòîì ñëó÷àå çíà÷åíèå Du [v ]ïîëàãàåòñÿ ðàâíûì 0 .endÎïèñàíèå àëãîðèòìà NetchangeÏðîöåäóðà Update(v )begin ifv =uthen beginelsebegin;(* Îöåíèòü ðàññòîÿíèå äî âåðøèíû v *)d := 1 + min{ndisu [w , v ] : w ∈ Neighu } ;choose w : d = 1 + ndisu [u, v ];d <NDu [v ] := d ; Nbu [v ] := wDu [v ] := N ; Nbu [v ] := udefDu [v ] := 0 Nbu [v ] := localifendthen beginelse begin;ïåðåìåííàÿ Du [v ] èçìåíèëà çíà÷åíèåx ∈ Neighusend h, v , Du [v ]i to xendendifthenforalldomydistendÅñëè u 6= v , òî êðàò÷àéøèé ïóòü èç u â v ñîñòîèò èç êàíàëà,ñîåäèíÿþùåãî u ñ îäíèì èç ñîñåäåé w , è êðàò÷àéøåãî ïóòè èçw âv .endÎïèñàíèå àëãîðèòìà NetchangeÏðîöåäóðà Update(v )begin ifv =uDu [v ] := 0 ; Nbu [v ] := local(* Îöåíèòü ðàññòîÿíèå äî âåðøèíû v *)d := 1 + min{ndisu [w , v ] : w ∈ Neighu } ;choose w : d = 1 + ndisu [u, v ];d <NDu [v ] := d ; Nbu [v ] := wDu [v ] := N ; Nbu [v ] := udefthen beginendelse beginifthen beginelse begin;ïåðåìåííàÿ Du [v ] èçìåíèëà çíà÷åíèåx ∈ Neighusend h, v , Du [v ]i to xendendifthenforalldomydistendÊîëü ñêîðî â ñåòè èìååòñÿ N óçëîâ, äëèíà ïóòè ñ íàèìåíüøèì÷èñëîì çâåíüåâ íå ïðåâîñõîäèò N − 1 .
 ïðîòèâíîì ñëó÷àåìîæíî ïðåäïîëàãàòü, ÷òî òàêîãî ïóòè âîîáùå íå ñóùåñòâóåò;èìåííî äëÿ ýòîé öåëè â òàáëèöå èñïîëüçóåòñÿ çíà÷åíèå N .endÎïèñàíèå àëãîðèòìà NetchangeÏðîöåäóðà Update(v )begin ifv =uDu [v ] := 0 ; Nbu [v ] := local(* Îöåíèòü ðàññòîÿíèå äî âåðøèíû v *)d := 1 + min{ndisu [w , v ] : w ∈ Neighu } ;choose w : d = 1 + ndisu [w , v ];d <NDu [v ] := d ; Nbu [v ] := wDu [v ] := N ; Nbu [v ] := udefthen beginendelse beginifthen beginelse begin;ïåðåìåííàÿ Du [v ] èçìåíèëà çíà÷åíèåx ∈ Neighusend h, v , Du [v ]i to xendendifthenforalldomydistendÅñëè îöåíêà ðàññòîÿíèÿ îò óçëà u äî óçëà v èçìåíèëàñü (ò.å.óìåíüøèëàñü), òî óçåë u îïîâåùàåò îá ýòîì âñåõ ñâîèõ ñîñåäåé,÷òîáû òå ìîãëè óòî÷íèòü ñâîì îöåíêè.endÎïèñàíèå àëãîðèòìà NetchangeProc-1 : Îáðàáîòêà ñîîáùåíèÿ h, v , di îò ñîñåäà w :{ Ñîîáùåíèå h, v , di â íà÷àëå î÷åðåäè Qwu }mydistmydistbeginreceive hfrom ;, v , diwndisu [w , v ] := d Update (v )mydist;endÏîñëå ïîëó÷åíèÿ ñîîáùåíèÿ h, v , di îò ñîñåäà w â óçëå uïåðåìåííîé ndisu [w , v ] ïðèñâàèâàåòñÿ çíà÷åíèå d .
Âðåçóëüòàòå èçìåíåíèÿ çíà÷åíèÿ ïåðåìåííîé ndisu [w , v ] îöåíêàd(u, v ) â óçëå u ìîæåò èçìåíèòüñÿ, è ïîýòîìó ýòà îöåíêàïåðåâû÷èñëÿåòñÿ âñÿêèé ðàç, êîãäà ïðîèñõîäÿò èçìåíåíèÿ âòàáëèöå ndisu . Åñëè îöåíêà ðàññòîÿíèÿ è â ñàìîì äåëåèçìåíÿåòñÿ, íàïðèìåð ñòàíîâèòñÿ ðàâíîé d 0 , òî îá ýòîìîïîâåùàþòñÿ âñå ñîñåäè ïðè ïîìîùè ñîîáùåíèé h, v , d 0 i.mydistmydistÎïèñàíèå àëãîðèòìà Netchange îòâåò íà âûõîä èç ñòðîÿ èëè âîññòàíîâëåíèåðàáîòîñïîñîáíîñòè êàíàëà ñâÿçè àëãîðèòì âíîñèòèçìåíåíèÿ â ëîêàëüíûå òàáëèöû è îòïðàâëÿåòñîîáùåíèå òèïàmydist, åñëè ïðè ýòîìèçìåíÿþòñÿ îöåíêè ðàññòîÿíèé.Ïðåäïîëàãàåòñÿ, ÷òî óâåäîìëåíèÿ î ïîëîìêàõ èïî÷èíêàõ êàíàëîâ ñâÿçè (äîïóùåíèå N3)ïîñòóïàþò â âèäå ñîîáùåíèé òèïàÊàíàë ñâÿçè ìåæäó óçëàìèïàðîé î÷åðåäåéQu1 u2èu1Qu2 u1.èu2fail è repair.ìîäåëèðóåòñÿÎïèñàíèå àëãîðèòìà NetchangeÊîãäà êàíàë âûõîäèò èç ñòðîÿ, ýòè î÷åðåäèóäàëÿþòñÿ èç êîíôèãóðàöèè (÷òî ïðèâîäèò êïîòåðå âñåõ ñîîáùåíèé â îáåèõ î÷åðåäÿõ), à óçëûïî îáå ñòîðîíû êàíàëà ñâÿçè ïîëó÷àþò ñîîáùåíèåòèïàfail.Êîãäà ñâÿçü â êàíàëå âîññòàíàâëèâàåòñÿ (èëè âñåòè ïîÿâëÿåòñÿ íîâûé êàíàë ñâÿçè), âêîíôèãóðàöèè âîçíèêàþò äâå íîâûå ïóñòûåî÷åðåäè, à óçëû ïî îáå ñòîðîíû ýòîãî êàíàëàrepair.
Ýòèñîîáùåíèÿ îáðàáàòûâàþòñÿ ñèíõðîííî â îáîèõñâÿçè ïîëó÷àþò ñîîáùåíèå òèïàóçëàõ.Îïèñàíèå àëãîðèòìà NetchangeProc-2 :  ñëó÷àå âûõîäà èç ñòðîÿ êàíàëà uw :beginreceive hforall;fail, w iNeighu := Neighu \ {w }v ∈ V do Update(v );endÊîãäà âûõîäèò èç ñòðîÿ êàíàë ñâÿçè ìåæäó óçëàìè u è w ,âåðøèíà w óäàëÿåòñÿ èç ñïèñêà Neighu .Ïðîâîäèòñÿ ïåðåâû÷èñëåíèå îöåíîê ðàññòîÿíèé äî êàæäîéâåðøèíû, è â ñëó÷àå èçìåíåíèÿ îöåíêè, îá ýòîì óçíàþò âñåîñòàâøèåñÿ ñîñåäè.Ýòî ïðîèñõîäèò, åñëè íåèñïðàâíûé êàíàë ðàíåå áûë îäíèì èççâåíüåâ íàèëó÷øåãî ìàðøðóòà è íå îñòàëîñü íè îäíîãî ñîñåäàw 0 , äëÿ êîòîðîãî âåðíî ðàâåíñòâî ndisu [w 0 , v ] = ndisu [w , v ].Îïèñàíèå àëãîðèòìà NetchangeProc-3 :  ñëó÷àå âîññòàíîâëåíèÿ êàíàëà uw :beginreceive hforallv ∈Vbegin;, w i Neighu := Neighu ∪ {w }repairdondisu [w ,v ] := N; send hmydist;, v , Du [v ]ito wendendÊîãäà êàíàë ñâÿçè âîññòàíàâëèâàåòñÿ, âåðøèíà w äîáàâëÿåòñÿê ñïèñêó âåðøèí Neighu , íî â ïàìÿòè óçëà u åùå íåò íèêàêèõîöåíîê ðàññòîÿíèÿ d(w , v ) .Íîâîìó ñîñåäó w íåìåäëåííî ñîîáùàþòñÿ îöåíêè Du [v ]ðàññòîÿíèé îò óçëà u äî âñåõ âîçìîæíûõ âåðøèí-àäðåñàòîâ v(ïóòåì îòïðàâëåíèÿ ñîîáùåíèé h, v , Du [v ]i.Äî òåõ ïîð ïîêà óçåë u íå ïîëó÷èò òàêîãî ñîîáùåíèÿ îò óçëà w, âåëè÷èíà N áóäåò èñïîëüçîâàòüñÿ â íåì äëÿ îöåíêèðàññòîÿíèÿ d(w , v ) , ò.
å. çíà÷åíèå ïåðåìåííîé ndisu [w , v ]ïîëàãàåòñÿ ðàâíûì N .mydistÎïèñàíèå àëãîðèòìà NetchangeÂû÷èñëåíèå àëãîðèòìà çàâåðøàåòñÿ, êîãäà â êàíàëàõ ñâÿçè íåîñòàåòñÿ ñîîáùåíèé, íàõîäÿùèõñÿ íà ýòàïå ïåðåñûëêè.Íî äëÿ âñåé ñèñòåìû â öåëîì òàêèå êîíôèãóðàöèè íå ÿâëÿþòñÿçàêëþ÷èòåëüíûìè, ïîòîìó ÷òî âû÷èñëåíèå ñèñòåìû ìîæåòáûòü ïðîäîëæåíî, ïîñëå òîãî êàê êàêîé-íèáóäü êàíàë âûéäåò èçñòðîÿ èëè âîññòàíîâèò ñâîþ ðàáîòîñïîñîáíîñòü (÷òî ïîòðåáóåòðåàêöèè ñî ñòîðîíû àëãîðèòìà).Êîíôèãóðàöèþ, íå èìåþùóþ â êàíàëàõ ñâÿçè íè îäíîãîñîîáùåíèÿ, ìû áóäåì íàçûâàòü ñòàáèëüíîé .
Äëÿ îïèñàíèÿýòîãî ÿâëåíèÿ ââåäåì äâà ïðåäèêàòà:up(u, w ) ≡ êàíàë ñâÿçè ìåæäó óçëàìè u, w èñïðàâåístable ≡ ∀ u, w : up(u, w ) ⇒ Qwuíå ñîäåðæèò ñîîáùåíèémydist.Èíâàðèàíòû àëãîðèòìà Netchange×òîáû îáîñíîâàòü êîððåêòíîñòü àëãîðèòìà Netchangeîòíîñèòåëüíî òðåáîâàíèé R1 è R2 íàì ïîíàäîáÿòñÿÈÍÂÀÐÈÀÍÒÛ.P(u, w , v ) ≡up(u, w ) ⇐⇒ w ∈ Neighu∧up(u, w ) ∧ Qwu=⇒∧(1)ñîäåðæèò ñîîáùåíèå h, v , diïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v ]mydistíå ñîäåðæèò ñîîáùåíèé hup(u, w )∧Qwu=⇒ ndisu [w , v ] = Dw [v ]mydist,v ,diÔîðìóëà P(u, w , v ) óòâåðæäàåò: åñëè ïðîöåññ u çàâåðøèëîáðàáîòêó ñîîáùåíèé òèïà, ïîëó÷åííûõ îò ïðîöåññà w ,òî îöåíêà ðàññòîÿíèÿ d(w , v ) â óçëå u ñîâïàäàåò ñ îöåíêîéðàññòîÿíèÿ d(w , v ) â óçëå w .mydist(2)(3)Èíâàðèàíòû àëãîðèòìà NetchangeËåììà 1.Äëÿ ëþáîé òðîéêè âåðøèí u0, w0, v0 ôîðìóëà P(u0, w0, v0)ÿâëÿåòñÿ èíâàðèàíòîì.Äîêàçàòåëüñòâî.Áóäåì ñ÷èòàòü, ÷òî âíà÷àëå âñå ñïèñêè Neighu ïðàâèëüíîîòðàæàþò ðàáîòîñïîñîáíîñòü êàíàëîâ ñâÿçè ìåæäó óçëàìè, ò.
å.ñîîòíîøåíèå (1) ñ÷èòàåòñÿ âåðíûì.Íóæíî ðàññìîòðåòü èíèöèàëèçàöèþ è òðè òèïà ïðîöåäóð:1. Proc-1 : ïðèåì ñîîáùåíèÿ òèïà. Ïðîèñõîäèò ïðèåìîäíîãî ñîîáùåíèÿ è (âîçìîæíî) îòïðàâëåíèå íåñêîëüêèõñîîáùåíèé.2. Proc-2 : îáðûâ êàíàëà è îáðàáîòêà ñîîáùåíèÿ òèïà âóçëàõ ïî îáå ñòîðîíû êàíàëà.3. Proc-3 : âîññòàíîâëåíèå êàíàëà è îáðàáîòêà ñîîáùåíèÿòèïàâ îáîèõ óçëàõ, ñîåäèíåííûõ ýòèì êàíàëîì.mydistfailrepairbegin;;Du [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0isendto wendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist(1), v0 , di(2)0mydist0 0=⇒ndisu0 [w0 ,v0 ] = Dw0 [v0 ],v0 ,di(3) ñàìîì íà÷àëå ïîñëå âûïîëíåíèÿ ïðîöåäóðû èíèöèàëèçàöèè âêàæäîì óçëå ñîîòíîøåíèå (1) âûïîëíÿåòñÿ ñîãëàñíîñäåëàííîìó äîïóùåíèþ î ñïèñêàõ Neighu .begin;;Du [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0isendto wendw0 ) ⇐⇒ w0 ∈ Neighu0up(u0 , w0 ) ∧ Qw0 u0=⇒up(u0 ,ñîäåðæèò ñîîáùåíèå hïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hmydist(1), v0 , di(2)0mydist0 0=⇒ndisu0 [w0 ,v0 ] = Dw0 [v0 ],v0 ,diÅñëè ïåðâîíà÷àëüíî âûïîëíÿåòñÿ óñëîâèå ¬up(u0, w0) , òîñîîòíîøåíèÿ (2) è (3), î÷åâèäíî, âûïîëíÿþòñÿ.(3)begin;;Du [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0isendto wendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist(1), v0 , di(2)0mydist0 0=⇒ndisu0 [w0 ,v0 ] = Dw0 [v0 ],v0 ,di(3)Åñëè æå âíà÷àëå âûïîëíÿåòñÿ óñëîâèå up(u0, w0) , òîñîãëàñíî (1), è ïîýòîìó ïîñëå èíèöèàëèçàöèè.w0 ∈ Neighu0ndisu0 [w0 , v0 ] = Nbegin;;Du [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0isendto wendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist(1), v0 , di(2)0mydist0 0=⇒ ndisu0 [w0 , v0 ] = Dw0 [v0 ]w0 = v0Dw0 [w0 ] = 0hmydist, v0 , 0iÅñëè, òîñîäåðæèòñÿ ñîîáùåíèåñîîòíîøåíèÿ (2) è (3).,v0 ,di(3), íî ïðè ýòîì â î÷åðåäè Qw u, è ïîýòîìó âåðíû0 0begin;;Du [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0isendto wendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist(1), v0 , di(2)00 0=⇒ ndisu0 [w0 , v0 ] = Dw0 [v0 ]w0 6= v0Dw0 [v0 ] = Nv0mydist,v0 ,di(3)Åñëè, òîè â î÷åðåäè êàíàëà (w0u0) íåòñîîáùåíèé îá óçëå , ïîýòîìó ñîîòíîøåíèÿ (2) è (3) òàêæåáóäóò âåðíû.Proc-1 : Îáðàáîòêà ñîîáùåíèÿ h, v , di îò ñîñåäà w :{ Ñîîáùåíèå h, v , di â íà÷àëå î÷åðåäè Qwu }receive h, v , di from w ;ndisu [w , v ] := d ; Update (v )mydistmydistbeginmydistendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0(1)mydist, v0 , di(2)0mydist0 0=⇒ndisu) [w0 ,v0 ] = Dw0 [v0 ]u,v0 ,di(3)hmydist, v , diÏðåäïîëîæèì, ÷òî óçåë ïîëó÷àåò ñîîáùåíèåîòóçëà w .Ýòî íå âëå÷åò çà ñîáîé íèêàêèõ èçìåíåíèé òîïîëîãèè ñåòè, èïîýòîìó ñïèñêè âåðøèí-ñîñåäåé Neigh íå èçìåíÿþòñÿ, èñîîòíîøåíèå (1) îñòàåòñÿ âåðíûì.Åñëè v 6= v0 , òî ñ ïîëó÷åíèåì ýòîãî ñîîáùåíèÿ â ôîðìóëåP(u0 , w0 , v0 ) íè÷åãî íå èçìåíÿåòñÿ.Proc-1 : Îáðàáîòêà ñîîáùåíèÿ h, v , di îò ñîñåäà w :{ Ñîîáùåíèå h, v , di â íà÷àëå î÷åðåäè Qwu }receive h, v , di from w ;ndisu [w , v ] := d ; Update (v )mydistmydistbeginmydistendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0(1)ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist, v0 , di(2)00 0=⇒ ndisu0 [w0 , v0 ] = Dw0 [v0 ]v = v0 , u = u0 , w = w0mydist,v0 ,di(3)Åñëè, òî çíà÷åíèå ndisu [w0, v0] ìîæåòèçìåíèòüñÿ.Åñëè Qw u ñîäåðæèò åùå îäíî ñîîáùåíèå îá óçëå v0 , òîçíà÷åíèÿ, ñîäåðæàùèåñÿ â ýòîì ñîîáùåíèè, óäîâëåòâîðÿþò (2).Cîîòíîøåíèÿ (3) ñîõðàíÿåòñÿ, ò.ê.