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

module SMCDEL.Examples.Prisoners where

import Data.HasCacBDD hiding (Top,Bot)

import SMCDEL.Explicit.S5
import SMCDEL.Internal.TexDisplay
import SMCDEL.Language
import SMCDEL.Symbolic.S5

n :: Int
n :: Int
n = Int
3

light :: Form
light :: Form
light = Prp -> Form
PrpF (Int -> Prp
P Int
0)

-- P 0 -- light is on
-- P i -- agent i has been in the room (and switched on the light)
-- agents: 1 is the counter, 2 and 3 are the others

prisonExpStart :: KripkeModelS5
prisonExpStart :: KripkeModelS5
prisonExpStart =
  [Int]
-> [(Agent, Partition)] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5
    [Int
1]
    [ (Agent
"1",[[Int
1]]) ]
    [ (Int
1, [(Int -> Prp
P Int
k,Bool
False) | Int
k <- [Int
0..Int
n] ] ) ]

prisonGoal :: Form
prisonGoal :: Form
prisonGoal = Agent -> Form -> Form
K Agent
"1" (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
k | Int
k <- [Int
1..Int
n] ]

prisonAction :: ActionModelS5
prisonAction :: ActionModelS5
prisonAction = [(Int, (Form, PostCondition))]
-> [(Agent, Partition)] -> ActionModelS5
ActMS5 [(Int, (Form, PostCondition))]
actions [(Agent, Partition)]
actRels where
  p :: Int -> Form
p = Prp -> Form
PrpF (Prp -> Form) -> (Int -> Prp) -> Int -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Prp
P
  actions :: [(Int, (Form, PostCondition))]
actions =
    [ (Int
0, (Int -> Form
p Int
0      , [(Int -> Prp
P Int
0, Form
Bot), (Int -> Prp
P Int
1, Form
Top)]) ) -- interview 1 with light on
    , (Int
1, (Form -> Form
Neg (Int -> Form
p Int
0), [            (Int -> Prp
P Int
1, Form
Top)]) ) -- interview 1 with light off
    ]
    [(Int, (Form, PostCondition))]
-> [(Int, (Form, PostCondition))] -> [(Int, (Form, PostCondition))]
forall a. [a] -> [a] -> [a]
++
    [ (Int
k, (Form
Top, [(Int -> Prp
P Int
0, Int -> Form
p Int
k Form -> Form -> Form
`Impl` Int -> Form
p Int
0), (Int -> Prp
P Int
k, Int -> Form
p Int
0 Form -> Form -> Form
`Impl` Int -> Form
p Int
k)]) ) | Int
k <- [Int
2..Int
n] ] -- interview k
  actRels :: [(Agent, Partition)]
actRels = [ (Agent
"1", [[Int
0],[Int
1],[Int
2..Int
n]]) ]

prisonInterview :: Int -> MultipointedActionModelS5
prisonInterview :: Int -> MultipointedActionModelS5
prisonInterview Int
1 = (ActionModelS5
prisonAction, [Int
0,Int
1])
prisonInterview Int
k = (ActionModelS5
prisonAction, [Int
k])

data Story a b = Story a [b]

endOf :: (Update a b, Optimizable a) => Story a b -> a
endOf :: forall a b. (Update a b, Optimizable a) => Story a b -> a
endOf (Story a
start [b]
actions) =
  (a -> b -> a) -> a -> [b] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\a
cur b
a -> [Prp] -> a -> a
forall a. Optimizable a => [Prp] -> a -> a
optimize (a -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf a
start) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ a
cur a -> b -> a
forall a b. Update a b => a -> b -> a
`update` b
a) a
start [b]
actions

instance (Update a b, Optimizable a, TexAble a, TexAble b) => TexAble (Story a b) where
  tex :: Story a b -> Agent
tex (Story a
start [b]
actions) = Agent -> Agent
adjust (a -> Agent
forall a. TexAble a => a -> Agent
tex a
start) Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ a -> [b] -> Agent
forall {a} {t}.
(TexAble a, TexAble t, Optimizable t, Update t a) =>
t -> [a] -> Agent
loop a
start [b]
actions where
    adjust :: Agent -> Agent
adjust Agent
thing = Agent
" \\raisebox{-.5\\height}{ \\begin{adjustbox}{max height=4cm, max width=0.3\\linewidth} $ " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
thing Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" $ \\end{adjustbox} } "
    loop :: t -> [a] -> Agent
loop t
_       []     = Agent
""
    loop t
current (a
a:[a]
as) =
      let
        new :: t
new = [Prp] -> t -> t
forall a. Optimizable a => [Prp] -> a -> a
optimize (a -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf a
start) (t -> t) -> t -> t
forall a b. (a -> b) -> a -> b
$ t
current t -> a -> t
forall a b. Update a b => a -> b -> a
`update` a
a
      in
        Agent
" \\times " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent -> Agent
adjust (a -> Agent
forall a. TexAble a => a -> Agent
tex a
a) Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" = " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent -> Agent
adjust (t -> Agent
forall a. TexAble a => a -> Agent
tex t
new) Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"\\] \\[ " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ t -> [a] -> Agent
loop t
new [a]
as

