Vecerajúci filozofi: Spec2
Problém s implementovaním Spec1:
- hladný je (eats), ak nejedia susedia ? splna to (odn3)
- problém je zabezpecit (odn4), pretoze jeden proces môze stále opakovat t ? h ? e ? t ? h ? e ? …
Riešenie:
- zavedieme asymetriu medzi procesmi ? usporiadanie
- hladný bud zacne jest alebo postúpi v usporiadaní nahor, az kým nie je navrchu
- ciastocné usporiadanie dostaneme tak, ze v pôvodnom grafe G orientujeme hrany (aby nevznikol cyklus), cím dostaneme nový graf G’
u ? v iff u je vyššie ako v
- orientácia je dynamická a chceme, aby platilo:
(a) G’ je acyklický
(b) hladný proces nikdy neklesne zmenami orientácií
(c) hladný nakoniec vzdy stúpa v usporiadaní, az dosiahne vrchol
Pravidlá pre zmenu orientácie G’:
1. Hrana zmení orientáciu len ked odpovedajúci vrchol zmení stav z hladný na eating
2. ? hrany incidentné s eating smerujú k nemu ? teda tento vrchol je nizšie v usporiadaní nez susedia
Lahko vidno, ze pravidlá 1. a 2. zabezpecia platnost (a), (b), (c).