module SMCDEL.Examples.SallyAnne where

import Data.Map.Strict (fromList)

import SMCDEL.Language
import SMCDEL.Symbolic.K
import SMCDEL.Symbolic.S5 (boolBddOf)

pp, qq, tt :: Prp
pp :: Prp
pp = Int -> Prp
P Int
0
tt :: Prp
tt = Int -> Prp
P Int
1
qq :: Prp
qq = Int -> Prp
P Int
7 -- this number does not matter

sallyInit :: BelScene
sallyInit :: BelScene
sallyInit = ([Prp] -> Bdd -> Map Agent RelBDD -> BelStruct
BlS [Prp
pp, Prp
tt] Bdd
law Map Agent RelBDD
obs, [Prp]
actual) where
  law :: Bdd
law    = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [Prp -> Form
PrpF Prp
pp, Form -> Form
Neg (Prp -> Form
PrpF Prp
tt)]
  obs :: Map Agent RelBDD
obs    = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Agent
"Sally", RelBDD
totalRelBdd), (Agent
"Anne", RelBDD
totalRelBdd) ]
  actual :: [Prp]
actual = [Prp
pp]

sallyPutsMarbleInBasket :: Event
sallyPutsMarbleInBasket :: Event
sallyPutsMarbleInBasket = ([Prp] -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
Trf [] Form
Top
  ([(Prp, Bdd)] -> Map Prp Bdd
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Prp
tt,Form -> Bdd
boolBddOf Form
Top) ])
  ([(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Agent
i,RelBDD
totalRelBdd) | Agent
i <- [Agent
"Anne",Agent
"Sally"] ]), [])

sallyIntermediate1 :: BelScene
sallyIntermediate1 :: BelScene
sallyIntermediate1 = BelScene
sallyInit BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
`update` Event
sallyPutsMarbleInBasket

sallyLeaves :: Event
sallyLeaves :: Event
sallyLeaves = ([Prp] -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
Trf [] Form
Top
  ([(Prp, Bdd)] -> Map Prp Bdd
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Prp
pp,Form -> Bdd
boolBddOf Form
Bot) ])
  ([(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Agent
i,RelBDD
totalRelBdd) | Agent
i <- [Agent
"Anne",Agent
"Sally"] ]), [])

sallyIntermediate2 :: BelScene
sallyIntermediate2 :: BelScene
sallyIntermediate2 = BelScene
sallyIntermediate1 BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
`update` Event
sallyLeaves

annePutsMarbleInBox :: Event
annePutsMarbleInBox :: Event
annePutsMarbleInBox = ([Prp] -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
Trf [Prp
qq] Form
Top
  ([(Prp, Bdd)] -> Map Prp Bdd
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Prp
tt,Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [Form -> Form
Neg (Prp -> Form
PrpF Prp
qq) Form -> Form -> Form
`Impl` Prp -> Form
PrpF Prp
tt, Prp -> Form
PrpF Prp
qq Form -> Form -> Form
`Impl` Form
Bot]) ])
  ([(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Agent
"Anne", [Prp] -> RelBDD
allsamebdd [Prp
qq]), (Agent
"Sally", Bdd -> RelBDD
cpBdd (Bdd -> RelBDD) -> Bdd -> RelBDD
forall a b. (a -> b) -> a -> b
$ Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Form -> Form
Neg (Prp -> Form
PrpF Prp
qq))  ]), [Prp
qq])

sallyIntermediate3 :: BelScene
sallyIntermediate3 :: BelScene
sallyIntermediate3 = BelScene
sallyIntermediate2 BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
`update` Event
annePutsMarbleInBox

sallyComesBack :: Event
sallyComesBack :: Event
sallyComesBack = ([Prp] -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
Trf [] Form
Top
  ([(Prp, Bdd)] -> Map Prp Bdd
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Prp
pp,Form -> Bdd
boolBddOf Form
Top) ])
  ([(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Agent
i,RelBDD
totalRelBdd) | Agent
i <- [Agent
"Anne",Agent
"Sally"] ]), [])

sallyIntermediate4 :: BelScene
sallyIntermediate4 :: BelScene
sallyIntermediate4 = BelScene
sallyIntermediate3 BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
`update` Event
sallyComesBack

sallyFinal :: BelScene
sallyFinal :: BelScene
sallyFinal = BelScene
sallyInit BelScene -> [Event] -> BelScene
forall a b. Update a b => a -> [b] -> a
`updates`
  [ Event
sallyPutsMarbleInBasket
  , Event
sallyLeaves
  , Event
annePutsMarbleInBox
  , Event
sallyComesBack ]

sallyFinalCheck :: Bool
sallyFinalCheck :: Bool
sallyFinalCheck = BelScene -> Form -> Bool
SMCDEL.Symbolic.K.evalViaBdd BelScene
sallyFinal (Agent -> Form -> Form
K Agent
"Sally" (Prp -> Form
PrpF Prp
tt))