module SMCDEL.Examples.DrinkLogic where

import SMCDEL.Language
import SMCDEL.Symbolic.S5

thirstyScene :: Int -> KnowScene
thirstyScene :: Int -> KnowScene
thirstyScene Int
n = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Int -> Prp
P Int
1..Int -> Prp
P Int
n] (Form -> Bdd
boolBddOf Form
Top) [ (Int -> Agent
forall a. Show a => a -> Agent
show Int
i,[Int -> Prp
P Int
i]) | Int
i <- [Int
1..Int
n] ], [Int -> Prp
P Int
1..Int -> Prp
P Int
n])

thirstyF :: Int -> Form
thirstyF :: Int -> Form
thirstyF Int
n = [Form] -> Form
Conj [ [Form] -> Form
Conj [ Int -> Form
forall {a}. Show a => a -> Form
doesNotKnow Int
k | Int
k <- [Int
1..Int
n] ]
                  , [Form] -> Form -> Form
pubAnnounceStack [ Int -> Form
forall {a}. Show a => a -> Form
doesNotKnow Int
i | Int
i<-[Int
1..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] ] (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K (Int -> Agent
forall a. Show a => a -> Agent
show Int
n) Form
allWantBeer ]
  where
    allWantBeer :: Form
allWantBeer   = [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] ]
    doesNotKnow :: a -> Form
doesNotKnow a
i = Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
Kw (a -> Agent
forall a. Show a => a -> Agent
show a
i) Form
allWantBeer

thirstyCheck :: Int -> Bool
thirstyCheck :: Int -> Bool
thirstyCheck Int
n = KnowScene -> Form -> Bool
evalViaBdd (Int -> KnowScene
thirstyScene Int
n) (Int -> Form
thirstyF Int
n)