{-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}

module SMCDEL.Examples.SimpleK where

import Data.HasCacBDD hiding (Bot,Top)
import Data.List ((\\))
import qualified Data.Map.Strict as M
import Data.Tagged (untag)

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

exampleModel :: KripkeModel
exampleModel :: KripkeModel
exampleModel = Map Action (Map Prp Bool, Map Agent [Action]) -> KripkeModel
KrM (Map Action (Map Prp Bool, Map Agent [Action]) -> KripkeModel)
-> Map Action (Map Prp Bool, Map Agent [Action]) -> KripkeModel
forall a b. (a -> b) -> a -> b
$ [(Action, (Map Prp Bool, Map Agent [Action]))]
-> Map Action (Map Prp Bool, Map Agent [Action])
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
  [ (Action
1, ([(Prp, Bool)] -> Map Prp Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Action -> Prp
P Action
0,Bool
True ),(Action -> Prp
P Action
1,Bool
True )], [(Agent, [Action])] -> Map Agent [Action]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent
alice,[Action
1]), (Agent
bob,[Action
1])] ) )
  , (Action
2, ([(Prp, Bool)] -> Map Prp Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Action -> Prp
P Action
0,Bool
False),(Action -> Prp
P Action
1,Bool
True )], [(Agent, [Action])] -> Map Agent [Action]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent
alice,[Action
1]), (Agent
bob,[Action
2])] ) ) ]

examplePointedModel :: PointedModel
examplePointedModel :: PointedModel
examplePointedModel = (KripkeModel
exampleModel,Action
1)

aliceBdd, bobBdd :: Bdd
[Bdd
aliceBdd,Bdd
bobBdd] = (Agent -> Bdd) -> [Agent] -> [Bdd]
forall a b. (a -> b) -> [a] -> [b]
map (Tagged Dubbel Bdd -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag (Tagged Dubbel Bdd -> Bdd)
-> (Agent -> Tagged Dubbel Bdd) -> Agent -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Agent -> KripkeModel -> Tagged Dubbel Bdd)
-> KripkeModel -> Agent -> Tagged Dubbel Bdd
forall a b c. (a -> b -> c) -> b -> a -> c
flip Agent -> KripkeModel -> Tagged Dubbel Bdd
SMCDEL.Symbolic.K.relBddOfIn KripkeModel
exampleModel) [Agent
alice,Agent
bob]

-- Privately tell alice that P 0, while bob thinks nothing happens.
exampleGenActM :: ActionModel
exampleGenActM :: ActionModel
exampleGenActM = Map Action Act -> ActionModel
ActM (Map Action Act -> ActionModel) -> Map Action Act -> ActionModel
forall a b. (a -> b) -> a -> b
$ [(Action, Act)] -> Map Action Act
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
  [ (Action
1, Act { pre :: Form
pre = Prp -> Form
PrpF (Action -> Prp
P Action
0), post :: PostCondition
post = PostCondition
forall k a. Map k a
M.empty, rel :: Map Agent [Action]
rel = [(Agent, [Action])] -> Map Agent [Action]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent
alice,[Action
1]), (Agent
bob,[Action
2])] } )
  , (Action
2, Act { pre :: Form
pre = Form
Top       , post :: PostCondition
post = PostCondition
forall k a. Map k a
M.empty, rel :: Map Agent [Action]
rel = [(Agent, [Action])] -> Map Agent [Action]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent
alice,[Action
2]), (Agent
bob,[Action
2])] } )
  ]

examplePointedActM :: PointedActionModel
examplePointedActM :: PointedActionModel
examplePointedActM = (ActionModel
exampleGenActM,Action
1)

exampleResult :: PointedModel
exampleResult :: PointedModel
exampleResult = PointedModel -> PointedActionModel -> PointedModel
forall a b. Update a b => a -> b -> a
update PointedModel
examplePointedModel PointedActionModel
examplePointedActM

