Vecerajúci filozofi: Spec2
prior[u, v] = u, ak u je vyššie nez v v grafe G’ (t.j. u ? v)
prior[v, u] = prior[u, v]
u.top ? ??v: E[u, v] ? v.h:: prior[u, v] = v?
Spec2: (odn1)?(odn3), (odn5)?(odn8), kde
- invariant u.e ? E[u, v] ? prior[u, v] = v (odn5)
- (prior[u, v] = v) unless v.e (odn6)
- inariant G’ je acyklický (odn7)
- (dn1, dn3?dn5), (odn5)?(odn7), ??u:: u.e ? ?u.e? /
/ ??u :: u.h ? u.top ? ?(u.h ? u.top)? (odn8)
co znamená:
- eating má nizšiu prioritu nez susedia (odn5)
- priorita sa mení, az ked zacne jest (odn6)