{-# LANGUAGE FlexibleInstances, TupleSections #-}

{- |
Converting between Kripke Models and Belief Structures
-}

module SMCDEL.Translations.K where

import Data.HasCacBDD hiding (Top,Bot)
import Data.List ((\\),elemIndex,nub,sort)
import Data.Maybe (fromJust)
import Data.Map.Strict ((!))
import qualified Data.Map.Strict as M

import SMCDEL.Language
import SMCDEL.Explicit.S5 (worldsOf)
import SMCDEL.Explicit.K
import SMCDEL.Internal.Help (apply,powerset,groupSortWith)
import SMCDEL.Symbolic.K
import SMCDEL.Symbolic.S5 (boolBddOf)
import SMCDEL.Translations.S5 (booloutof)
import SMCDEL.Other.BDD2Form

-- | Convert a belief scene to a pointed Kripke model.
blsToKripke :: BelScene -> PointedModel
blsToKripke :: BelScene -> PointedModel
blsToKripke (f :: BelStruct
f@(BlS [Prp]
_ Bdd
_ Map Agent RelBDD
obdds), [Prp]
curs) = (KripkeModel
m, World
cur) where
  links :: [([Prp], World)]
links = [[Prp]] -> [World] -> [([Prp], World)]
forall a b. [a] -> [b] -> [(a, b)]
zip (BelStruct -> [[Prp]]
statesOf BelStruct
f) [World
0..]
  m :: KripkeModel
m = Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
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
M.fromList
    [ (World
w, ( [(Prp, Bool)] -> Map Prp Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Prp
p, Prp
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
s) | Prp
p <- BelStruct -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf BelStruct
f]
          , [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent
a, ([Prp] -> World) -> [[Prp]] -> [World]
forall a b. (a -> b) -> [a] -> [b]
map ([([Prp], World)] -> [Prp] -> World
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [([Prp], World)]
links) ([[Prp]] -> [World]) -> [[Prp]] -> [World]
forall a b. (a -> b) -> a -> b
$ [Prp] -> Agent -> [[Prp]]
reachFromFor [Prp]
s Agent
a) | Agent
a <- BelStruct -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf BelStruct
f] ) )
    | ([Prp]
s,World
w) <- [([Prp], World)]
links ]
  reachFromFor :: [Prp] -> Agent -> [[Prp]]
reachFromFor [Prp]
s Agent
a = ([Prp] -> Bool) -> [[Prp]] -> [[Prp]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\[Prp]
t -> [Prp] -> RelBDD -> Bool
forall a. TagBdd a => [Prp] -> Tagged a Bdd -> Bool
tagBddEval ([Prp] -> [Prp]
mv [Prp]
s [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp] -> [Prp]
cp [Prp]
t) (Map Agent RelBDD
obdds Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
a)) (BelStruct -> [[Prp]]
statesOf BelStruct
f)
  cur :: World
cur = Maybe World -> World
forall a. HasCallStack => Maybe a -> a
fromJust ([Prp] -> [([Prp], World)] -> Maybe World
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [Prp]
curs [([Prp], World)]
links)

kripkeToBls :: PointedModel -> BelScene
kripkeToBls :: PointedModel -> BelScene
kripkeToBls pm :: PointedModel
pm@(KripkeModel
m,World
_) | KripkeModel -> Bool
distinctVal KripkeModel
m = PointedModel -> BelScene
kripkeToBlsUnsafe PointedModel
pm
                     | Bool
otherwise     = PointedModel -> BelScene
kripkeToBlsUnsafe (PointedModel -> PointedModel
ensureDistinctVal PointedModel
pm)

kripkeToBlsUnsafe :: PointedModel -> BelScene
kripkeToBlsUnsafe :: PointedModel -> BelScene
kripkeToBlsUnsafe (KripkeModel
m, World
cur) = ([Prp] -> Bdd -> Map Agent RelBDD -> BelStruct
BlS [Prp]
vocab Bdd
lawbdd Map Agent RelBDD
obdds, KripkeModel -> World -> [Prp]
truthsInAt KripkeModel
m World
cur) where
  vocab :: [Prp]
vocab  = KripkeModel -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KripkeModel
m
  lawbdd :: Bdd
lawbdd = [Bdd] -> Bdd
disSet [ [Prp] -> [Prp] -> Bdd
booloutof (KripkeModel -> World -> [Prp]
truthsInAt KripkeModel
m World
w) [Prp]
vocab | World
w <- KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
m ]
  obdds  :: M.Map Agent RelBDD
  obdds :: Map Agent RelBDD
