Vecerajúci filozofi: Spec3
Motivácia: zo Spec2 by sme mohli odvodit program s jednoduchým pravidlom:
- hungry proces u zacne jest, ak u.top a ak ziaden jeho sused neje. Ak zacne jest, tak prior[u, v] sa stane v pre všetkých susedov vrcholu u.
Toto je ale nevhodné pre distribuovanú architektúru: hungry totiz musí najprv zistit, ci susedia nejedia
Dalšie zjemnenie: Spec3: jeho úlohou je nahradit (odn3), teda invariant ?(u.e ? v.e ? E[u, v]), vlastnostou, ktorá sa dá implementovat v distribuovanej architektúre.
Zavedieme novú premennú fork[u, v], ktorá môze mat hodnotu u alebo v; znacka, ktorú má len jeden zo susediacich vrcholov
proces môze jest, ak má všetky znacky
Spec3: (odn1), (odn2), (odn5) ? (odn9), kde
- invariant u.e ? E[u, v] ? fork[u, v] = u (odn9)
teda (odn9) nahradilo (odn3)
Dôkaz, ze (odn9) ? (odn3):
u.e ? v.e ? E[u, v] ? u = v ? E[u, v]
ale ?(u = v ? E[u, v]) kedze ?E[u, u], a teda