module SMCDEL.Examples.MuddyChildren where
import Data.List
import Data.Maybe (fromJust)
import Data.Map.Strict (fromList)
import SMCDEL.Internal.Help (seteq)
import SMCDEL.Language
import SMCDEL.Symbolic.S5
import qualified SMCDEL.Symbolic.K
import qualified SMCDEL.Explicit.K
mudScnInit :: Int -> Int -> KnowScene
mudScnInit :: World -> World -> KnowScene
mudScnInit World
n World
m = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
vocab Bdd
law [(Agent, [Prp])]
obs, [Prp]
actual) where
vocab :: [Prp]
vocab = [World -> Prp
P World
1 .. World -> Prp
P World
n]
law :: Bdd
law = Form -> Bdd
boolBddOf Form
Top
obs :: [(Agent, [Prp])]
obs = [ (World -> Agent
forall a. Show a => a -> Agent
show World
i, Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) [Prp]
vocab) | World
i <- [World
1..World
n] ]
actual :: [Prp]
actual = [World -> Prp
P World
1 .. World -> Prp
P World
m]
myMudScnInit :: KnowScene
myMudScnInit :: KnowScene
myMudScnInit = World -> World -> KnowScene
mudScnInit World
3 World
3
knows :: Int -> Form
knows :: World -> Form
knows World
i = Agent -> Form -> Form
Kw (World -> Agent
forall a. Show a => a -> Agent
show World
i) (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ World -> Prp
P World
i)
nobodyknows :: Int -> Form
nobodyknows :: World -> Form
nobodyknows World
n = [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ World -> Form
knows World
i | World
i <- [World
1..World
n] ]
father :: Int -> Form
father :: World -> Form
father World
n = [Form] -> Form
Disj ((Prp -> Form) -> [Prp] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Form
PrpF [World -> Prp
P World
1 .. World -> Prp
P World
n])
mudScn0 :: KnowScene
mudScn0 :: KnowScene
mudScn0 = KnowScene -> Form -> KnowScene
forall a b. Update a b => a -> b -> a
update KnowScene
myMudScnInit (World -> Form
father World
3)
mudScn1 :: KnowScene
mudScn1 :: KnowScene
mudScn1 = KnowScene -> Form -> KnowScene
forall a b. Update a b => a -> b -> a
update KnowScene
mudScn0 (World -> Form
nobodyknows World
3)
mudScn2 :: KnowScene
mudKns2 :: KnowStruct
mudScn2 :: KnowScene
mudScn2@(KnowStruct
mudKns2,[Prp]
_) = KnowScene -> Form -> KnowScene
forall a b. Update a b => a -> b -> a
update KnowScene
mudScn1 (World -> Form
nobodyknows World
3)
empty :: Int -> KnowScene
empty :: World -> KnowScene
empty World
n = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [] (Form -> Bdd
boolBddOf Form
Top) [(Agent, [Prp])]
forall {a}. [(Agent, [a])]
obs,[]) where
obs :: [(Agent, [a])]
obs = [ (World -> Agent
forall a. Show a => a -> Agent
show World
i, []) | World
i <- [World
1..World
n] ]
buildMC :: Int -> Int -> Event
buildMC :: World -> World -> Event
buildMC World
n World
m = (([Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer)
-> [Prp] -> Form -> [(Agent, [Prp])] -> KnowTransformer
noChange [Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer
KnTrf [Prp]
vocab Form
Top [(Agent, [Prp])]
obs, (World -> Prp) -> [World] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map World -> Prp
P [World
1..World
m]) where
obs :: [(Agent, [Prp])]
obs = [ (World -> Agent
forall a. Show a => a -> Agent
show World
i, Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) [Prp]
vocab) | World
i <- [World
1..World
n] ]
vocab :: [Prp]
vocab = (World -> Prp) -> [World] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map World -> Prp
P [World
1..World
n]
buildResult :: KnowScene
buildResult :: KnowScene
buildResult = World -> KnowScene
empty World
3 KnowScene -> Event -> KnowScene
forall a b. Update a b => a -> b -> a
`update` World -> World -> Event
buildMC World
3 World
3
mudGenKrpInit :: Int -> Int -> SMCDEL.Explicit.K.PointedModel
mudGenKrpInit :: World -> World -> PointedModel
mudGenKrpInit World
n World
m = (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
SMCDEL.Explicit.K.KrM (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel)
-> Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
forall a b. (a -> b) -> a -> b
$ [(World, (Map Prp Bool, Map Agent [World]))]
-> Map World (Map Prp Bool, Map Agent [World])
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(World, (Map Prp Bool, Map Agent [World]))]
wlist, World
cur) where
wlist :: [(World, (Map Prp Bool, Map Agent [World]))]
wlist = [ (World
w, ([(Prp, Bool)] -> Map Prp Bool
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([[(Prp, Bool)]]
vals [[(Prp, Bool)]] -> World -> [(Prp, Bool)]
forall a. HasCallStack => [a] -> World -> a
!! World
w), [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(Agent, [World])] -> Map Agent [World])
-> [(Agent, [World])] -> Map Agent [World]
forall a b. (a -> b) -> a -> b
$ World -> [(Agent, [World])]
relFor World
w)) | World
w <- [World]
ws ]
ws :: [World]
ws = [World
0..(World
2World -> World -> World
forall a b. (Num a, Integral b) => a -> b -> a
^World
nWorld -> World -> World
forall a. Num a => a -> a -> a
-World
1)]
vals :: [[(Prp, Bool)]]
vals = ([(Prp, Bool)] -> [(Prp, Bool)])
-> [[(Prp, Bool)]] -> [[(Prp, Bool)]]
forall a b. (a -> b) -> [a] -> [b]
map [(Prp, Bool)] -> [(Prp, Bool)]
forall a. Ord a => [a] -> [a]
sort (([[(Prp, Bool)]] -> Prp -> [[(Prp, Bool)]])
-> [[(Prp, Bool)]] -> [Prp] -> [[(Prp, Bool)]]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [[(Prp, Bool)]] -> Prp -> [[(Prp, Bool)]]
forall {a}. [[(a, Bool)]] -> a -> [[(a, Bool)]]
buildTable [[]] [World -> Prp
P World
k | World
k<- [World
1..World
n]])
buildTable :: [[(a, Bool)]] -> a -> [[(a, Bool)]]
buildTable [[(a, Bool)]]
partrows a
p = [ (a
p,Bool
v)(a, Bool) -> [(a, Bool)] -> [(a, Bool)]
forall a. a -> [a] -> [a]
:[(a, Bool)]
pr | Bool
v <-[Bool
True,Bool
False], [(a, Bool)]
pr <- [[(a, Bool)]]
partrows ]
relFor :: World -> [(Agent, [World])]
relFor World
w = [ (World -> Agent
forall a. Show a => a -> Agent
show World
i, World -> World -> [World]
seesFrom World
i World
w) | World
i <- [World
1..World
n] ]
seesFrom :: World -> World -> [World]
seesFrom World
i World
w = (World -> Bool) -> [World] -> [World]
forall a. (a -> Bool) -> [a] -> [a]
filter (\World
v -> World -> [(Prp, Bool)] -> [(Prp, Bool)] -> Bool
samefor World
i ([[(Prp, Bool)]]
vals [[(Prp, Bool)]] -> World -> [(Prp, Bool)]
forall a. HasCallStack => [a] -> World -> a
!! World
w) ([[(Prp, Bool)]]
vals [[(Prp, Bool)]] -> World -> [(Prp, Bool)]
forall a. HasCallStack => [a] -> World -> a
!! World
v)) [World]
ws
samefor :: World -> [(Prp, Bool)] -> [(Prp, Bool)] -> Bool
samefor World
i [(Prp, Bool)]
ps [(Prp, Bool)]
qs = [Prp] -> [Prp] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
seteq (Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) (((Prp, Bool) -> Prp) -> [(Prp, Bool)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst ([(Prp, Bool)] -> [Prp]) -> [(Prp, Bool)] -> [Prp]
forall a b. (a -> b) -> a -> b
$ ((Prp, Bool) -> Bool) -> [(Prp, Bool)] -> [(Prp, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp, Bool) -> Bool
forall a b. (a, b) -> b
snd [(Prp, Bool)]
ps)) (Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) (((Prp, Bool) -> Prp) -> [(Prp, Bool)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst ([(Prp, Bool)] -> [Prp]) -> [(Prp, Bool)] -> [Prp]
forall a b. (a -> b) -> a -> b
$ ((Prp, Bool) -> Bool) -> [(Prp, Bool)] -> [(Prp, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp, Bool) -> Bool
forall a b. (a, b) -> b
snd [(Prp, Bool)]
qs))
cur :: World
cur = Maybe World -> World
forall a. HasCallStack => Maybe a -> a
fromJust ([(Prp, Bool)] -> [[(Prp, Bool)]] -> Maybe World
forall a. Eq a => a -> [a] -> Maybe World
elemIndex [(Prp, Bool)]
curVal [[(Prp, Bool)]]
vals)
curVal :: [(Prp, Bool)]
curVal = [(Prp, Bool)] -> [(Prp, Bool)]
forall a. Ord a => [a] -> [a]
sort ([(Prp, Bool)] -> [(Prp, Bool)]) -> [(Prp, Bool)] -> [(Prp, Bool)]
forall a b. (a -> b) -> a -> b
$ [(Prp
p,Bool
True) | Prp
p <- [World -> Prp
P World
1 .. World -> Prp
P World
m]] [(Prp, Bool)] -> [(Prp, Bool)] -> [(Prp, Bool)]
forall a. [a] -> [a] -> [a]
++ [(Prp
p,Bool
True) | Prp
p <- [World -> Prp
P (World
mWorld -> World -> World
forall a. Num a => a -> a -> a
+World
1) .. World -> Prp
P World
n]]
myMudGenKrpInit :: SMCDEL.Explicit.K.PointedModel
myMudGenKrpInit :: PointedModel
myMudGenKrpInit = World -> World -> PointedModel
mudGenKrpInit World
3 World
3
mudBelScnInit :: Int -> Int -> SMCDEL.Symbolic.K.BelScene
mudBelScnInit :: World -> World -> BelScene
mudBelScnInit World
n World
m = ([Prp] -> Bdd -> Map Agent RelBDD -> BelStruct
SMCDEL.Symbolic.K.BlS [Prp]
vocab Bdd
law Map Agent RelBDD
obs, [Prp]
actual) where
vocab :: [Prp]
vocab = [World -> Prp
P World
1 .. World -> Prp
P World
n]
law :: Bdd
law = Form -> Bdd
boolBddOf Form
Top
obs :: Map Agent RelBDD
obs = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(World -> Agent
forall a. Show a => a -> Agent
show World
i, [Prp] -> RelBDD
SMCDEL.Symbolic.K.allsamebdd ([Prp] -> RelBDD) -> [Prp] -> RelBDD
forall a b. (a -> b) -> a -> b
$ Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete (World -> Prp
P World
i) [Prp]
vocab) | World
i <- [World
1..World
n]]
actual :: [Prp]
actual = [World -> Prp
P World
1 .. World -> Prp
P World
m]
myMudBelScnInit :: SMCDEL.Symbolic.K.BelScene
myMudBelScnInit :: BelScene
myMudBelScnInit = World -> World -> BelScene
mudBelScnInit World
3 World
3