obdds  = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Agent
i, Bdd -> Bdd -> Bdd
restrictLaw (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Agent -> KripkeModel -> RelBDD
relBddOfIn Agent
i KripkeModel
m Tagged Dubbel (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b.
Tagged Dubbel (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> RelBDD
mvBdd Bdd
lawbdd Tagged Dubbel (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b.
Tagged Dubbel (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bdd -> RelBDD
cpBdd Bdd
lawbdd)) | Agent
i <- [Agent]
agents ]
  agents :: [Agent]
agents = KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModel
m

ensureDistinctVal :: PointedModel -> PointedModel
ensureDistinctVal :: PointedModel -> PointedModel
ensureDistinctVal (krm :: KripkeModel
krm@(KrM Map World (Map Prp Bool, Map Agent [World])
m), World
cur) = if KripkeModel -> Bool
distinctVal KripkeModel
krm then (KripkeModel
krm,World
cur) else (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
newM,World
cur) where
  sameVals :: [[World]]
sameVals = (World -> [Prp]) -> [World] -> [[World]]
forall a b. (Eq a, Ord b) => (a -> b) -> [a] -> [[a]]
groupSortWith (KripkeModel -> World -> [Prp]
truthsInAt KripkeModel
krm) (KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
krm)
  indexOf :: World -> World
indexOf World
w = let k :: World
k = Maybe World -> World
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe World -> World) -> Maybe World -> World
forall a b. (a -> b) -> a -> b
$ World -> [World] -> Maybe World
forall a. Eq a => a -> [a] -> Maybe World
elemIndex World
w ([[World]] -> [World]
forall a. HasCallStack => [a] -> a
head ([[World]] -> [World]) -> [[World]] -> [World]
forall a b. (a -> b) -> a -> b
$ ([World] -> Bool) -> [[World]] -> [[World]]
forall a. (a -> Bool) -> [a] -> [a]
filter (World -> [World] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem World
w) [[World]]
sameVals) in World
k
  numAddProps :: World
numAddProps = Double -> World
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Double -> World) -> Double -> World
forall a b. (a -> b) -> a -> b
$ Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase (Double
2::Double) (World -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (World -> Double) -> World -> Double
forall a b. (a -> b) -> a -> b
$ [World] -> World
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (([World] -> World) -> [[World]] -> [World]
forall a b. (a -> b) -> [a] -> [b]
map [World] -> World
forall a. [a] -> World
forall (t :: * -> *) a. Foldable t => t a -> World
length [[World]]
sameVals) World -> World -> World
forall a. Num a => a -> a -> a
+ World
1)
  addProps :: [Prp]
addProps = World -> [Prp] -> [Prp]
forall a. World -> [a] -> [a]
take World
numAddProps [[Prp] -> Prp
freshp (KripkeModel -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KripkeModel
krm) ..]
  addValForIndex :: World -> Map Prp Bool
addValForIndex World
k = [(Prp, Bool)] -> Map Prp Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Prp
p, Prp
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([[Prp]] -> [[Prp]]
forall a. [a] -> [a]
reverse ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
addProps) [[Prp]] -> World -> [Prp]
forall a. HasCallStack => [a] -> World -> a
!! World
k) ) | Prp
p <- [Prp]
addProps ]
  newM :: Map World (Map Prp Bool, Map Agent [World])
newM = (World
 -> (Map Prp Bool, Map Agent [World])
 -> (Map Prp Bool, Map Agent [World]))
-> Map World (Map Prp Bool, Map Agent [World])
-> Map World (Map Prp Bool, Map Agent [World])
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (\World
w (Map Prp Bool
val,Map Agent [World]
r) -> (Map Prp Bool -> Map Prp Bool -> Map Prp Bool
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map Prp Bool
val (World -> Map Prp Bool
addValForIndex (World -> World
indexOf World
w)),Map Agent [World]
r)) Map World (Map Prp Bool, Map Agent [World])
m

actionToEvent :: PointedActionModel -> Event
actionToEvent :: PointedActionModel -> Event
actionToEvent (ActM Map World Act
am, World
faction) = ([Prp] -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
Trf [Prp]
addprops Form
addlaw Map Prp Bdd
changelaw Map Agent RelBDD
eventObs, [Prp]
efacts) where
  actions :: [World]
