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.

You can also download a PDF version of this report and the source files.

```
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 `texModel`

from `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 _
```