Vecerajúci filozofi: Spec4
Formálny popis: Spec4: nech clean[u, v]: boolean
clean[u, v] = true ? vidlicka od u a v je clean, inak je dirty
prior[u, v] = u ? ((fork[u, v] = u) = clean[u, v])
Spec4: (odn1), (odn2), (odn7), (odn8), (odn10)?(odn13), kde
- invariant u.e ? E[u, v] ?
fork[u, v] = u ? ?clean[u, v] (odn10)
- fork[u, v] = v ? clean[u, v] unless v.e (odn11)
- fork[u, v] = u ? ?clean[u, v] unless
fork[u, v] = v ? clean[u, v] (odn12)
- fork[u, v] = u ? clean[u, v] ? u.h (odn13)
cize
- namiesto (odn5), (odn9) máme (odn10)
- namiesto (odn6) máme (odn11), (odn12)
Motivácia pre zlepšenie: Spec4 evokuje nasledovné riešenie:
- non-eating proces u pošle vidlicku hladnému (hungry) susedovi v, ak je [táto vidlicka] dirty
- hungry proces u je (eats), ak drzí ? odpovedajúce vidlicky a ak pre kazdého suseda v spolocná vidlicka je clean alebo v je thinking; ak proces je (eats), zašpiní všetky vidlicky
Problém: ako môze proces u zistit, ci sused v je hladný?