exampleStart :: BelScene
exampleStart :: BelScene
exampleStart = ([Prp] -> Bdd -> Map Agent (Tagged Dubbel Bdd) -> BelStruct
BlS [Action -> Prp
P Action
0] Bdd
law Map Agent (Tagged Dubbel Bdd)
obs, [Prp]
actual) where
  law :: Bdd
law    = Form -> Bdd
boolBddOf Form
Top
  obs :: Map Agent (Tagged Dubbel Bdd)
obs    = [(Agent, Tagged Dubbel Bdd)] -> Map Agent (Tagged Dubbel Bdd)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Agent
"1", Bdd -> Tagged Dubbel Bdd
mvBdd (Bdd -> Tagged Dubbel Bdd) -> Bdd -> Tagged Dubbel Bdd
forall a b. (a -> b) -> a -> b
$ Form -> Bdd
boolBddOf Form
Top), (Agent
"2", [Prp] -> Tagged Dubbel Bdd
allsamebdd [Action -> Prp
P Action
0]) ]
  actual :: [Prp]
actual = [Action -> Prp
P Action
0]

exampleEvent :: Event
exampleEvent :: Event
exampleEvent = ([Prp]
-> Form
-> Map Prp Bdd
-> Map Agent (Tagged Dubbel Bdd)
-> Transformer
Trf [Action -> Prp
P Action
1] Form
addlaw Map Prp Bdd
forall k a. Map k a
M.empty Map Agent (Tagged Dubbel Bdd)
eventObs, [Action -> Prp
P Action
1]) where
  addlaw :: Form
addlaw = Prp -> Form
PrpF (Action -> Prp
P Action
1) Form -> Form -> Form
`Impl` Prp -> Form
PrpF (Action -> Prp
P Action
0)
  eventObs :: Map Agent (Tagged Dubbel Bdd)
eventObs = [(Agent, Tagged Dubbel Bdd)] -> Map Agent (Tagged Dubbel Bdd)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Agent
"1", [Prp] -> Tagged Dubbel Bdd
allsamebdd [Action -> Prp
P Action
1]), (Agent
"2", Bdd -> Tagged Dubbel Bdd
cpBdd (Bdd -> Tagged Dubbel Bdd)
-> (Form -> Bdd) -> Form -> Tagged Dubbel Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Bdd
boolBddOf (Form -> Tagged Dubbel Bdd) -> Form -> Tagged Dubbel Bdd
forall a b. (a -> b) -> a -> b
$ Form -> Form
Neg (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Action -> Prp
P Action
1)) ]

exampleBlTresult :: BelScene
exampleBlTresult :: BelScene
exampleBlTresult = BelScene
exampleStart BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
`update` Event
exampleEvent

publicMakeFalseActM :: [Agent] -> Prp -> PointedActionModel
publicMakeFalseActM :: [Agent] -> Prp -> PointedActionModel
publicMakeFalseActM [Agent]
ags Prp
p =
  (Map Action Act -> ActionModel
ActM (Map Action Act -> ActionModel) -> Map Action Act -> ActionModel
forall a b. (a -> b) -> a -> b
$ [(Action, Act)] -> Map Action Act
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Action
1::Int, Form -> PostCondition -> Map Agent [Action] -> Act
Act Form
myPre PostCondition
myPost Map Agent [Action]
myRel) ], Action
0) where
    myPre :: Form
myPre  = Form
Top
    myPost :: PostCondition
myPost = [(Prp, Form)] -> PostCondition
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Prp
p,Form
Bot)]
    myRel :: Map Agent [Action]
myRel  = [(Agent, [Action])] -> Map Agent [Action]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent
i,[Action
1]) | Agent
i <- [Agent]
ags]

