module SMCDEL.Examples.DoorMat where

import SMCDEL.Explicit.S5 as Exp hiding (announce)
import SMCDEL.Language
import SMCDEL.Symbolic.S5 hiding (announce)
import SMCDEL.Translations.S5
import SMCDEL.Other.Planning

explain :: Prp -> String
explain :: Prp -> String
explain (P Int
1) = String
"key-under-mat"
explain (P Int
2) = String
"bob-has-key"
explain (P Int
k) = String
"prop-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k

dmStart :: MultipointedKnowScene
dmStart :: MultipointedKnowScene
dmStart = ([Prp] -> Bdd -> [(String, [Prp])] -> KnowStruct
KnS [Prp]
voc Bdd
law [(String, [Prp])]
obs, Bdd
cur) where
  voc :: [Prp]
voc = [ Int -> Prp
P Int
1, Int -> Prp
P Int
2 ]
  law :: Bdd
law = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
2 -- it is common knowledge that Bob has no key
  obs :: [(String, [Prp])]
obs = [ (String
"Anne",[Int -> Prp
P Int
1]), (String
"Bob",[ ]) ] -- Anne knows whether the key is under the mat
  cur :: Bdd
cur = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
1) -- actually, the key is under the mat

tryTake :: MultipointedEvent
tryTake :: MultipointedEvent
tryTake = ([Prp]
-> Form -> [(Prp, Bdd)] -> [(String, [Prp])] -> KnowTransformer
KnTrf [Prp]
addprops Form
addlaw [(Prp, Bdd)]
changeLaw [(String, [Prp])]
addObs, Form -> Bdd
boolBddOf Form
Top) where
  addprops :: [Prp]
addprops    = [Int -> Prp
P Int
3]
  addlaw :: Form
addlaw      = Prp -> Form
PrpF (Int -> Prp
P Int
3) Form -> Form -> Form
`Equi` Prp -> Form
PrpF (Int -> Prp
P Int
1)
  changeLaw :: [(Prp, Bdd)]
changeLaw   = [ (Int -> Prp
P Int
1, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [Prp -> Form
PrpF (Int -> Prp
P Int
3) Form -> Form -> Form
`Impl` Form
Bot, Form -> Form
Neg (Prp -> Form
PrpF (Int -> Prp
P Int
3)) Form -> Form -> Form
`Impl` Prp -> Form
PrpF (Int -> Prp
P Int
1)])
                , (Int -> Prp
P Int
2, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [Prp -> Form
PrpF (Int -> Prp
P Int
3) Form -> Form -> Form
`Impl` Form
Top, Form -> Form
Neg (Prp -> Form
PrpF (Int -> Prp
P Int
3)) Form -> Form -> Form
`Impl` Prp -> Form
PrpF (Int -> Prp
P Int
2)]) ]
  addObs :: [(String, [Prp])]
addObs      = [ (String
"Anne",[]), (String
"Bob",[Int -> Prp
P Int
3]) ]


tryTakeL :: Labelled MultipointedEvent
tryTakeL :: Labelled MultipointedEvent
tryTakeL = (String
"tryTake", MultipointedEvent
tryTake)

dmGoal :: Form
dmGoal :: Form
dmGoal = Prp -> Form
PrpF (Int -> Prp
P Int
2) -- Bob should get the key!

dmTask :: Task MultipointedKnowScene MultipointedEvent
dmTask :: Task MultipointedKnowScene MultipointedEvent
dmTask = MultipointedKnowScene
-> [Labelled MultipointedEvent]
-> Form
-> Task MultipointedKnowScene MultipointedEvent
forall state action.
state -> [(String, action)] -> Form -> Task state action
Task MultipointedKnowScene
dmStart [(String
"tryTake",MultipointedEvent
tryTake)] Form
dmGoal

dmResult :: MultipointedKnowScene
dmResult :: MultipointedKnowScene
dmResult =  MultipointedKnowScene
dmStart MultipointedKnowScene -> MultipointedEvent -> MultipointedKnowScene
forall a b. Update a b => a -> b -> a
`update` MultipointedEvent
tryTake

dmResultKripke :: MultipointedModelS5
dmResultKripke :: MultipointedModelS5
dmResultKripke = MultipointedKnowScene -> MultipointedModelS5
knsToKripkeMulti MultipointedKnowScene
dmResult

dmResultBob :: MultipointedKnowScene
dmResultBob :: MultipointedKnowScene
dmResultBob = (MultipointedKnowScene
dmStart MultipointedKnowScene -> String -> MultipointedKnowScene
forall o. HasPerspective o => o -> String -> o
`asSeenBy` String
"Bob") MultipointedKnowScene -> MultipointedEvent -> MultipointedKnowScene
forall a b. Update a b => a -> b -> a
`update` MultipointedEvent
tryTake

dmResultBobKripke :: MultipointedModelS5
dmResultBobKripke :: MultipointedModelS5
dmResultBobKripke = MultipointedKnowScene -> MultipointedModelS5
knsToKripkeMulti MultipointedKnowScene
dmResultBob

dm :: Task MultipointedKnowScene MultipointedEvent
dm :: Task MultipointedKnowScene MultipointedEvent
dm = MultipointedKnowScene
-> [Labelled MultipointedEvent]
-> Form
-> Task MultipointedKnowScene MultipointedEvent
forall state action.
state -> [(String, action)] -> Form -> Task state action
Task MultipointedKnowScene
dmStart [ Labelled MultipointedEvent
tryTakeL ] Form
dmGoal

dmCoop :: CoopTask MultipointedKnowScene MultipointedEvent
dmCoop :: CoopTask MultipointedKnowScene MultipointedEvent
dmCoop = MultipointedKnowScene
-> [Owned MultipointedEvent]
-> Form
-> CoopTask MultipointedKnowScene MultipointedEvent
forall state action.
state -> [Owned action] -> Form -> CoopTask state action
CoopTask MultipointedKnowScene
dmStart [(String
"Bob",Labelled MultipointedEvent
tryTakeL)] Form
dmGoal

announce :: MultipointedEvent
announce :: MultipointedEvent
announce = ( [Prp]
-> Form -> [(Prp, Bdd)] -> [(String, [Prp])] -> KnowTransformer
KnTrf [] (Prp -> Form
PrpF (Int -> Prp
P Int
1)) [] [ (String
"Anne",[]), (String
"Bob",[]) ]
           , Form -> Bdd
boolBddOf Form
Top )

announce' :: Labelled MultipointedEvent
announce' :: Labelled MultipointedEvent
announce' = (String
"announce", MultipointedEvent
announce)

dmCoop2 :: CoopTask MultipointedKnowScene MultipointedEvent
dmCoop2 :: CoopTask MultipointedKnowScene MultipointedEvent
dmCoop2 = MultipointedKnowScene
-> [Owned MultipointedEvent]
-> Form
-> CoopTask MultipointedKnowScene MultipointedEvent
forall state action.
state -> [Owned action] -> Form -> CoopTask state action
CoopTask MultipointedKnowScene
dmStart [ (String
"Bob" , Labelled MultipointedEvent
tryTakeL )
                           , (String
"Anne", Labelled MultipointedEvent
announce') ] Form
dmGoal

dmPlan2 :: ICPlan MultipointedEvent
dmPlan2 :: [Owned MultipointedEvent]
dmPlan2 = [ (String
"Anne",Labelled MultipointedEvent
announce'), (String
"Bob",Labelled MultipointedEvent
tryTakeL) ]