Vecerajúci filozofi: Spec5
Formálne: Spec5
- pre kazdú dvojicu susedov zavedieme rt[u, v] s hodnotami u a v (práve jedna z nich)
- skratka u.me znací „u may eat“ (u môze jest)
- podmienka, za ktorej u posiela request-token procesu v, je oznacená sendreq[u, v]
- podmienka, za ktorej u posiela fork procesu v, je oznacená sendfork[u, v]
u má request-token iff rt[u, v] = u
u.me ? ??v: E[u, v]::
(fork[u, v] = u ? (clean[u, v] ? rt[u, v] = v))?
sendreq[u, v] ? (fork[u, v] = v) ? (rt[u, v] = u) ? u.h
sendfork[u, v] ?
(fork[u, v] = u) ? ?clean[u, v] ? (rt[u, v] = u) ? ?u.e
Spec5: (odn1), (odn2), (odn7), (odn10)?(odn19), kde
- invariant
(fork[u, v] = u) ? (rt[u, v] = u) ? v.h (odn14)
- rt[u, v] = u unless sendreq[u, v] (odn15)
- sendreq[u, v] ensures rt[u, v] = v (odn16)
- fork[u, v] = u unless sendfork[u, v] (odn17)
- sendfork[u, v] ensures fork[u, v] = v (odn18)
- (u.h ? u.me) ensures ?(u.h ? u.me) (odn19)