actions      = Map World Act -> [World]
forall k a. Map k a -> [k]
M.keys Map World Act
am
  (P World
fstnewp)  = [Prp] -> Prp
freshp ([Prp] -> Prp) -> [Prp] -> Prp
forall a b. (a -> b) -> a -> b
$ (Act -> [Prp]) -> [Act] -> [Prp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap -- avoid props in pre and postconditions
                 (\Act
c -> [Form] -> [Prp]
propsInForms (Act -> Form
pre Act
c Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: Map Prp Form -> [Form]
forall k a. Map k a -> [a]
M.elems (Act -> Map Prp Form
post Act
c)) [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ Map Prp Form -> [Prp]
forall k a. Map k a -> [k]
M.keys (Act -> Map Prp Form
post Act
c)) (Map World Act -> [Act]
forall k a. Map k a -> [a]
M.elems Map World Act
am)
  addprops :: [Prp]
addprops     = [World -> Prp
P World
fstnewp..World -> Prp
P World
maxactprop] -- new props to distinguish all actions
  maxactprop :: World
maxactprop   = World
fstnewp World -> World -> World
forall a. Num a => a -> a -> a
+ Float -> World
forall b. Integral b => Float -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Float -> Float -> Float
forall a. Floating a => a -> a -> a
logBase Float
2 (World -> Float
forall a b. (Integral a, Num b) => a -> b
fromIntegral (World -> Float) -> World -> Float
forall a b. (a -> b) -> a -> b
$ [World] -> World
forall a. [a] -> World
forall (t :: * -> *) a. Foldable t => t a -> World
length [World]
actions) :: Float) World -> World -> World
forall a. Num a => a -> a -> a
- World
1
  ell :: World -> [Prp]
ell          = Rel World [Prp] -> World -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply (Rel World [Prp] -> World -> [Prp])
-> Rel World [Prp] -> World -> [Prp]
forall a b. (a -> b) -> a -> b
$ [World] -> [[Prp]] -> Rel World [Prp]
forall a b. [a] -> [b] -> [(a, b)]
zip [World]
actions ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
addprops) -- injectively label actions with sets of propositions
  addlaw :: Form
addlaw       = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Disj [ [Form] -> Form
Conj [ [Prp] -> [Prp] -> Form
booloutofForm (World -> [Prp]
ell World
a) [Prp]
addprops, Act -> Form
pre (Act -> Form) -> Act -> Form
forall a b. (a -> b) -> a -> b
$ Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
a ] | World
a <- [World]
actions ]
  changeprops :: [Prp]
changeprops  = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Map Prp Form -> [Prp]) -> [Map Prp Form] -> [Prp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Map Prp Form -> [Prp]
forall k a. Map k a -> [k]
M.keys ([Map Prp Form] -> [Prp])
-> (Map World (Map Prp Form) -> [Map Prp Form])
-> Map World (Map Prp Form)
-> [Prp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map World (Map Prp Form) -> [Map Prp Form]
forall k a. Map k a -> [a]
M.elems (Map World (Map Prp Form) -> [Prp])
-> Map World (Map Prp Form) -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Act -> Map Prp Form) -> Map World Act -> Map World (Map Prp Form)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map Act -> Map Prp Form
post Map World Act
am -- propositions to be changed
  changelaw :: Map Prp Bdd
changelaw    = [(Prp, Bdd)] -> Map Prp Bdd
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Prp
p, Prp -> Bdd
changeFor Prp
p) | Prp
p <- [Prp]
changeprops ] -- encode postconditions
  changeFor :: Prp -> Bdd
changeFor Prp
p  = [Bdd] -> Bdd
disSet [ [Prp] -> [Prp] -> Bdd
booloutof (World -> [Prp]
ell World
k) [Prp]
addprops Bdd -> Bdd -> Bdd
`con` Form -> Bdd
boolBddOf (Act -> Prp -> Form
safepost (Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
k) Prp
p) | World
k <- [World]
actions ]
  eventObs :: Map Agent RelBDD
eventObs     = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Agent
i, Agent -> RelBDD
forall {f :: * -> *}. Applicative f => Agent -> f Bdd
obsLawFor Agent
i) | Agent
i <- ActionModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf (Map World Act -> ActionModel
ActM Map World Act
am) ]
  obsLawFor :: Agent -> f Bdd
obsLawFor Agent
i  = Bdd -> f Bdd
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bdd -> f Bdd) -> Bdd -> f Bdd
forall a b. (a -> b) -> a -> b
$ [Bdd] -> Bdd
disSet (Map World Bdd -> [Bdd]
forall k a. Map k a -> [a]
M.elems (Map World Bdd -> [Bdd]) -> Map World Bdd -> [Bdd]
forall a b. (a -> b) -> a -> b
$ (World -> Act -> Bdd) -> Map World Act -> Map World Bdd
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (Agent -> World -> Act -> Bdd
link Agent
i) Map World Act
am)
  link :: Agent -> World -> Act -> Bdd
