module SMCDEL.Examples.SimpleS5 where

import Data.List ((\\))

import SMCDEL.Explicit.S5
import SMCDEL.Translations.S5
import SMCDEL.Symbolic.S5
import SMCDEL.Language

myStart :: KnowScene
myStart :: KnowScene
myStart = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Int -> Prp
P Int
0] (Form -> Bdd
boolBddOf Form
Top) [(Agent
"Alice",[]),(Agent
"Bob",[Int -> Prp
P Int
0])],[Int -> Prp
P Int
0])

publicMakeFalse :: [Agent] -> Prp -> Event
publicMakeFalse :: [Agent] -> Prp -> Event
publicMakeFalse [Agent]
agents Prp
p = ([Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer
KnTrf [] Form
Top [(Prp, Bdd)]
mychangelaw [(Agent, [Prp])]
forall {a}. [(Agent, [a])]
myobs, []) where
  mychangelaw :: [(Prp, Bdd)]
mychangelaw = [ (Prp
p,Form -> Bdd
boolBddOf Form
Bot) ]
  myobs :: [(Agent, [a])]
myobs = [ (Agent
i,[]) | Agent
i <- [Agent]
agents ]

myEvent :: Event
myEvent :: Event
myEvent = [Agent] -> Prp -> Event
publicMakeFalse (KnowScene -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KnowScene
myStart) (Int -> Prp
P Int
0)

myResult :: KnowScene
myResult :: KnowScene
myResult = KnowScene
myStart KnowScene -> Event -> KnowScene
forall a b. Update a b => a -> b -> a
`update` Event
myEvent

exampleStart :: KnowScene
exampleStart :: KnowScene
exampleStart = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Int -> Prp
P Int
0] (Form -> Bdd
boolBddOf Form
Top) [(Agent
"Alice",[]),(Agent
"Bob",[Int -> Prp
P Int
0])],[Int -> Prp
P Int
0])

makeFalseShowTo :: [Agent] -> Prp -> [Agent] -> Event
makeFalseShowTo :: [Agent] -> Prp -> [Agent] -> Event
makeFalseShowTo [Agent]
agents Prp
p [Agent]
intheknow = ([Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer
KnTrf [Int -> Prp
P Int
99] Form
Top [(Prp, Bdd)]
examplechangelaw [(Agent, [Prp])]
exampleobs, []) where
  examplechangelaw :: [(Prp, Bdd)]
examplechangelaw = [ (Prp
p,Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
99)) ]
  exampleobs :: [(Agent, [Prp])]
exampleobs = [ (Agent
i,[Int -> Prp
P Int
99]) | Agent
i <- [Agent]
intheknow           ]
            [(Agent, [Prp])] -> [(Agent, [Prp])] -> [(Agent, [Prp])]
forall a. [a] -> [a] -> [a]
++ [ (Agent
i,[    ]) | Agent
i <- [Agent]
agents [Agent] -> [Agent] -> [Agent]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Agent]
intheknow ]

exampleEvent :: Event
exampleEvent :: Event
exampleEvent = [Agent] -> Prp -> [Agent] -> Event
makeFalseShowTo (KnowScene -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KnowScene
exampleStart) (Int -> Prp
P Int
0) [Agent
"Bob"]

exampleResult :: KnowScene
exampleResult :: KnowScene
exampleResult = KnowScene
exampleStart KnowScene -> Event -> KnowScene
forall a b. Update a b => a -> b -> a
`update` Event
exampleEvent

thirdEvent :: Event
thirdEvent :: Event
thirdEvent = [Agent] -> Prp -> [Agent] -> Event
makeFalseShowTo (KnowScene -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KnowScene
exampleStart) (Int -> Prp
P Int
0) [Agent
"Alice"]

thirdResult :: KnowScene
thirdResult :: KnowScene
thirdResult = KnowScene
exampleStart KnowScene -> Event -> KnowScene
forall a b. Update a b => a -> b -> a
`update` Event
thirdEvent

problemPM :: PointedModelS5
problemPM :: PointedModelS5
problemPM = ( [Int]
-> [(Agent, Partition)] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5 [Int
0,Int
1,Int
2,Int
3] [ (Agent
alice,[[Int
0],[Int
1,Int
2,Int
3]]), (Agent
bob,[[Int
0,Int
1,Int
2],[Int
3]]) ]
  [ (Int
0,[(Int -> Prp
P Int
1,Bool
True ),(Int -> Prp
P Int
2,Bool
True )]), (Int
1,[(Int -> Prp
P Int
1,Bool
True ),(Int -> Prp
P Int
2,Bool
False)])
  , (Int
2,[(Int -> Prp
P Int
1,Bool
False),(Int -> Prp
P Int
2,Bool
True )]), (Int
3,[(Int -> Prp
P Int
1,Bool
False),(Int -> Prp
P Int
2,Bool
False)]) ], Int
1::World )

problemKNS :: KnowScene
problemKNS :: KnowScene
problemKNS = PointedModelS5 -> KnowScene
kripkeToKns PointedModelS5
problemPM