module CAIA where import Data.List data Agent = A | B | C | D | E deriving (Eq,Ord,Enum) a,alice, b,bob, c,carol, d,dave, e,ernie :: Agent a = A; alice = A b = B; bob = B c = C; carol = C d = D; dave = D e = E; ernie = E instance Show Agent where show A = "a"; show B = "b"; show C = "c"; show D = "d"; show E = "e" data Prop = P Int | Q Int | R Int deriving (Eq,Ord) instance Show Prop where show (P 0) = "p"; show (P i) = "p" ++ show i show (Q 0) = "q"; show (Q i) = "q" ++ show i show (R 0) = "r"; show (R i) = "r" ++ show i data EpistM state = Mo { dom :: [state], agents :: [Agent], valuation :: [(state,[Prop])], rels :: [(Agent,state,state)], actual :: [state] } deriving (Eq,Show) exampleModel :: EpistM Integer exampleModel = Mo [0..3] [a..c] [(0,[]),(1,[P 0]),(2,[Q 0]),(3,[P 0, Q 0])] ([ (a,x,x) | x <- [0..3] ] ++ [ (b,x,x) | x <- [0..3] ] ++ [ (c,x,y) | x <- [0..3], y <- [0..3] ]) [1] type Rel a = [(a,a)] containedIn :: Eq a => [a] -> [a] -> Bool containedIn xs ys = all (\ x -> elem x ys) xs cnv :: Rel a -> Rel a cnv r = [ (y,x) | (x,y) <- r ] infixr 5 @@ (@@) :: Eq a => Rel a -> Rel a -> Rel a r @@ s = nub [ (x,z) | (x,y) <- r, (w,z) <- s, y == w ] reflR :: Eq a => [a] -> Rel a -> Bool reflR xs r = [(x,x) | x <- xs] `containedIn` r symmR :: Eq a => Rel a -> Bool symmR r = cnv r `containedIn` r transR :: Eq a => Rel a -> Bool transR r = (r @@ r) `containedIn` r isS5 :: Eq a => [a] -> Rel a -> Bool isS5 xs r = reflR xs r && transR r && symmR r rel :: Agent -> EpistM a -> Rel a rel a model = [ (x,y) | (b,x,y) <- rels model, a == b ] rel2partition :: Ord a => [a] -> Rel a -> [[a]] rel2partition [] r = [] rel2partition (x:xs) r = xclass : rel2partition (xs\\xclass) r where xclass = x : [ y | y <- xs, (x,y) `elem` r ] showS5 :: (Ord a,Show a) => EpistM a -> [String] showS5 m = show (dom m) : show (valuation m) : map show [ (a,(rel2partition (dom m)) (rel a m)) | a <- (agents m)] ++ [show (actual m)] displayS5 :: (Ord a,Show a) => EpistM a -> IO() displayS5 = putStrLn . unlines . showS5 initM :: [Agent] -> [Prop] -> EpistM Integer initM ags props = (Mo worlds ags val accs points) where worlds = [0..(2^k-1)] k = length props val = zip worlds (sortL (powerList props)) accs = [ (ag,st1,st2) | ag <- ags, st1 <- worlds, st2 <- worlds ] points = worlds powerList :: [a] -> [[a]] powerList [] = [[]] powerList (x:xs) = (powerList xs) ++ (map (x:) (powerList xs)) sortL :: Ord a => [[a]] -> [[a]] sortL = sortBy (\ xs ys -> if length xs < length ys then LT else if length xs > length ys then GT else compare xs ys) lfp :: Eq a => (a -> a) -> a -> a lfp f x | x == f x = x | otherwise = lfp f (f x) rtc :: Ord a => [a] -> Rel a -> Rel a rtc xs r = lfp (\ s -> (sort.nub) (s ++ (r@@s))) i where i = [ (x,x) | x <- xs ] data Form = Top | Prop Prop | Neg Form | Conj [Form] | Disj [Form] | K EE Form | PA Form Form | PC [(Prop,Form)] Form deriving (Eq,Ord) data EE = Agent Agent | Test Form | Cmp EE EE | Sum [EE] | Star EE deriving (Eq,Ord) p = Prop (P 0) q = Prop (Q 0) instance Show Form where show Top = "T" show (Prop p) = show p show (Neg f) = '-':(show f) show (Conj fs) = '&': show fs show (Disj fs) = 'v': show fs show (K e f) = '[':show e ++"]"++show f show (PA f1 f2) = '[':'!': show f1 ++"]"++show f2 show (PC s f) = show s ++ show f instance Show EE where show (Agent a) = show a show (Test f) = '?': show f show (Cmp e1 e2) = show e1 ++ ";" ++ show e2 show (Sum es) = 'U': show es show (Star e) = '(': show e ++ ")*" ck :: [Agent] -> Form -> Form ck ags f = K (Star (Sum [Agent a | a <- ags])) f apply :: Eq a => [(a,b)] -> a -> b apply [] _ = error "argument not in list" apply ((x,z):xs) y | x == y = z | otherwise = apply xs y rightS :: Ord a => a -> Rel a -> [a] rightS x r = (sort.nub) [ z | (y,z) <- r, x == y ] isTrueAt :: Ord state => EpistM state -> state -> Form -> Bool isTrueAt m w Top = True isTrueAt m w (Prop p) = p `elem` (concat [ ps | (w',ps) <- valuation m, w'==w]) isTrueAt m w (Neg f) = not (isTrueAt m w f) isTrueAt m w (Conj fs) = and (map (isTrueAt m w) fs) isTrueAt m w (Disj fs) = or (map (isTrueAt m w) fs) isTrueAt m w (K e f) = and (map (flip (isTrueAt m) f) (rightS w (evalEE m e))) isTrueAt m w (PA f1 f2) = not (isTrueAt m w f1) || isTrueAt m' w f2 where m' = upd_pa m f1 isTrueAt m w (PC s f) = isTrueAt (upd_pc m s) w f evalEE :: Ord state => EpistM state -> EE -> Rel state evalEE m (Agent a) = rel a m evalEE m (Test f) = [(w,w) | w <- dom m, isTrueAt m w f] evalEE m (Cmp e1 e2) = (evalEE m e1) @@ (evalEE m e2) evalEE m (Sum (es)) = (sort.nub) (concat (map (evalEE m) es)) evalEE m (Star e) = rtc (dom m) (evalEE m e) test1 = isTrueAt (initM [a..c] [P 0]) 0 (ck [a..c] (Neg (K (Agent a) p))) isTrue :: Ord state => EpistM state -> Form -> Bool isTrue m f = and [ isTrueAt m s f | s <- actual m ] test2 = isTrue (initM [a..c] [P 0]) (ck [a..c] (Neg (K (Agent a) p))) upd_pa :: Ord state => EpistM state -> Form -> EpistM state upd_pa m@(Mo states agents val rels actual) f = (Mo states' agents val' rels' actual') where states' = [ s | s <- states, isTrueAt m s f ] val' = [ (s,p) | (s,p) <- val, s `elem` states' ] rels' = [ (a,x,y) | (a,x,y) <- rels, x `elem` states', y `elem` states' ] actual' = [ s | s <- actual, s `elem` states' ] type Subst = [(Prop,Form)] upd_pc :: Ord state => EpistM state -> Subst -> EpistM state upd_pc m@(Mo worlds agents val acc points) subst = (Mo worlds agents val' acc points) where val' = [ (w,[p | p <- ps, isTrueAt m w (liftS subst p)]) | w <- worlds ] ps = (sort.nub) (concat (map snd val)) liftS :: Subst -> Prop -> Form liftS [] p = Prop p liftS ((x,z):xs) y | x == y = z | otherwise = liftS xs y m0 = initM [a..c] [P 0,Q 0] convert :: Eq state => EpistM state -> EpistM Integer convert (Mo states agents val rels actual) = Mo states' agents val' rels' actual' where states' = map f states val' = map (\ (x,y) -> (f x,y)) val rels' = map (\ (x,y,z) -> (x,f y,f z)) rels actual' = map f actual f = apply (zip states [0..]) gsm :: Ord state => EpistM state -> EpistM state gsm (Mo states ags val rel points) = Mo states' ags val' rel' points where states' = closure rel ags points val' = [(s,ps) | (s,ps) <- val, s `elem` states' ] rel' = [(ag,s,s') | (ag,s,s') <- rel, s `elem` states', s' `elem` states' ] closure :: Ord state => [(Agent,state,state)] -> [Agent] -> [state] -> [state] closure rel agents xs = lfp f xs where f = \ ys -> (nub.sort) (ys ++ (expand rel agents ys)) expand :: Ord state => [(Agent,state,state)] -> [Agent] -> [state] -> [state] expand rel agents ys = (nub.sort.concat) [ alternatives rel ag state | ag <- agents, state <- ys ] alternatives :: Eq state => [(Agent,state,state)] -> Agent -> state -> [state] alternatives rel ag current = [ s' | (a,s,s') <- rel, a == ag, s == current ] p1, p2, p3, p4 :: Form p1 = Prop (P 1); p2 = Prop (P 2) p3 = Prop (P 3); p4 = Prop (P 4) computeAcc :: Agent -> [Integer] -> [Prop] -> [(Integer,[Prop])] -> [(Agent,Integer,Integer)] computeAcc ag states props val = [ (ag,x,y) | x <- states, y <- states, apply val x \\ props == apply val y \\ props ] initMuddy :: EpistM Integer initMuddy = Mo states [a..d] valuation (computeAcc a states [P 1] valuation ++ computeAcc b states [P 2] valuation ++ computeAcc c states [P 3] valuation ++ computeAcc d states [P 4] valuation) [7] where states = [0..15] valuation = zip states (powerList [P 1,P 2,P 3,P 4]) m1 = convert (upd_pa initMuddy (Disj [p1,p2,p3,p4])) aK = Disj [K (Agent a) p1, K (Agent a) (Neg p1)] bK = Disj [K (Agent b) p2, K (Agent b) (Neg p2)] cK = Disj [K (Agent c) p3, K (Agent c) (Neg p3)] dK = Disj [K (Agent d) p4, K (Agent d) (Neg p4)] m2 = convert (upd_pa m1 (Conj [Neg aK,Neg bK,Neg cK,Neg dK])) m3 = convert (upd_pa m2 (Conj [Neg aK,Neg bK,Neg cK,Neg dK])) m4 = convert (upd_pa m3 (Conj [Neg aK, bK, cK, dK]))