module RPAU
where
import List
import HFKR
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
s5example :: EpistM Integer
s5example =
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]
dom :: EpistM a -> [a]
dom (Mo states _ _ _ _) = states
rel :: Agent -> EpistM a -> Rel a
rel a (Mo states agents val rels actual) =
[ (x,y) | (agent,x,y) <- rels, a == agent ]
rel2partition :: Ord a => [a] -> Rel a -> [[a]]
rel2partition [] r = []
rel2partition (x:xs) r =
xclass : rel2partition (xs \\ xclass) r
where
xclass = x : [ y | y <- xs, elem (x,y) r ]
showS5 :: (Ord a,Show a) => EpistM a -> [String]
showS5 m@(Mo states agents val rels actual) =
show states :
show val :
map show [ (a, (rel2partition states) (rel a m))
| a <- agents ]
++
[show actual]
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)
genK :: Ord state => [(Agent,state,state)]
-> [Agent] -> Rel state
genK r ags = [ (x,y) | (a,x,y) <- r, a `elem` ags ]
rightS :: Ord a => Rel a -> a -> [a]
rightS r x = (sort.nub) [ z | (y,z) <- r, x == y ]
genAlts :: Ord state => [(Agent,state,state)]
-> [Agent] -> state -> [state]
genAlts r ags s = rightS (genK r ags) s
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 ]
tc :: Ord a => Rel a -> Rel a
tc r = lfp (\ s -> (sort.nub) (s ++ (r @@ s))) r
commonK :: Ord state => [(Agent,state,state)]
-> [Agent] -> [state] -> Rel state
commonK r ags xs = rtc xs (genK r ags)
commonAlts :: Ord state => [(Agent,state,state)]
-> [Agent] -> [state] -> state -> [state]
commonAlts r ags xs s = rightS (commonK r ags xs) s
data Form = Top
| Prop Prop
| Neg Form
| Conj [Form]
| Disj [Form]
| K Agent Form
| CK [Agent] Form
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 agent f) = '[':show agent++"]"++show f
show (CK agents f) = 'C': show agents ++ show 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
{-
From here, all functions that depend on isTrueAt
have been commented out.
To get them back, after you have implemented isTrueAt,
just remove all occurrences of {- and -}
-}
{-
test1 = isTrueAt
(initM [a..c] [P 0]) 0
(CK [a..c] (Neg (K a p)))
-}
{-
isTrue :: Ord state => EpistM state -> Form -> Bool
isTrue m@(Mo worlds agents val acc points) f =
and [ isTrueAt m s f | s <- points ]
-}
{-
test2 = isTrue
(initM [a..c] [P 0])
(CK [a..c] (Neg (K 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' ]
-}
m0 = initM [a..c] [P 0,Q 0]
{-
HERE is your homework: replace the ... by your definitions
and remove comment brackets
isTrueAt :: Ord state =>
EpistM state -> state -> Form -> Bool
isTrueAt m w Top = ...
isTrueAt
m@(Mo worlds agents val acc points) w (Prop p) = ...
isTrueAt m w (Neg f) = ...
isTrueAt m w (Conj fs) = ...
isTrueAt m w (Disj fs) = ...
isTrueAt
m@(Mo worlds agents val acc points) w (K ag f) =
...
isTrueAt
m@(Mo worlds agents val acc points) w (CK ags f) =
...
-}