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])]