Najkratšia cesta, ASM
Program v ekvacionálnej schéme
P2 môze byt alokovaný do ASV s N2 procesormi tak, ze kazdý pocíta H[i, j, k] pre dané i, j
Program v read-only schéme (riešenie s jemnou atomicitou)
vyuzijeme nasledujúci vlastnost:
H[i, j, k +1] ? H[i, j, k]
ako dôsledok: môzeme pouzit H[i, j, k + m] namiesto H[i, j, k] pre m ? 0
Formulujme nasledujúci invariant:
d[i, j] = H[i, j, k]
? d[i, j] je dlzka nejakej cesty z i do j
? k ? N
v P4 je synchrónnost podstatná ? jedno k sa pouzíva pre výpocet kazdého d[i, j]. Teraz predpokladáme asynchrónne riešenie, v ktorom d[i, j] sa pocíta (i, j)-tym procesorom a k sa nahradí lokálnou premennou k[i, j]
zoslabením predošlého invariantu dostaneme invariant
d[i, j] ? H[i, j, k[i, j]]
? d[i, j] je dlzka nejakej cesty z i do j
? k[i, j] ? N