prisonExpStory :: Story PointedModelS5 MultipointedActionModelS5
prisonExpStory :: Story PointedModelS5 MultipointedActionModelS5
prisonExpStory = PointedModelS5
-> [MultipointedActionModelS5]
-> Story PointedModelS5 MultipointedActionModelS5
forall a b. a -> [b] -> Story a b
Story (KripkeModelS5
prisonExpStart,Int
1) ((Int -> MultipointedActionModelS5)
-> [Int] -> [MultipointedActionModelS5]
forall a b. (a -> b) -> [a] -> [b]
map Int -> MultipointedActionModelS5
prisonInterview [Int
2,Int
1,Int
3,Int
1])

prisonSymStart :: MultipointedKnowScene
prisonSymStart :: MultipointedKnowScene
prisonSymStart = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS ((Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P [Int
0..Int
n]) Bdd
law [(Agent, [Prp])]
forall {a}. [(Agent, [a])]
obs, Bdd
actualStatesBdd) where
  law :: Bdd
law    = Form -> Bdd
boolBddOf ([Form] -> Form
Conj (Form -> Form
Neg Form
light Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
wasInterviewed Int
k | Int
k <- [Int
1..Int
n] ]))
  obs :: [(Agent, [a])]
obs    = [ (Agent
"1", []) ]
  actualStatesBdd :: Bdd
actualStatesBdd = Bdd
top

wasInterviewed, isNowInterviewed :: Int -> Form
wasInterviewed :: Int -> Form
wasInterviewed     = Prp -> Form
PrpF (Prp -> Form) -> (Int -> Prp) -> Int -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Prp
P
isNowInterviewed :: Int -> Form
isNowInterviewed Int
k = Prp -> Form
PrpF (Int -> Prp
P (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n))

lightSeenByOne :: Form
lightSeenByOne :: Form
lightSeenByOne  = Prp -> Form
PrpF (Int -> Prp
P (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n)))

prisonSymEvent :: KnowTransformer
prisonSymEvent :: KnowTransformer
prisonSymEvent = [Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer
KnTrf -- agent 1 is interviewed
  ((Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P ([Int] -> [Prp]) -> [Int] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [ Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
n | Int
k <- [Int
1..Int
n] ] [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+(Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n)] ) -- distinguish events
  ([Form] -> Form
Conj [ Int -> Form
isNowInterviewed Int
1 Form -> Form -> Form
`Impl` (Form
lightSeenByOne Form -> Form -> Form
`Equi` Form
light)
        , [Form] -> Form
Disj [ [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
isNowInterviewed Int
k Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
isNowInterviewed Int
l | Int
l <- [Int
1..Int
n], Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
k ] | Int
k <- [Int
1..Int
n]]
        ] )
  -- light might be switched and visits of the agents might be recorded
  ( [ (Int -> Prp
P Int
0, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$
          [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
isNowInterviewed Int
1 Form -> Form -> Form
`Impl` Form
Bot -- 1 turns off the light
               Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ [Form] -> Form
Conj [Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
wasInterviewed Int
k, Int -> Form
isNowInterviewed Int
k] Form -> Form -> Form
`Impl` Form
Top
                          , [Form] -> Form
Conj [      Int -> Form
wasInterviewed Int
k, Int -> Form
isNowInterviewed Int
k] Form -> Form -> Form
`Impl` Form
light ]
                        | Int
k <- [Int
2..Int
n] ])
  , (Int -> Prp
P Int
1, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Disj [Int -> Form
wasInterviewed Int
1, [Form] -> Form
Conj [           Int -> Form
isNowInterviewed Int
1]])
  ]
  [(Prp, Bdd)] -> [(Prp, Bdd)] -> [(Prp, Bdd)]
forall a. [a] -> [a] -> [a]
++
  [ (Int -> Prp
P Int
k, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Disj [Int -> Form
wasInterviewed Int
k, [Form] -> Form
Conj [Form -> Form
Neg Form
light, Int -> Form
isNowInterviewed Int
k]])
  | Int
k <- [Int
2..Int
n] ] )
  -- agent 1 observes whether they are interviewed, and if so, also observes the light
  [ (Agent
"1", let (PrpF Prp
px, PrpF Prp
py) = (Int -> Form
isNowInterviewed Int
1, Form
lightSeenByOne) in [Prp
px, Prp
py]) ]

prisonSymInterview :: Int -> MultipointedEvent
prisonSymInterview :: Int -> MultipointedEvent
prisonSymInterview Int
k = (KnowTransformer
prisonSymEvent, Form -> Bdd
boolBddOf (Int -> Form
isNowInterviewed Int
k))

prisonSymStory :: Story MultipointedKnowScene MultipointedEvent
prisonSymStory :: Story MultipointedKnowScene MultipointedEvent
prisonSymStory = MultipointedKnowScene
-> [MultipointedEvent]
-> Story MultipointedKnowScene MultipointedEvent
forall a b. a -> [b] -> Story a b
Story MultipointedKnowScene
prisonSymStart ((Int -> MultipointedEvent) -> [Int] -> [MultipointedEvent]
forall a b. (a -> b) -> [a] -> [b]
map Int -> MultipointedEvent
prisonSymInterview [Int
2,Int
1,Int
3,Int
1])