{- |
We model the story of the muddy children which is known in many versions.
See for example~\cite{Littlewood1953:amm},~\cite[p.~24-30]{fagin1995reasoning} or~\cite[p.~93-96]{DitHoekKooi2007:del}.

Our implementation treats the general case for \(n\) children out of which \(m\) are muddy, but we focus on the case of three children who are all muddy.
As usual, all children can observe whether the others are muddy but do not see their own face.
This is represented by the observational variables:
Agent $1$ observes $p_2$ and $p_3$, agent $2$ observes $p_1$ and $p_3$ and agent $3$ observes $p_1$ and $p_2$.
-}

module SMCDEL.Examples.MuddyChildren where

import Data.List
import Data.Maybe (fromJust)
import Data.Map.Strict (fromList)

import SMCDEL.Internal.Help (seteq)
import SMCDEL.Language
import SMCDEL.Symbolic.S5
import qualified SMCDEL.Symbolic.K
import qualified SMCDEL.Explicit.K

-- | The initial knowledge structure, given the total number of children, and the number of muddy children.
mudScnInit :: Int -> Int -> KnowScene
mudScnInit :: World -> World -> KnowScene
mudScnInit World
n World
m = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
vocab Bdd
law [(Agent, [Prp])]
obs, [Prp]
actual) where
  vocab :: [Prp]
vocab  = [World -> Prp
P World
1 .. World -> Prp
P World
n]
  law :: Bdd
law    = Form -> Bdd
boolBddOf Form
Top
  obs :: [(Agent, [Prp])]
obs    = [ (World -> Agent
forall a. Show a => a -> Agent
show World
i, Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) [Prp]
vocab) | World
i <- [World
1..World
n] ]
  actual :: [Prp]
actual = [World -> Prp
P World
1 .. World -> Prp
P World
m]

-- | The initial structure for 3 muddy children.
myMudScnInit :: KnowScene
myMudScnInit :: KnowScene
myMudScnInit = World -> World -> KnowScene
mudScnInit World
3 World
3

-- | A formula to say that the given child knows whether it is muddy.
knows :: Int -> Form
knows :: World -> Form
knows World
i = Agent -> Form -> Form
Kw (World -> Agent
forall a. Show a => a -> Agent
show World
i) (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ World -> Prp
P World
i)

-- | A formula to say that none out of \(n\) children knows its own state.
nobodyknows :: Int -> Form
nobodyknows :: World -> Form
nobodyknows World
n = [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ World -> Form
knows World
i | World
i <- [World
1..World
n] ]

-- | Announcement of the father announce that someone is muddy.
father :: Int -> Form
father :: World -> Form
father World
n = [Form] -> Form
Disj ((Prp -> Form) -> [Prp] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Form
PrpF [World -> Prp
P World
1 .. World -> Prp
P World
n])

-- | Result after announcing `father 3` in `myMudScnInit`.
mudScn0 :: KnowScene
mudScn0 :: KnowScene
mudScn0 = KnowScene -> Form -> KnowScene
forall a b. Update a b => a -> b -> a
update KnowScene
myMudScnInit (World -> Form
father World
3)

mudScn1 :: KnowScene
mudScn1 :: KnowScene
mudScn1 = KnowScene -> Form -> KnowScene
forall a b. Update a b => a -> b -> a
update KnowScene
mudScn0 (World -> Form
nobodyknows World
3)

mudScn2 :: KnowScene
mudKns2 :: KnowStruct
mudScn2 :: KnowScene
mudScn2@(KnowStruct
mudKns2,[Prp]
_) = KnowScene -> Form -> KnowScene
forall a b. Update a b => a -> b -> a
update KnowScene
mudScn1 (World -> Form
nobodyknows World
3)

empty :: Int -> KnowScene
empty :: World -> KnowScene
empty World
n = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [] (Form -> Bdd
boolBddOf Form
Top) [(Agent, [Prp])]
forall {a}. [(Agent, [a])]
obs,[]) where
  obs :: [(Agent, [a])]
obs    = [ (World -> Agent
forall a. Show a => a -> Agent
show World
i, []) | World
i <- [World
1..World
n] ]