link Agent
i World
k Act
ch  = [Prp] -> [Prp] -> Bdd
booloutof ([Prp] -> [Prp]
mv ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ World -> [Prp]
ell World
k) ([Prp] -> [Prp]
mv [Prp]
addprops) Bdd -> Bdd -> Bdd
`con` -- encode relations
                 [Bdd] -> Bdd
disSet [ [Prp] -> [Prp] -> Bdd
booloutof ([Prp] -> [Prp]
cp ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ World -> [Prp]
ell World
there) ([Prp] -> [Prp]
cp [Prp]
addprops) | World
there <- Act -> Map Agent [World]
rel Act
ch Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
i ]
  efacts :: [Prp]
efacts       = World -> [Prp]
ell World
faction

eventToAction :: Event -> PointedActionModel
eventToAction :: Event -> PointedActionModel
eventToAction (t :: Transformer
t@(Trf [Prp]
addprops Form
addlaw Map Prp Bdd
changelaw Map Agent RelBDD
eventObs), [Prp]
efacts) = (Map World Act -> ActionModel
ActM Map World Act
am, World
faction) where
  actlist :: [([Prp], World)]
actlist    = [[Prp]] -> [World] -> [([Prp], World)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
addprops) [World
0..]
  am :: Map World Act
am         = [(World, Act)] -> Map World Act
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (World
a, Form -> Map Prp Form -> Map Agent [World] -> Act
Act ([Prp] -> Form
preFor [Prp]
ps) ([Prp] -> Map Prp Form
forall {t :: * -> *}. Foldable t => t Prp -> Map Prp Form
postFor [Prp]
ps) ([Prp] -> Map Agent [World]
relFor [Prp]
ps)) | ([Prp]
ps,World
a) <- [([Prp], World)]
actlist, [Prp] -> Form
preFor [Prp]
ps Form -> Form -> Bool
forall a. Eq a => a -> a -> Bool
/= Form
Bot ]
  preFor :: [Prp] -> Form
preFor [Prp]
ps  = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [(Prp, Form)] -> Form -> Form
substitSet ((Prp -> (Prp, Form)) -> [Prp] -> [(Prp, Form)]
forall a b. (a -> b) -> [a] -> [b]
map (, Form
Top) [Prp]
ps [(Prp, Form)] -> [(Prp, Form)] -> [(Prp, Form)]
forall a. [a] -> [a] -> [a]
++ (Prp -> (Prp, Form)) -> [Prp] -> [(Prp, Form)]
forall a b. (a -> b) -> [a] -> [b]
map (, Form
Bot) ([Prp]
addprops [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
ps)) Form
addlaw
  postFor :: t Prp -> Map Prp Form
postFor t Prp
ps = [(Prp, Form)] -> Map Prp Form
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Prp
q, Bdd -> Form
formOf (Bdd -> Form) -> Bdd -> Form
forall a b. (a -> b) -> a -> b
$ (Map Prp Bdd
changelaw Map Prp Bdd -> Prp -> Bdd
forall k a. Ord k => Map k a -> k -> a
! Prp
q) Bdd -> Assignment -> Bdd
`restrictSet` [(World
p, World -> Prp
P World
p Prp -> t Prp -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Prp
ps) | (P World
p) <- [Prp]
addprops]) | Prp
q <- Map Prp Bdd -> [Prp]
forall k a. Map k a -> [k]
M.keys Map Prp Bdd
changelaw ]
  relFor :: [Prp] -> Map Agent [World]
relFor [Prp]
ps  = [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent
i,Agent -> [World]
rFor Agent
i) | Agent
i <- Transformer -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf Transformer
t] where
    rFor :: Agent -> [World]
rFor Agent
i   = (([Prp], World) -> [World]) -> [([Prp], World)] -> [World]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\([Prp]
qs,World
b) -> [ World
b | [Prp] -> RelBDD -> Bool
forall a. TagBdd a => [Prp] -> Tagged a Bdd -> Bool
tagBddEval ([Prp] -> [Prp]
mv [Prp]
ps [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp] -> [Prp]
cp [Prp]
qs) (Map Agent RelBDD
eventObs Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
i), [Prp] -> Form
preFor [Prp]
qs Form -> Form -> Bool
forall a. Eq a => a -> a -> Bool
/= Form
Bot ]) [([Prp], World)]
actlist
  faction :: World
faction    = [([Prp], World)] -> [Prp] -> World
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [([Prp], World)]
actlist [Prp]
efacts