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)