publicMakeFalseTrf :: [Agent] -> Prp -> Event
publicMakeFalseTrf :: [Agent] -> Prp -> Event
publicMakeFalseTrf [Agent]
agents Prp
p = ([Prp]
-> Form
-> Map Prp Bdd
-> Map Agent (Tagged Dubbel Bdd)
-> Transformer
Trf [] Form
Top Map Prp Bdd
changelaw Map Agent (Tagged Dubbel Bdd)
eventobs, []) where
  changelaw :: Map Prp Bdd
changelaw = [(Prp, Bdd)] -> Map Prp Bdd
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Prp
p,Form -> Bdd
boolBddOf Form
Bot) ]
  eventobs :: Map Agent (Tagged Dubbel Bdd)
eventobs  = [(Agent, Tagged Dubbel Bdd)] -> Map Agent (Tagged Dubbel Bdd)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Agent
i,Tagged Dubbel Bdd
totalRelBdd) | Agent
i <- [Agent]
agents ]

myEvent :: Event
myEvent :: Event
myEvent = [Agent] -> Prp -> Event
publicMakeFalseTrf (BelScene -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf BelScene
exampleStart) (Action -> Prp
P Action
0)

tResult :: BelScene
tResult :: BelScene
tResult = BelScene
exampleStart BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
`update` Event
myEvent

flipOverAndShowTo :: [Agent] -> Prp -> Agent -> Event
flipOverAndShowTo :: [Agent] -> Prp -> Agent -> Event
flipOverAndShowTo [Agent]
everyone Prp
p Agent
i = ([Prp]
-> Form
-> Map Prp Bdd
-> Map Agent (Tagged Dubbel Bdd)
-> Transformer
Trf [Prp
q] Form
eventlaw Map Prp Bdd
changelaw Map Agent (Tagged Dubbel Bdd)
eventobs, [Prp
q]) where
  q :: Prp
q         = [Prp] -> Prp
freshp [Prp
p]
  eventlaw :: Form
eventlaw  = Prp -> Form
PrpF Prp
q Form -> Form -> Form
`Equi` Prp -> Form
PrpF Prp
p
  changelaw :: Map Prp Bdd
changelaw = [(Prp, Bdd)] -> Map Prp Bdd
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Prp
p, Form -> Bdd
boolBddOf (Form -> Bdd) -> (Prp -> Form) -> Prp -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
Neg (Form -> Form) -> (Prp -> Form) -> Prp -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prp -> Form
PrpF (Prp -> Bdd) -> Prp -> Bdd
forall a b. (a -> b) -> a -> b
$ Prp
p) ]
  eventobs :: Map Agent (Tagged Dubbel Bdd)
eventobs  = [(Agent, Tagged Dubbel Bdd)] -> Map Agent (Tagged Dubbel Bdd)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Agent, Tagged Dubbel Bdd)] -> Map Agent (Tagged Dubbel Bdd))
-> [(Agent, Tagged Dubbel Bdd)] -> Map Agent (Tagged Dubbel Bdd)
forall a b. (a -> b) -> a -> b
$ (Agent
i, [Prp] -> Tagged Dubbel Bdd
allsamebdd [Prp
q])
                       (Agent, Tagged Dubbel Bdd)
-> [(Agent, Tagged Dubbel Bdd)] -> [(Agent, Tagged Dubbel Bdd)]
forall a. a -> [a] -> [a]
: [ (Agent
j,Tagged Dubbel Bdd
totalRelBdd) | Agent
j <- [Agent]
everyone [Agent] -> [Agent] -> [Agent]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Agent
i] ]

myOtherEvent :: Event
myOtherEvent :: Event
myOtherEvent = [Agent] -> Prp -> Agent -> Event
flipOverAndShowTo [Agent
"1",Agent
"2"] (Action -> Prp
P Action
0) Agent
"1"

tResult2 :: BelScene
tResult2 :: BelScene
tResult2 = BelScene
exampleStart BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
`update` Event
myOtherEvent

exampleBelScn :: BelScene
exampleBelScn :: BelScene
exampleBelScn = PointedModel -> BelScene
kripkeToBls PointedModel
examplePointedModel