module SMCDEL.Examples.CoinFlip where

import Data.Map.Strict (fromList)
import Data.List ((\\))

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

coinStart :: BelScene
coinStart :: BelScene
coinStart = ([Prp] -> Bdd -> Map Agent RelBDD -> BelStruct
BlS [Int -> Prp
P Int
0] Bdd
law Map Agent RelBDD
obs, [Prp]
actual) where
  law :: Bdd
law    = Form -> Bdd
boolBddOf (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
0)
  obs :: Map Agent RelBDD
obs    = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Agent
"a", [Prp] -> RelBDD
allsamebdd [Int -> Prp
P Int
0]), (Agent
"b", [Prp] -> RelBDD
allsamebdd [Int -> Prp
P Int
0]) ]
  actual :: [Prp]
actual = [Int -> Prp
P Int
0]

flipRandomAndShowTo :: [Agent] -> Prp -> Agent -> Event
flipRandomAndShowTo :: [Agent] -> Prp -> Agent -> Event
flipRandomAndShowTo [Agent]
everyone Prp
p Agent
i = ([Prp] -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
Trf [Prp
q] Form
eventlaw Map Prp Bdd
changelaw Map Agent RelBDD
obs, [Prp
q]) where
  q :: Prp
q = [Prp] -> Prp
freshp [Prp
p]
  eventlaw :: Form
eventlaw = Form
Top
  changelaw :: Map Prp Bdd
changelaw = [(Prp, Bdd)] -> Map Prp Bdd
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Prp
p, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF Prp
q) ]
  obs :: Map Agent RelBDD
obs = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(Agent, RelBDD)] -> Map Agent RelBDD)
-> [(Agent, RelBDD)] -> Map Agent RelBDD
forall a b. (a -> b) -> a -> b
$
    (Agent
i, [Prp] -> RelBDD
allsamebdd  [Prp
q]) (Agent, RelBDD) -> [(Agent, RelBDD)] -> [(Agent, RelBDD)]
forall a. a -> [a] -> [a]
:
    [ (Agent
j,RelBDD
totalRelBdd) | Agent
j <- [Agent]
everyone [Agent] -> [Agent] -> [Agent]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Agent
i] ]

coinFlip :: Event
coinFlip :: Event
coinFlip = [Agent] -> Prp -> Agent -> Event
flipRandomAndShowTo [Agent
"a",Agent
"b"] (Int -> Prp
P Int
0) Agent
"b"

coinResult :: BelScene
coinResult :: BelScene
coinResult = BelScene
coinStart BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
`update` Event
coinFlip