Vecerajúci filozofi 2
Špecifikácia pre user:
- u.t unless u.h in user (udn1)
- stable u.h in user (udn2)
- u.e unless u.t in user (udn3)
- podmienená vlastnost pre user: (udn4)
??(u, v) :: ?(u.e ? v.e)? / ? ?u :: u.e ? ?u.e?
Špecifikácia pre user ? os:
- invariant ?(u.e ? v.e ? E[u, v]) in user ? os (dn1)
- u.h ? u.e in user ? os (dn2)
obmedzenia pre os:
- constant u.t in os (odn1)
- stable u.e in os (odn2)
t.j. v os nie sú prechody z eating a prechody z a do thinking
odvodená vlastnost pre user:
odvodené vlastnosti pre os:
- stable ?u.h in os
- u.h unless u.e in os
odvodené vlastnosti pre user ? os:
- u.t unless u.h in user ? os (dn3)
- u.h unless u.e in user ? os (dn4)
- u.e unless u.t in user ? os (dn5)