buildMC :: Int -> Int -> Event
buildMC :: World -> World -> Event
buildMC World
n World
m = (([Prp]
 -> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer)
-> [Prp] -> Form -> [(Agent, [Prp])] -> KnowTransformer
noChange [Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer
KnTrf [Prp]
vocab Form
Top [(Agent, [Prp])]
obs, (World -> Prp) -> [World] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map World -> Prp
P [World
1..World
m]) where
  obs :: [(Agent, [Prp])]
obs = [ (World -> Agent
forall a. Show a => a -> Agent
show World
i, Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) [Prp]
vocab) | World
i <- [World
1..World
n] ]
  vocab :: [Prp]
vocab = (World -> Prp) -> [World] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map World -> Prp
P [World
1..World
n]

buildResult :: KnowScene
buildResult :: KnowScene
buildResult = World -> KnowScene
empty World
3 KnowScene -> Event -> KnowScene
forall a b. Update a b => a -> b -> a
`update` World -> World -> Event
buildMC World
3 World
3

mudGenKrpInit :: Int -> Int -> SMCDEL.Explicit.K.PointedModel
mudGenKrpInit :: World -> World -> PointedModel
mudGenKrpInit World
n World
m = (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
SMCDEL.Explicit.K.KrM (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel)
-> Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
forall a b. (a -> b) -> a -> b
$ [(World, (Map Prp Bool, Map Agent [World]))]
-> Map World (Map Prp Bool, Map Agent [World])
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(World, (Map Prp Bool, Map Agent [World]))]
wlist, World
cur) where
  wlist :: [(World, (Map Prp Bool, Map Agent [World]))]
wlist = [ (World
w, ([(Prp, Bool)] -> Map Prp Bool
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([[(Prp, Bool)]]
vals [[(Prp, Bool)]] -> World -> [(Prp, Bool)]
forall a. HasCallStack => [a] -> World -> a
!! World
w), [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(Agent, [World])] -> Map Agent [World])
-> [(Agent, [World])] -> Map Agent [World]
forall a b. (a -> b) -> a -> b
$ World -> [(Agent, [World])]
relFor World
w)) | World
w <- [World]
ws ]
  ws :: [World]
ws    = [World
0..(World
2World -> World -> World
forall a b. (Num a, Integral b) => a -> b -> a
^World
nWorld -> World -> World
forall a. Num a => a -> a -> a
-World
1)]
  vals :: [[(Prp, Bool)]]
vals  = ([(Prp, Bool)] -> [(Prp, Bool)])
-> [[(Prp, Bool)]] -> [[(Prp, Bool)]]
forall a b. (a -> b) -> [a] -> [b]
map [(Prp, Bool)] -> [(Prp, Bool)]
forall a. Ord a => [a] -> [a]
sort (([[(Prp, Bool)]] -> Prp -> [[(Prp, Bool)]])
-> [[(Prp, Bool)]] -> [Prp] -> [[(Prp, Bool)]]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [[(Prp, Bool)]] -> Prp -> [[(Prp, Bool)]]
forall {a}. [[(a, Bool)]] -> a -> [[(a, Bool)]]
buildTable [[]] [World -> Prp
P World
k | World
k<- [World
1..World
n]])
  buildTable :: [[(a, Bool)]] -> a -> [[(a, Bool)]]
buildTable [[(a, Bool)]]
partrows a
p = [ (a
p,Bool
v)(a, Bool) -> [(a, Bool)] -> [(a, Bool)]
forall a. a -> [a] -> [a]
:[(a, Bool)]
pr | Bool
v <-[Bool
True,Bool
False], [(a, Bool)]
pr <- [[(a, Bool)]]
partrows ]
  relFor :: World -> [(Agent, [World])]
relFor World
w = [ (World -> Agent
forall a. Show a => a -> Agent
show World
i, World -> World -> [World]
seesFrom World
i World
w) | World
i <- [World
1..World
n] ]
  seesFrom :: World -> World -> [World]
