module ModelsVocab where
import List
--import Test.QuickCheck
type Rel a = [(a,a)]
sameR :: Ord a => Rel a -> Rel a -> Bool
sameR r s = sort (nub r) == sort (nub s)
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 ]
containedIn :: Eq a => [a] -> [a] -> Bool
containedIn xs ys = all (\ x -> elem x ys) xs
euclR :: Eq a => Rel a -> Bool
euclR r = (cnv r @@ r) `containedIn` r
serialR :: Eq a => Rel a -> Bool
serialR r =
all (not.null)
(map (\ (x,y) -> [ v | (u,v) <- r, y == u]) r)
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
isKD45 :: Eq a => Rel a -> Bool
isKD45 r = transR r && serialR r && euclR r
data Agent = Ag Int deriving (Eq,Ord)
a,alice, b,bob, c,carol, d,dave, e,ernie :: Agent
a = Ag 0; alice = Ag 0
b = Ag 1; bob = Ag 1
c = Ag 2; carol = Ag 2
d = Ag 3; dave = Ag 3
e = Ag 4; ernie = Ag 4
instance Show Agent where
show (Ag 0) = "a"; show (Ag 1) = "b";
show (Ag 2) = "c"; show (Ag 3) = "d" ;
show (Ag 4) = "e";
show (Ag n) = 'a': show n
data Prp = P Int | Q Int | R Int deriving (Eq,Ord)
instance Show Prp 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
[state]
[Agent]
[Prp]
[(state,[Prp])]
[(Agent,state,state)]
[state] deriving (Eq,Show)
s5example :: EpistM Integer
s5example =
Mo [0..3]
[a,b,c]
[P 0, Q 0]
[(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 ag (Mo states agents _ val rels actual) =
[ (x,y) | (agent,x,y) <- rels, ag == agent ]
valuation :: EpistM a -> [(a,[Prp])]
valuation (Mo _ _ _ val _ _ ) = val
vocab :: EpistM a -> [Prp]
vocab (Mo _ _ voc _ _ _) = voc
valStat :: Eq a => a -> EpistM a -> [Prp]
valStat x (Mo states agents voc val rels actual)
= [y | (state,[y]) <- val, state == x ]
vcbSet :: Eq a => EpistM a -> [Prp]
vcbSet (Mo states agents voc val rels actual)
= nub ( [y | (states,[y]) <- val] )
actual :: EpistM a -> [a]
actual (Mo _ _ _ _ _ actual) = actual
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 voc val rels actual) =
show states :
show voc :
show val :
map show [ (ag, (rel2partition states) (rel ag m))
| ag <- agents ]
++
[show actual]
displayS5 :: (Ord a,Show a) => EpistM a -> IO()
displayS5 = putStrLn . unlines . showS5
initM :: [Agent] -> [Prp] -> EpistM Integer
initM ags props = (Mo worlds ags props 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
epsilon :: [Agent] -> EpistM Integer
epsilon ags = initM ags []
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) | (ag,x,y) <- r, ag `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 = rightS (genK r ags)
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 ++ (s@@s))) ri
where ri = nub (r ++ [(x,x) | x <- xs ])
prop_RtcRefl :: Ord a => [a] -> Rel a -> Bool
prop_RtcRefl xs r = reflR xs (rtc xs r)
prop_RtcTr :: Ord a => [a] -> Rel a -> Bool
prop_RtcTr xs r = transR (rtc xs r)
tc :: Ord a => Rel a -> Rel a
tc r = lfp (\ s -> (sort.nub) (s ++ (s @@ s))) r
prop_TcTr :: Ord a => Rel a -> Bool
prop_TcTr r = transR (tc 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
| Prp Prp
| Neg Form
| Conj [Form]
| Disj [Form]
| K Agent Form
| CK [Agent] Form
deriving (Eq,Ord)
p = Prp (P 0)
q = Prp (Q 0)
instance Show Form where
show Top = "T"
show (Prp 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
impl :: Form -> Form -> Form
impl form1 form2 = Disj [Neg form1, form2]
getPs :: Form -> [Prp]
getPs Top = []
getPs (Prp p) = [p]
getPs (Neg f) = getPs f
getPs (Conj fs) = (sort.nub.concat) (map getPs fs)
getPs (Disj fs) = (sort.nub.concat) (map getPs fs)
getPs (K agent f) = getPs f
getPs (CK agents f) = getPs 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
maybe_Not :: Maybe Bool -> Maybe Bool
maybe_Not Nothing = Nothing
maybe_Not (Just x) = Just (not x)
maybe_And :: [Maybe Bool] -> Maybe Bool
maybe_And [] = Just True
maybe_And (Nothing:xs) = Nothing
maybe_And ((Just True):xs) = maybe_And (xs)
maybe_And ((Just False):xs) = Just False
maybe_Or :: [Maybe Bool] -> Maybe Bool
maybe_Or [] = Just False
maybe_Or (Nothing:xs) = Nothing
maybe_Or ((Just True):xs) = Just True
maybe_Or ((Just False):xs) = maybe_Or (xs)
maybe_All:: (Maybe Bool -> Maybe Bool) -> [Maybe Bool] ->
Maybe Bool
maybe_All f = (maybe_And). map f
maybe_Any :: (Maybe Bool -> Maybe Bool) -> [Maybe Bool] ->
Maybe Bool
maybe_Any f = (maybe_Or). map f
isTrueAtMayb :: Ord state =>
EpistM state -> state -> Form -> Maybe Bool
isTrueAtMayb m w Top = Just True
isTrueAtMayb
m@(Mo worlds agents voc val acc points) w (Prp p) =
if notElem p voc then Nothing else
if elem p (concat [props|(w',props) <- val, w'==w]) then
(Just True)
else Just False
isTrueAtMayb m w (Neg f) = maybe_Not (isTrueAtMayb m w f)
isTrueAtMayb m w (Conj fs) =
maybe_And (map (isTrueAtMayb m w) fs)
isTrueAtMayb m w (Disj fs) =
maybe_Or (map (isTrueAtMayb m w) fs)
isTrueAtMayb
m@(Mo worlds agents voc val acc points) w (K ag f) =
maybe_And (map (flip (isTrueAtMayb m) f)
(rightS (rel ag m) w))
isTrueAtMayb
m@(Mo worlds agents voc val acc points) w (CK ags f) =
maybe_And (map (flip (isTrueAtMayb m) f)
(commonAlts acc ags worlds w))
isTrue :: Ord state => EpistM state -> Form -> Maybe Bool
isTrue m@(Mo worlds agents voc val acc points) f =
maybe_And [isTrueAtMayb m s f | s <- points ]
upd_pa :: Ord state =>
EpistM state -> Form -> EpistM state
upd_pa m@(Mo states agents voc val rels actual) f =
(Mo states' agents voc val' rels' actual')
where
states' = [ s | s <- states, isTrueAtMayb m s f ==
Just True]
val' = [(s,p) | (s,p) <- val,
s `elem` states' ]
rels' = [(ag,x,y) | (ag,x,y) <- rels,
x `elem` states',
y `elem` states' ]
actual' = [ s | s <- actual, s `elem` states' ]
m0 = initM [a,b,c] [P 0,Q 0]
convert :: Eq state =>
EpistM state -> EpistM Integer
convert (Mo states agents voc val rels actual) =
Mo states' agents voc 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 voc val rel points) =
(Mo states' ags voc val' rel' points)
where
states' = closure rel ags points
val' = [(s,props) | (s,props) <- val,
elem s states' ]
rel' = [(ag,s,s') | (ag,s,s') <- rel,
elem s states',
elem s' 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 ]
type State = Integer
sameVal :: (Eq a,Eq b) => [(a,b)] -> a -> a -> Bool
sameVal val w1 w2 = apply val w1 == apply val w2
cf2part :: (Eq a) =>
[a] -> (a -> a -> Bool) -> [[a]]
cf2part [] r = []
cf2part (x:xs) r = xblock : cf2part rest r
where
(xblock,rest) = (x : filter (r x) xs,
filter (not . (r x)) xs)
initPartition :: Eq a => EpistM a -> [[a]]
initPartition (Mo states agents voc val rel actual) =
cf2part states (\ x y -> sameVal val x y)
bl :: Eq a => [[a]] -> a -> [a]
bl part x = head (filter (elem x) part)
accBlocks :: Eq a =>
EpistM a -> [[a]] -> a -> Agent -> [[a]]
accBlocks m@(Mo _ _ _ _ rel _) part s ag =
nub [ bl part y | (ag',x,y) <- rel,
ag' == ag, x == s ]
sameAB :: Ord a =>
EpistM a -> [[a]] -> a -> a -> Bool
sameAB m@(Mo states ags voc val rel actual) part s t =
and [ sort (accBlocks m part s ag)
== sort (accBlocks m part t ag) | ag <- ags ]
refineStep :: Ord a => EpistM a -> [[a]] -> [[a]]
refineStep m p = refineP m p p
where
refineP :: Ord a =>
EpistM a -> [[a]] -> [[a]] -> [[a]]
refineP m part [] = []
refineP m part (bl:blocks) =
newblocks ++ (refineP m part blocks)
where
newblocks =
cf2part bl (\ x y -> sameAB m part x y)
refine :: Ord a => EpistM a -> [[a]] -> [[a]]
refine m = lfp (refineStep m)
minimalModel :: Ord a => EpistM a -> EpistM [a]
minimalModel m@(Mo states agents voc val rel actual) =
(Mo states' agents voc val' rel' actual')
where
states' = refine m (initPartition m)
f = bl states'
val' = (nub . sort)
(map (\ (x,y) -> (f x, y)) val)
rel' = (nub . sort)
(map (\ (x,y,z) -> (x, f y, f z)) rel)
actual' = map f actual
bisim :: Ord a => EpistM a -> EpistM State
bisim = convert . minimalModel . gsm