This report shows how to solve the famous riddle from Singapore (see New York Times) with epistemic model checking. We use
DEMO_S5 from https://web.archive.org/web/20160803170251/http://homepages.cwi.nl/~jve/software/demo_s5/ and a modified version of
KRIPKEVIS from https://w4eg.de/malvin/illc/kripkevis.
module CHERYL where import Data.List import Data.Function import DEMO_S5 import KRIPKEVIS
We first define the set of all possibilities:
allpos :: [(Int, String)] allpos = [ (15,"May"), (16,"May"), (19,"May"), (17,"June"), (18,"June"), (14,"July"), (16,"July"), (14,"August"), (15,"August"), (17,"August") ]
This forms the set of worlds in our initial model. Moreover, also the set of actual worlds is the full set, hence
allpos occurs twice in the definition below. The two elements of
rels define the epistemic relations of Albert and Bernard. Instead of listing explicitly which possibilities they can distinguish we use haskell functions to say that they confuse the same day and the same month, respectively.
initCheryl :: EpistM (Int,String) = Mo allpos [a,b]  rels allpos where initCheryl = [ ( a, groupBy ((==) `on` snd) allpos ) rels ==) `on` fst) (sortBy (compare `on` fst) allpos) ) ] , ( b, groupBy ((
This is the initial model with all possibilities:
The formula saying that i knows Cheryl’s birthday is defined as the disjunction over all statements of the form “Agent i knows that the birthday is s”:
knowsBday :: Agent -> Form (Int, [Char]) = Disj [ Kn i (Info s) | s <- allpos ]knowsBday i
Now we update the model three times, using the function
upd_pa for public announcements. First with Albert: I don’t know when Cheryl’s birthday is and I know that Bernard does not know.
= upd_pa initCheryl (Conj [Ng $ knowsBday a, Kn a $ Ng (knowsBday b)])model2
The second announcement by Bernard: “Now I know when Cheryl’s birthday is.”
= upd_pa model2 (knowsBday b)model3
Finally, Albert says: “Now I also know when Cheryl’s birthday is.”
= upd_pa model3 (knowsBday a)model4
Lastly, this helper function uses
KRIPKEVIS to generate the drawings:
myTexModel :: EpistM (Int,String) -> String -> IO String Mo states _ _ rels pointed) fn = myTexModel ("" texModel showState showAgent showVal VisModel states rels [(s,0)|s<-states] pointed) fn (where = (show n) ++ string showState (n,string) = if i==a then "Albert" else "Bernard" showAgent i = "" showVal _