seesFrom World
i World
w = (World -> Bool) -> [World] -> [World]
forall a. (a -> Bool) -> [a] -> [a]
filter (\World
v -> World -> [(Prp, Bool)] -> [(Prp, Bool)] -> Bool
samefor World
i ([[(Prp, Bool)]]
vals [[(Prp, Bool)]] -> World -> [(Prp, Bool)]
forall a. HasCallStack => [a] -> World -> a
!! World
w) ([[(Prp, Bool)]]
vals [[(Prp, Bool)]] -> World -> [(Prp, Bool)]
forall a. HasCallStack => [a] -> World -> a
!! World
v)) [World]
ws
  samefor :: World -> [(Prp, Bool)] -> [(Prp, Bool)] -> Bool
samefor World
i [(Prp, Bool)]
ps [(Prp, Bool)]
qs = [Prp] -> [Prp] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
seteq (Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) (((Prp, Bool) -> Prp) -> [(Prp, Bool)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst ([(Prp, Bool)] -> [Prp]) -> [(Prp, Bool)] -> [Prp]
forall a b. (a -> b) -> a -> b
$ ((Prp, Bool) -> Bool) -> [(Prp, Bool)] -> [(Prp, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp, Bool) -> Bool
forall a b. (a, b) -> b
snd [(Prp, Bool)]
ps)) (Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) (((Prp, Bool) -> Prp) -> [(Prp, Bool)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst ([(Prp, Bool)] -> [Prp]) -> [(Prp, Bool)] -> [Prp]
forall a b. (a -> b) -> a -> b
$ ((Prp, Bool) -> Bool) -> [(Prp, Bool)] -> [(Prp, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp, Bool) -> Bool
forall a b. (a, b) -> b
snd [(Prp, Bool)]
qs))
  cur :: World
cur = Maybe World -> World
forall a. HasCallStack => Maybe a -> a
fromJust ([(Prp, Bool)] -> [[(Prp, Bool)]] -> Maybe World
forall a. Eq a => a -> [a] -> Maybe World
elemIndex [(Prp, Bool)]
curVal [[(Prp, Bool)]]
vals)
  curVal :: [(Prp, Bool)]
curVal = [(Prp, Bool)] -> [(Prp, Bool)]
forall a. Ord a => [a] -> [a]
sort ([(Prp, Bool)] -> [(Prp, Bool)]) -> [(Prp, Bool)] -> [(Prp, Bool)]
forall a b. (a -> b) -> a -> b
$ [(Prp
p,Bool
True) | Prp
p <- [World -> Prp
P World
1 .. World -> Prp
P World
m]] [(Prp, Bool)] -> [(Prp, Bool)] -> [(Prp, Bool)]
forall a. [a] -> [a] -> [a]
++ [(Prp
p,Bool
True) | Prp
p <- [World -> Prp
P (World
mWorld -> World -> World
forall a. Num a => a -> a -> a
+World
1) .. World -> Prp
P World
n]]

myMudGenKrpInit :: SMCDEL.Explicit.K.PointedModel
myMudGenKrpInit :: PointedModel
myMudGenKrpInit = World -> World -> PointedModel
mudGenKrpInit World
3 World
3

mudBelScnInit :: Int -> Int -> SMCDEL.Symbolic.K.BelScene
mudBelScnInit :: World -> World -> BelScene
mudBelScnInit World
n World
m = ([Prp] -> Bdd -> Map Agent RelBDD -> BelStruct
SMCDEL.Symbolic.K.BlS [Prp]
vocab Bdd
law Map Agent RelBDD
obs, [Prp]
actual) where
  vocab :: [Prp]
vocab  = [World -> Prp
P World
1 .. World -> Prp
P World
n]
  law :: Bdd
law    = Form -> Bdd
boolBddOf Form
Top
  obs :: Map Agent RelBDD
obs    = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(World -> Agent
forall a. Show a => a -> Agent
show World
i, [Prp] -> RelBDD
SMCDEL.Symbolic.K.allsamebdd ([Prp] -> RelBDD) -> [Prp] -> RelBDD
forall a b. (a -> b) -> a -> b
$ Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) [Prp]
vocab) | World
i <- [World
1..World
n]]
  actual :: [Prp]
actual = [World -> Prp
P World
1 .. World -> Prp
P World
m]

myMudBelScnInit :: SMCDEL.Symbolic.K.BelScene
myMudBelScnInit :: BelScene
myMudBelScnInit = World -> World -> BelScene
mudBelScnInit World
3 World
3