module Muddy where
import List
import HFKR
import RPAU
import RAMU
import IEMC
{- let's model the case where Bob, Carol and Dave are muddy -}
bcd_dirty = Conj [Neg p1, p2, p3, p4]
{- the following series of updates expresses that each child
is aware of the state (muddy or not) of the other children -}
awareness = [info [b,c,d] p1,
info [a,c,d] p2,
info [a,b,d] p3,
info [a,b,c] p4 ]
{- formulas for knowing whether one is muddy -}
aKn = Disj [K a p1, K a (Neg p1)]
bKn = Disj [K b p2, K b (Neg p2)]
cKn = Disj [K c p3, K c (Neg p3)]
dKn = Disj [K d p4, K d (Neg p4)]
{- We start with an initial situation where the four agents are
blissfully unaware about the muddiness facts, and update
with the test expressing that b,c,d are in fact muddy. This
gives model mu0. -}
mu0 = upd (initM [a,b,c,d] [P 1, P 2, P 3, P 4]) (test bcd_dirty)
{- next, add awareness information -}
mu1 = upds mu0 awareness
{- a public announcement of the father that at least one child
is muddy. -}
mu2 = upd mu1 (public (Disj [p1, p2, p3, p4]))
{- the first round: they all say they don't know their state. -}
mu3 = upd mu2 (public (Conj[Neg aKn, Neg bKn, Neg cKn, Neg dKn]))
{- the second round: they still all don't know their state. -}
mu4 = upd mu3 (public (Conj[Neg aKn, Neg bKn, Neg cKn, Neg dKn]))
{- now b, c and d say they know. In the final model all is
known to everyone -}
mu5 = upds mu4 [public (Conj[bKn, cKn, dKn])]