{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables,
TupleSections #-}
module SMCDEL.Symbolic.Ki where
import Data.Tagged
import Control.Arrow (first)
import Data.Dynamic (fromDynamic)
import Data.HasCacBDD hiding (Top,Bot)
import Data.List (sort,intersect,(\\))
import qualified Data.Map.Strict as M
import Data.Map.Strict ((!))
import SMCDEL.Internal.Help (apply,lfp,powerset)
import SMCDEL.Language
import SMCDEL.Other.BDD2Form
import SMCDEL.Symbolic.S5 (State,boolBddOf,texBddWith,bddEval,relabelWith)
import SMCDEL.Translations.S5 (booloutof)
mvP, cpP :: Int -> Prp -> Prp
mvP :: Int -> Prp -> Prp
mvP Int
m (P Int
n) = Int -> Prp
P ((Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n) Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
m)
cpP :: Int -> Prp -> Prp
cpP Int
m (P Int
n) = Int -> Prp
P ((Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
m)
unmvcpP :: Int -> Prp -> Prp
unmvcpP :: Int -> Prp -> Prp
unmvcpP Int
m (P Int
n) | Int -> Bool
forall a. Integral a => a -> Bool
even (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
m) = Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
m) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
| Bool
otherwise = Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
mv, cp :: Int -> [Prp] -> [Prp]
mv :: Int -> State -> State
mv Int
m = (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map ((Prp -> Prp) -> State -> State) -> (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> a -> b
$ Int -> Prp -> Prp
mvP Int
m
cp :: Int -> State -> State
cp Int
m = (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map ((Prp -> Prp) -> State -> State) -> (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> a -> b
$ Int -> Prp -> Prp
cpP Int
m
unmv, uncp :: Int -> [Prp] -> [Prp]
unmv :: Int -> State -> State
unmv Int
m = (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Prp
f where
f :: Prp -> Prp
f (P Int
n) | Int -> Bool
forall a. Integral a => a -> Bool
odd Int
m = Agent -> Prp
forall a. HasCallStack => Agent -> a
error Agent
"unmv failed: Number is odd!"
| Bool
otherwise = Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
m) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
uncp :: Int -> State -> State
uncp Int
m = (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Prp
f where
f :: Prp -> Prp
f (P Int
n) | Int -> Bool
forall a. Integral a => a -> Bool
even Int
m = Agent -> Prp
forall a. HasCallStack => Agent -> a
error Agent
"uncp failed: Number is even!"
| Bool
otherwise = Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
data Dubbel
type RelBDD = Tagged Dubbel Bdd
totalRelBdd, emptyRelBdd :: RelBDD
totalRelBdd :: RelBDD
totalRelBdd = Bdd -> RelBDD
forall a. a -> Tagged Dubbel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bdd -> RelBDD) -> Bdd -> RelBDD
forall a b. (a -> b) -> a -> b
$ Form -> Bdd
boolBddOf Form
Top
emptyRelBdd :: RelBDD
emptyRelBdd = Bdd -> RelBDD
forall a. a -> Tagged Dubbel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bdd -> RelBDD) -> Bdd -> RelBDD
forall a b. (a -> b) -> a -> b
$ Form -> Bdd
boolBddOf Form
Bot
allsamebdd :: Int -> [Prp] -> RelBDD
allsamebdd :: Int -> State -> RelBDD
allsamebdd Int
m State
ps = Bdd -> RelBDD
forall a. a -> Tagged Dubbel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bdd -> RelBDD) -> Bdd -> RelBDD
forall a b. (a -> b) -> a -> b
$ [Bdd] -> Bdd
conSet [Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF Prp
p Form -> Form -> Form
`Equi` Prp -> Form
PrpF Prp
p' | (Prp
p,Prp
p') <- State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> State -> State
mv Int
m State
ps) (Int -> State -> State
cp Int
m State
ps)]
class TagBdd a where
tagBddEval :: [Prp] -> Tagged a Bdd -> Bool
tagBddEval State
truths Tagged a Bdd
querybdd = Bdd -> (Int -> Bool) -> Bool
evaluateFun (Tagged a Bdd -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag Tagged a Bdd
querybdd) (\Int
n -> Int -> Prp
P Int
n Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` State
truths)
instance TagBdd Dubbel
cpBdd :: Int -> Bdd -> RelBDD
cpBdd :: Int -> Bdd -> RelBDD
cpBdd Int
m Bdd
b = Bdd -> RelBDD
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> RelBDD) -> Bdd -> RelBDD
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Bdd -> Bdd
relabelFun (\Int
n -> (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Bdd
b
mvBdd :: Int -> Bdd -> RelBDD
mvBdd :: Int -> Bdd -> RelBDD
mvBdd Int
m Bdd
b = Bdd -> RelBDD
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> RelBDD) -> Bdd -> RelBDD
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Bdd -> Bdd
relabelFun (\Int
n -> (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m) Bdd
b
unmvBdd :: Int -> RelBDD -> Bdd
unmvBdd :: Int -> RelBDD -> Bdd
unmvBdd Int
m (Tagged Bdd
b) =
(Int -> Int) -> Bdd -> Bdd
relabelFun (\Int
n -> if Int -> Bool
forall a. Integral a => a -> Bool
even (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
m) then (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
m) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2 else Agent -> Int
forall a. HasCallStack => Agent -> a
error (Agent
"Not even: " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Int -> Agent
forall a. Show a => a -> Agent
show Int
n)) Bdd
b
data BelStruct = BlS [Prp]
Bdd
(M.Map Agent Int, RelBDD)
deriving (BelStruct -> BelStruct -> Bool
(BelStruct -> BelStruct -> Bool)
-> (BelStruct -> BelStruct -> Bool) -> Eq BelStruct
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BelStruct -> BelStruct -> Bool
== :: BelStruct -> BelStruct -> Bool
$c/= :: BelStruct -> BelStruct -> Bool
/= :: BelStruct -> BelStruct -> Bool
Eq,Int -> BelStruct -> Agent -> Agent
[BelStruct] -> Agent -> Agent
BelStruct -> Agent
(Int -> BelStruct -> Agent -> Agent)
-> (BelStruct -> Agent)
-> ([BelStruct] -> Agent -> Agent)
-> Show BelStruct
forall a.
(Int -> a -> Agent -> Agent)
-> (a -> Agent) -> ([a] -> Agent -> Agent) -> Show a
$cshowsPrec :: Int -> BelStruct -> Agent -> Agent
showsPrec :: Int -> BelStruct -> Agent -> Agent
$cshow :: BelStruct -> Agent
show :: BelStruct -> Agent
$cshowList :: [BelStruct] -> Agent -> Agent
showList :: [BelStruct] -> Agent -> Agent
Show)
instance Pointed BelStruct State
type BelScene = (BelStruct,State)
instance Pointed BelStruct Bdd
type MultipointedBelScene = (BelStruct,Bdd)
instance HasVocab BelStruct where
vocabOf :: BelStruct -> State
vocabOf (BlS State
voc Bdd
_ (Map Agent Int, RelBDD)
_) = State
voc
instance HasAgents BelStruct where
agentsOf :: BelStruct -> [Agent]
agentsOf (BlS State
_ Bdd
_ (Map Agent Int
ag, RelBDD
_)) = Map Agent Int -> [Agent]
forall k a. Map k a -> [k]
M.keys Map Agent Int
ag
bddOf :: BelStruct -> Form -> Bdd
bddOf :: BelStruct -> Form -> Bdd
bddOf BelStruct
_ Form
Top = Bdd
top
bddOf BelStruct
_ Form
Bot = Bdd
bot
bddOf BelStruct
_ (PrpF (P Int
n)) = Int -> Bdd
var Int
n
bddOf BelStruct
bls (Neg Form
form) = Bdd -> Bdd
neg (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
form
bddOf BelStruct
bls (Conj [Form]
forms) = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> [Bdd] -> Bdd
forall a b. (a -> b) -> a -> b
$ (Form -> Bdd) -> [Form] -> [Bdd]
forall a b. (a -> b) -> [a] -> [b]
map (BelStruct -> Form -> Bdd
bddOf BelStruct
bls) [Form]
forms
bddOf BelStruct
bls (Disj [Form]
forms) = [Bdd] -> Bdd
disSet ([Bdd] -> Bdd) -> [Bdd] -> Bdd
forall a b. (a -> b) -> a -> b
$ (Form -> Bdd) -> [Form] -> [Bdd]
forall a b. (a -> b) -> [a] -> [b]
map (BelStruct -> Form -> Bdd
bddOf BelStruct
bls) [Form]
forms
bddOf BelStruct
bls (Xor [Form]
forms) = [Bdd] -> Bdd
xorSet ([Bdd] -> Bdd) -> [Bdd] -> Bdd
forall a b. (a -> b) -> a -> b
$ (Form -> Bdd) -> [Form] -> [Bdd]
forall a b. (a -> b) -> [a] -> [b]
map (BelStruct -> Form -> Bdd
bddOf BelStruct
bls) [Form]
forms
bddOf BelStruct
bls (Impl Form
f Form
g) = Bdd -> Bdd -> Bdd
imp (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
g)
bddOf BelStruct
bls (Equi Form
f Form
g) = Bdd -> Bdd -> Bdd
equ (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
g)
bddOf BelStruct
bls (Forall State
ps Form
f) = [Int] -> Bdd -> Bdd
forallSet ((Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum State
ps) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f)
bddOf BelStruct
bls (Exists State
ps Form
f) = [Int] -> Bdd -> Bdd
existsSet ((Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum State
ps) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f)
bddOf bls :: BelStruct
bls@(BlS State
allprops Bdd
lawbdd (Map Agent Int
ags, RelBDD
obdds)) (K Agent
i Form
form) = Int -> RelBDD -> Bdd
unmvBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) RelBDD
result where
result :: RelBDD
result = [Int] -> Bdd -> Bdd
forallSet [Int]
ps' (Bdd -> Bdd) -> RelBDD -> RelBDD
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bdd -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) 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 -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelBDD
forall {s}. Tagged s Bdd
omegai 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
<*> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
form)))
ps' :: [Int]
ps' = (Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum (State -> [Int]) -> State -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
allprops
omegai :: Tagged s Bdd
omegai = Bdd -> Tagged s Bdd
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> Tagged s Bdd) -> Bdd -> Tagged s Bdd
forall a b. (a -> b) -> a -> b
$ Bdd -> (Int, Bool) -> Bdd
restrict (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
obdds) (Map Agent Int
ags Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
! Agent
i, Bool
True)
bddOf bls :: BelStruct
bls@(BlS State
allprops Bdd
lawbdd (Map Agent Int
ags, RelBDD
obdds)) (Kw Agent
i Form
form) = Int -> RelBDD -> Bdd
unmvBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) RelBDD
result where
result :: RelBDD
result = Bdd -> Bdd -> Bdd
dis (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Form -> RelBDD
part Form
form 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
<*> Form -> RelBDD
part (Form -> Form
Neg Form
form)
part :: Form -> RelBDD
part Form
f = [Int] -> Bdd -> Bdd
forallSet [Int]
ps' (Bdd -> Bdd) -> RelBDD -> RelBDD
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bdd -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) 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 -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelBDD
forall {s}. Tagged s Bdd
omegai 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
<*> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f)))
ps' :: [Int]
ps' = (Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum (State -> [Int]) -> State -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
allprops
omegai :: Tagged s Bdd
omegai = Bdd -> Tagged s Bdd
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> Tagged s Bdd) -> Bdd -> Tagged s Bdd
forall a b. (a -> b) -> a -> b
$ Bdd -> (Int, Bool) -> Bdd
restrict (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
obdds) (Map Agent Int
ags Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
! Agent
i, Bool
True)
bddOf bls :: BelStruct
bls@(BlS State
voc Bdd
lawbdd (Map Agent Int
ag,RelBDD
obdds)) (Ck [Agent]
ags Form
form) = (Bdd -> Bdd) -> Bdd -> Bdd
forall a. Eq a => (a -> a) -> a -> a
lfp Bdd -> Bdd
lambda Bdd
top where
ps' :: [Int]
ps' = (Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum (State -> [Int]) -> State -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ag) State
voc
lambda :: Bdd -> Bdd
lambda :: Bdd -> Bdd
lambda Bdd
z = Int -> RelBDD -> Bdd
unmvBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ag) (RelBDD -> Bdd) -> RelBDD -> Bdd
forall a b. (a -> b) -> a -> b
$
[Int] -> Bdd -> Bdd
forallSet [Int]
ps' (Bdd -> Bdd) -> RelBDD -> RelBDD
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(Bdd -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ag) 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 -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> ([Bdd] -> Bdd) -> [Bdd] -> Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bdd] -> Bdd
disSet ([Bdd] -> Bdd -> Bdd)
-> Tagged Dubbel [Bdd] -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RelBDD] -> Tagged Dubbel [Bdd]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [Bdd -> RelBDD
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> RelBDD) -> Bdd -> RelBDD
forall a b. (a -> b) -> a -> b
$ Bdd -> (Int, Bool) -> Bdd
restrict (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
obdds) (Map Agent Int
ag Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
! Agent
i, Bool
True) | Agent
i <- [Agent]
ags]) 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
<*>
Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ag) (Bdd -> Bdd -> Bdd
con (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
form) Bdd
z)))
bddOf BelStruct
bls (Ckw [Agent]
ags Form
form) = Bdd -> Bdd -> Bdd
dis (BelStruct -> Form -> Bdd
bddOf BelStruct
bls ([Agent] -> Form -> Form
Ck [Agent]
ags Form
form)) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls ([Agent] -> Form -> Form
Ck [Agent]
ags (Form -> Form
Neg Form
form)))
bddOf bls :: BelStruct
bls@(BlS State
allprops Bdd
lawbdd (Map Agent Int
ags, RelBDD
obdds)) (Dk [Agent]
ags_names Form
form) = Int -> RelBDD -> Bdd
unmvBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) RelBDD
result where
result :: RelBDD
result = [Int] -> Bdd -> Bdd
forallSet [Int]
ps' (Bdd -> Bdd) -> RelBDD -> RelBDD
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bdd -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) 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 -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelBDD
forall {s}. Tagged s Bdd
omegai 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
<*> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
form)))
ps' :: [Int]
ps' = (Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum (State -> [Int]) -> State -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
allprops
omegai :: Tagged s Bdd
omegai = Bdd -> Tagged s Bdd
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> Tagged s Bdd) -> Bdd -> Tagged s Bdd
forall a b. (a -> b) -> a -> b
$ Bdd -> [(Int, Bool)] -> Bdd
restrictSet (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
obdds) ([(Int, Bool)] -> Bdd) -> [(Int, Bool)] -> Bdd
forall a b. (a -> b) -> a -> b
$ (Agent -> (Int, Bool)) -> [Agent] -> [(Int, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ((,Bool
True) (Int -> (Int, Bool)) -> (Agent -> Int) -> Agent -> (Int, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Agent Int
ags Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
!)) [Agent]
ags_names
bddOf bls :: BelStruct
bls@(BlS State
allprops Bdd
lawbdd (Map Agent Int
ags, RelBDD
obdds)) (Dkw [Agent]
ags_names Form
form) = Int -> RelBDD -> Bdd
unmvBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) RelBDD
result where
result :: RelBDD
result = Bdd -> Bdd -> Bdd
dis (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Form -> RelBDD
part Form
form 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
<*> Form -> RelBDD
part (Form -> Form
Neg Form
form)
part :: Form -> RelBDD
part Form
f = [Int] -> Bdd -> Bdd
forallSet [Int]
ps' (Bdd -> Bdd) -> RelBDD -> RelBDD
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bdd -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) 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 -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelBDD
forall {s}. Tagged s Bdd
omegai 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
<*> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f)))
ps' :: [Int]
ps' = (Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum (State -> [Int]) -> State -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
allprops
omegai :: Tagged s Bdd
omegai = Bdd -> Tagged s Bdd
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> Tagged s Bdd) -> Bdd -> Tagged s Bdd
forall a b. (a -> b) -> a -> b
$ Bdd -> [(Int, Bool)] -> Bdd
restrictSet (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
obdds) ([(Int, Bool)] -> Bdd) -> [(Int, Bool)] -> Bdd
forall a b. (a -> b) -> a -> b
$ (Agent -> (Int, Bool)) -> [Agent] -> [(Int, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ((,Bool
True) (Int -> (Int, Bool)) -> (Agent -> Int) -> Agent -> (Int, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map Agent Int
ags Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
!)) [Agent]
ags_names
bddOf BelStruct
bls (PubAnnounce Form
f Form
g) =
Bdd -> Bdd -> Bdd
imp (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f) (BelStruct -> Form -> Bdd
bddOf (BelStruct
bls BelStruct -> Form -> BelStruct
forall a b. Update a b => a -> b -> a
`update` Form
f) Form
g)
bddOf BelStruct
bls (PubAnnounceW Form
f Form
g) =
Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f)
(BelStruct -> Form -> Bdd
bddOf (BelStruct
bls BelStruct -> Form -> BelStruct
forall a b. Update a b => a -> b -> a
`update` Form
f ) Form
g)
(BelStruct -> Form -> Bdd
bddOf (BelStruct
bls BelStruct -> Form -> BelStruct
forall a b. Update a b => a -> b -> a
`update` Form -> Form
Neg Form
f) Form
g)
bddOf bls :: BelStruct
bls@(BlS State
props Bdd
_ (Map Agent Int, RelBDD)
_) (Announce [Agent]
ags Form
f Form
g) =
Bdd -> Bdd -> Bdd
imp (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f) (Bdd -> (Int, Bool) -> Bdd
restrict Bdd
bdd2 (Int
k,Bool
True)) where
bdd2 :: Bdd
bdd2 = BelStruct -> Form -> Bdd
bddOf (BelStruct -> [Agent] -> Form -> BelStruct
announce BelStruct
bls [Agent]
ags Form
f) Form
g
(P Int
k) = State -> Prp
freshp State
props
bddOf bls :: BelStruct
bls@(BlS State
props Bdd
_ (Map Agent Int, RelBDD)
_) (AnnounceW [Agent]
ags Form
f Form
g) =
Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f) Bdd
bdd2a Bdd
bdd2b where
bdd2a :: Bdd
bdd2a = Bdd -> (Int, Bool) -> Bdd
restrict (BelStruct -> Form -> Bdd
bddOf (BelStruct -> [Agent] -> Form -> BelStruct
announce BelStruct
bls [Agent]
ags Form
f ) Form
g) (Int
k,Bool
True)
bdd2b :: Bdd
bdd2b = Bdd -> (Int, Bool) -> Bdd
restrict (BelStruct -> Form -> Bdd
bddOf (BelStruct -> [Agent] -> Form -> BelStruct
announce BelStruct
bls [Agent]
ags (Form -> Form
Neg Form
f)) Form
g) (Int
k,Bool
True)
(P Int
k) = State -> Prp
freshp State
props
bddOf BelStruct
bls (Dia (Dyn Agent
dynLabel Dynamic
d) Form
f) =
Bdd -> Bdd -> Bdd
con (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
preCon)
(Bdd -> Bdd) -> (Form -> Bdd) -> Form -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
copyrelInverse
(Bdd -> Bdd) -> (Form -> Bdd) -> Form -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> Bdd
simulateActualEvents
(Bdd -> Bdd) -> (Form -> Bdd) -> Form -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, Bdd)] -> Bdd -> Bdd
substitSimul [ (Int
k, Map Prp Bdd
changeLaw Map Prp Bdd -> Prp -> Bdd
forall k a. Ord k => Map k a -> k -> a
! Prp
p)
| p :: Prp
p@(P Int
k) <- State
changeProps]
(Bdd -> Bdd) -> (Form -> Bdd) -> Form -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BelStruct -> Form -> Bdd
bddOf (BelStruct
bls BelStruct -> Transformer -> BelStruct
forall a b. Update a b => a -> b -> a
`update` Transformer
trf)
(Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Form
f
where
changeProps :: State
changeProps = Map Prp Bdd -> State
forall k a. Map k a -> [k]
M.keys Map Prp Bdd
changeLaw
copychangeProps :: State
copychangeProps = [(State -> Prp
freshp (State -> Prp) -> State -> Prp
forall a b. (a -> b) -> a -> b
$ BelStruct -> State
forall a. HasVocab a => a -> State
vocabOf BelStruct
bls State -> State -> State
forall a. [a] -> [a] -> [a]
++ State
addProps)..]
copyrelInverse :: [(Prp, Prp)]
copyrelInverse = State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip State
copychangeProps State
changeProps
(trf :: Transformer
trf@(Trf State
addProps Form
addLaw Map Prp Bdd
changeLaw (Map Agent Int, RelBDD)
_), [(Prp, Prp)]
shiftrel) = BelStruct -> Transformer -> (Transformer, [(Prp, Prp)])
shiftPrepare BelStruct
bls Transformer
trfUnshifted
(Form
preCon,Transformer
trfUnshifted,Bdd -> Bdd
simulateActualEvents) =
case Dynamic -> Maybe Event
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
Just ((Transformer
t,State
x) :: Event) -> ( Event -> Form
forall a. HasPrecondition a => a -> Form
preOf (Transformer
t,State
x), Transformer
t, (Bdd -> [(Int, Bool)] -> Bdd
`restrictSet` [(Int, Bool)]
actualAss) )
where actualAss :: [(Int, Bool)]
actualAss = [(Int
newK, Int -> Prp
P Int
k Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` State
x) | (P Int
k, P Int
newK) <- [(Prp, Prp)]
shiftrel]
Maybe Event
Nothing -> case Dynamic -> Maybe MultipointedEvent
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
Just ((Transformer
t,Bdd
xsBdd) :: MultipointedEvent) ->
( MultipointedEvent -> Form
forall a. HasPrecondition a => a -> Form
preOf (Transformer
t,Bdd
xsBdd), Transformer
t
, [Int] -> Bdd -> Bdd
existsSet ((Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum State
addProps)
(Bdd -> Bdd) -> (Bdd -> Bdd) -> Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> Bdd -> Bdd
con Bdd
actualsBdd
(Bdd -> Bdd) -> (Bdd -> Bdd) -> Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> Bdd -> Bdd
con (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
addLaw)
) where actualsBdd :: Bdd
actualsBdd = [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftrel Bdd
xsBdd
Maybe MultipointedEvent
Nothing -> Agent -> (Form, Transformer, Bdd -> Bdd)
forall a. HasCallStack => Agent -> a
error (Agent -> (Form, Transformer, Bdd -> Bdd))
-> Agent -> (Form, Transformer, Bdd -> Bdd)
forall a b. (a -> b) -> a -> b
$ Agent
"cannot update belief structure with '" Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
dynLabel Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"':\n " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Dynamic -> Agent
forall a. Show a => a -> Agent
show Dynamic
d
validViaBdd :: BelStruct -> Form -> Bool
validViaBdd :: BelStruct -> Form -> Bool
validViaBdd bls :: BelStruct
bls@(BlS State
_ Bdd
lawbdd (Map Agent Int, RelBDD)
_) Form
f = Bdd
top Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd -> Bdd -> Bdd
imp Bdd
lawbdd (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f)
evalViaBdd :: BelScene -> Form -> Bool
evalViaBdd :: BelScene -> Form -> Bool
evalViaBdd (bls :: BelStruct
bls@(BlS State
allprops Bdd
_ (Map Agent Int, RelBDD)
_),State
s) Form
f = let
bdd :: Bdd
bdd = BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f
b :: Bdd
b = Bdd -> [(Int, Bool)] -> Bdd
restrictSet Bdd
bdd [(Int, Bool)]
list
list :: [(Int, Bool)]
list = [ (Int
n, Int -> Prp
P Int
n Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` State
s) | (P Int
n) <- State
allprops ]
in
case (Bdd
bBdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
==Bdd
top,Bdd
bBdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
==Bdd
bot) of
(Bool
True,Bool
_) -> Bool
True
(Bool
_,Bool
True) -> Bool
False
(Bool, Bool)
_ -> Agent -> Bool
forall a. HasCallStack => Agent -> a
error (Agent -> Bool) -> Agent -> Bool
forall a b. (a -> b) -> a -> b
$ Agent
"evalViaBdd failed: Composite BDD leftover!\n"
Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" bls: " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ BelStruct -> Agent
forall a. Show a => a -> Agent
show BelStruct
bls Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"\n"
Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" s: " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ State -> Agent
forall a. Show a => a -> Agent
show State
s Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"\n"
Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" form: " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Form -> Agent
forall a. Show a => a -> Agent
show Form
f Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"\n"
Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" bdd: " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Bdd -> Agent
forall a. Show a => a -> Agent
show Bdd
bdd Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"\n"
Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" list: " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ [(Int, Bool)] -> Agent
forall a. Show a => a -> Agent
show [(Int, Bool)]
list Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"\n"
Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" b: " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Bdd -> Agent
forall a. Show a => a -> Agent
show Bdd
b Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"\n"
instance Semantics BelStruct where
isTrue :: BelStruct -> Form -> Bool
isTrue = BelStruct -> Form -> Bool
validViaBdd
instance Semantics BelScene where
isTrue :: BelScene -> Form -> Bool
isTrue = BelScene -> Form -> Bool
evalViaBdd
instance Semantics MultipointedBelScene where
isTrue :: MultipointedBelScene -> Form -> Bool
isTrue (kns :: BelStruct
kns@(BlS State
_ Bdd
lawBdd (Map Agent Int, RelBDD)
_), Bdd
statesBdd) Form
f =
let a :: Bdd
a = Bdd -> Bdd -> Bdd
imp Bdd
lawBdd (Bdd -> Bdd -> Bdd
imp Bdd
statesBdd (BelStruct -> Form -> Bdd
bddOf BelStruct
kns Form
f))
in Bdd
a Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top
instance Update BelStruct Form where
checks :: [BelStruct -> Form -> Bool]
checks = [ ]
unsafeUpdate :: BelStruct -> Form -> BelStruct
unsafeUpdate bls :: BelStruct
bls@(BlS State
allprops Bdd
lawdd (Map Agent Int, RelBDD)
obs) Form
f =
State -> Bdd -> (Map Agent Int, RelBDD) -> BelStruct
BlS State
allprops (Bdd -> Bdd -> Bdd
con Bdd
lawdd (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
f)) (Map Agent Int, RelBDD)
obs
instance Update BelScene Form where
unsafeUpdate :: BelScene -> Form -> BelScene
unsafeUpdate (BelStruct
kns,State
s) Form
psi = (BelStruct -> Form -> BelStruct
forall a b. Update a b => a -> b -> a
unsafeUpdate BelStruct
kns Form
psi,State
s)
announce :: BelStruct -> [Agent] -> Form -> BelStruct
announce :: BelStruct -> [Agent] -> Form -> BelStruct
announce bls :: BelStruct
bls@(BlS State
props Bdd
lawbdd (Map Agent Int
ag,RelBDD
obdds)) [Agent]
ags Form
psi = State -> Bdd -> (Map Agent Int, RelBDD) -> BelStruct
BlS State
newprops Bdd
newlawbdd (Map Agent Int
ag,RelBDD
newobdds) where
(P Int
k) = State -> Prp
freshp State
props
newprops :: State
newprops = State -> State
forall a. Ord a => [a] -> [a]
sort (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
k Prp -> State -> State
forall a. a -> [a] -> [a]
: State
props
newlawbdd :: Bdd
newlawbdd = Bdd -> Bdd -> Bdd
con Bdd
lawbdd (Bdd -> Bdd -> Bdd
imp (Int -> Bdd
var Int
k) (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
psi))
newobdds :: RelBDD
newobdds = (RelBDD -> RelBDD -> RelBDD) -> RelBDD -> [RelBDD] -> RelBDD
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\RelBDD
x RelBDD
y -> Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelBDD
x 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
<*> RelBDD
y) (Bdd -> RelBDD
forall {k} (s :: k) b. b -> Tagged s b
Tagged Bdd
top) [Agent -> RelBDD -> RelBDD
newOfor Agent
i (RelBDD -> RelBDD) -> RelBDD -> RelBDD
forall a b. (a -> b) -> a -> b
$ Bdd -> RelBDD
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> (Int, Bool) -> Bdd
restrict (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
obdds) (Map Agent Int
ag Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
! Agent
i, Bool
True)) | Agent
i <- Map Agent Int -> [Agent]
forall k a. Map k a -> [k]
M.keys Map Agent Int
ag]
newOfor :: Agent -> RelBDD -> RelBDD
newOfor Agent
i RelBDD
oi | Agent
i Agent -> [Agent] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Agent]
ags = Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelBDD
oi 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
equ (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Bdd -> RelBDD
mvBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ag) (Int -> Bdd
var Int
k) 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
<*> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ag) (Int -> Bdd
var Int
k))
| Bool
otherwise = Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelBDD
oi 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
neg (Bdd -> Bdd) -> RelBDD -> RelBDD
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Bdd -> RelBDD
cpBdd (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ag) (Int -> Bdd
var Int
k))
statesOf :: BelStruct -> [State]
statesOf :: BelStruct -> [State]
statesOf (BlS State
allprops Bdd
lawbdd (Map Agent Int, RelBDD)
_) = ([(Prp, Bool)] -> State) -> [[(Prp, Bool)]] -> [State]
forall a b. (a -> b) -> [a] -> [b]
map (State -> State
forall a. Ord a => [a] -> [a]
sort(State -> State)
-> ([(Prp, Bool)] -> State) -> [(Prp, Bool)] -> State
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(Prp, Bool)] -> State
forall {b}. [(b, Bool)] -> [b]
getTrues) [[(Prp, Bool)]]
prpsats where
bddvars :: [Int]
bddvars = (Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum State
allprops
bddsats :: [[(Int, Bool)]]
bddsats = [Int] -> Bdd -> [[(Int, Bool)]]
allSatsWith [Int]
bddvars Bdd
lawbdd
prpsats :: [[(Prp, Bool)]]
prpsats = ([(Int, Bool)] -> [(Prp, Bool)])
-> [[(Int, Bool)]] -> [[(Prp, Bool)]]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Bool) -> (Prp, Bool)) -> [(Int, Bool)] -> [(Prp, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Prp) -> (Int, Bool) -> (Prp, Bool)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Int -> Prp
forall a. Enum a => Int -> a
toEnum)) [[(Int, Bool)]]
bddsats
getTrues :: [(b, Bool)] -> [b]
getTrues = ((b, Bool) -> b) -> [(b, Bool)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (b, Bool) -> b
forall a b. (a, b) -> a
fst ([(b, Bool)] -> [b])
-> ([(b, Bool)] -> [(b, Bool)]) -> [(b, Bool)] -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, Bool) -> Bool) -> [(b, Bool)] -> [(b, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (b, Bool) -> Bool
forall a b. (a, b) -> b
snd
texRelBDD :: RelBDD -> String
texRelBDD :: RelBDD -> Agent
texRelBDD (Tagged Bdd
b) = (Int -> Agent) -> Bdd -> Agent
texBddWith Int -> Agent
forall {a}. (Integral a, Show a) => a -> Agent
texRelProp Bdd
b where
texRelProp :: a -> Agent
texRelProp a
n
| a -> Bool
forall a. Integral a => a -> Bool
even a
n = a -> Agent
forall a. Show a => a -> Agent
show (a
n a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
2)
| Bool
otherwise = a -> Agent
forall a. Show a => a -> Agent
show ((a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
2) Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"'"
bddprefix, bddsuffix :: String
bddprefix :: Agent
bddprefix = Agent
"\\begin{array}{l} \\scalebox{0.3}{"
bddsuffix :: Agent
bddsuffix = Agent
"} \\end{array} \n"
data Transformer = Trf
[Prp]
Form
(M.Map Prp Bdd)
(M.Map Agent Int, RelBDD)
deriving (Transformer -> Transformer -> Bool
(Transformer -> Transformer -> Bool)
-> (Transformer -> Transformer -> Bool) -> Eq Transformer
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Transformer -> Transformer -> Bool
== :: Transformer -> Transformer -> Bool
$c/= :: Transformer -> Transformer -> Bool
/= :: Transformer -> Transformer -> Bool
Eq,Int -> Transformer -> Agent -> Agent
[Transformer] -> Agent -> Agent
Transformer -> Agent
(Int -> Transformer -> Agent -> Agent)
-> (Transformer -> Agent)
-> ([Transformer] -> Agent -> Agent)
-> Show Transformer
forall a.
(Int -> a -> Agent -> Agent)
-> (a -> Agent) -> ([a] -> Agent -> Agent) -> Show a
$cshowsPrec :: Int -> Transformer -> Agent -> Agent
showsPrec :: Int -> Transformer -> Agent -> Agent
$cshow :: Transformer -> Agent
show :: Transformer -> Agent
$cshowList :: [Transformer] -> Agent -> Agent
showList :: [Transformer] -> Agent -> Agent
Show)
instance HasAgents Transformer where
agentsOf :: Transformer -> [Agent]
agentsOf (Trf State
_ Form
_ Map Prp Bdd
_ (Map Agent Int
ags,RelBDD
_)) = Map Agent Int -> [Agent]
forall k a. Map k a -> [k]
M.keys Map Agent Int
ags
instance HasPrecondition Transformer where
preOf :: Transformer -> Form
preOf Transformer
_ = Form
Top
instance Pointed Transformer State
type Event = (Transformer,State)
instance HasPrecondition Event where
preOf :: Event -> Form
preOf (Trf State
addprops Form
addlaw Map Prp Bdd
_ (Map Agent Int, RelBDD)
_, State
x) = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ State -> State -> Form -> Form
substitOutOf State
x State
addprops Form
addlaw
instance Pointed Transformer [State]
type MultipointedEvent = (Transformer,Bdd)
instance HasPrecondition MultipointedEvent where
preOf :: MultipointedEvent -> Form
preOf (Trf State
addprops Form
addlaw Map Prp Bdd
_ (Map Agent Int, RelBDD)
_, Bdd
xsBdd) =
Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ State -> Form -> Form
Exists State
addprops ([Form] -> Form
Conj [ Bdd -> Form
formOf Bdd
xsBdd, Form
addlaw ])
shiftPrepare :: BelStruct -> Transformer -> (Transformer, [(Prp,Prp)])
shiftPrepare :: BelStruct -> Transformer -> (Transformer, [(Prp, Prp)])
shiftPrepare (BlS State
props Bdd
_ (Map Agent Int, RelBDD)
_) (Trf State
addprops Form
addlaw Map Prp Bdd
changelaw (Map Agent Int
ags, RelBDD
eventObs)) =
(State
-> Form -> Map Prp Bdd -> (Map Agent Int, RelBDD) -> Transformer
Trf State
shiftaddprops Form
addlawShifted Map Prp Bdd
changelawShifted (Map Agent Int
ags, RelBDD
forall {s}. Tagged s Bdd
eventObsShifted), [(Prp, Prp)]
shiftrel) where
shiftrel :: [(Prp, Prp)]
shiftrel = [(Prp, Prp)] -> [(Prp, Prp)]
forall a. Ord a => [a] -> [a]
sort ([(Prp, Prp)] -> [(Prp, Prp)]) -> [(Prp, Prp)] -> [(Prp, Prp)]
forall a b. (a -> b) -> a -> b
$ State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip State
addprops [(State -> Prp
freshp State
props)..]
shiftaddprops :: State
shiftaddprops = ((Prp, Prp) -> Prp) -> [(Prp, Prp)] -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Prp) -> Prp
forall a b. (a, b) -> b
snd [(Prp, Prp)]
shiftrel
addlawShifted :: Form
addlawShifted = [(Prp, Prp)] -> Form -> Form
replPsInF [(Prp, Prp)]
shiftrel Form
addlaw
changelawShifted :: Map Prp Bdd
changelawShifted = (Bdd -> Bdd) -> Map Prp Bdd -> Map Prp Bdd
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ([(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftrel) Map Prp Bdd
changelaw
shiftrelMVCP :: [(Prp, Prp)]
shiftrelMVCP = [(Prp, Prp)] -> [(Prp, Prp)]
forall a. Ord a => [a] -> [a]
sort ([(Prp, Prp)] -> [(Prp, Prp)]) -> [(Prp, Prp)] -> [(Prp, Prp)]
forall a b. (a -> b) -> a -> b
$ State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> State -> State
mv (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
addprops) (Int -> State -> State
mv (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
shiftaddprops)
[(Prp, Prp)] -> [(Prp, Prp)] -> [(Prp, Prp)]
forall a. [a] -> [a] -> [a]
++ State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
addprops) (Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
shiftaddprops)
eventObsShifted :: Tagged s Bdd
eventObsShifted = (Tagged s Bdd -> Tagged s Bdd -> Tagged s Bdd)
-> Tagged s Bdd -> [Tagged s Bdd] -> Tagged s Bdd
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Tagged s Bdd
x Tagged s Bdd
y -> Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> Tagged s Bdd -> Tagged s (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged s Bdd
x Tagged s (Bdd -> Bdd) -> Tagged s Bdd -> Tagged s Bdd
forall a b. Tagged s (a -> b) -> Tagged s a -> Tagged s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tagged s Bdd
y) (Bdd -> Tagged s Bdd
forall {k} (s :: k) b. b -> Tagged s b
Tagged Bdd
top) [Bdd -> Tagged s Bdd
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> Tagged s Bdd) -> Bdd -> Tagged s Bdd
forall a b. (a -> b) -> a -> b
$ [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftrelMVCP (Bdd -> (Int, Bool) -> Bdd
restrict (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
eventObs) (Map Agent Int
ags Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
! Agent
i, Bool
True)) | Agent
i <- Map Agent Int -> [Agent]
forall k a. Map k a -> [k]
M.keys Map Agent Int
ags]
instance Update BelScene Event where
unsafeUpdate :: BelScene -> Event -> BelScene
unsafeUpdate (bls :: BelStruct
bls@(BlS State
props Bdd
law (Map Agent Int
ags, RelBDD
obdds)),State
s) (Transformer
trf, State
eventFactsUnshifted) = (State -> Bdd -> (Map Agent Int, RelBDD) -> BelStruct
BlS State
newprops Bdd
newlaw (Map Agent Int
ags, RelBDD
forall {s}. Tagged s Bdd
newobs), State
news) where
(Trf State
addprops Form
addlaw Map Prp Bdd
changelaw (Map Agent Int
ag, RelBDD
addObs), [(Prp, Prp)]
shiftrel) = BelStruct -> Transformer -> (Transformer, [(Prp, Prp)])
shiftPrepare BelStruct
bls Transformer
trf
eventFacts :: State
eventFacts = (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map ([(Prp, Prp)] -> Prp -> Prp
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Prp, Prp)]
shiftrel) State
eventFactsUnshifted
changeprops :: State
changeprops = Map Prp Bdd -> State
forall k a. Map k a -> [k]
M.keys Map Prp Bdd
changelaw
copyrel :: [(Prp, Prp)]
copyrel = State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip State
changeprops [(State -> Prp
freshp (State -> Prp) -> State -> Prp
forall a b. (a -> b) -> a -> b
$ State
props State -> State -> State
forall a. [a] -> [a] -> [a]
++ State
addprops)..]
copychangeprops :: State
copychangeprops = ((Prp, Prp) -> Prp) -> [(Prp, Prp)] -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Prp) -> Prp
forall a b. (a, b) -> b
snd [(Prp, Prp)]
copyrel
copyrelMVCP :: [(Prp, Prp)]
copyrelMVCP = [(Prp, Prp)] -> [(Prp, Prp)]
forall a. Ord a => [a] -> [a]
sort ([(Prp, Prp)] -> [(Prp, Prp)]) -> [(Prp, Prp)] -> [(Prp, Prp)]
forall a b. (a -> b) -> a -> b
$ State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> State -> State
mv (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
changeprops) (Int -> State -> State
mv (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
copychangeprops)
[(Prp, Prp)] -> [(Prp, Prp)] -> [(Prp, Prp)]
forall a. [a] -> [a] -> [a]
++ State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
changeprops) (Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
copychangeprops)
newprops :: State
newprops = State -> State
forall a. Ord a => [a] -> [a]
sort (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ State
props State -> State -> State
forall a. [a] -> [a] -> [a]
++ State
addprops State -> State -> State
forall a. [a] -> [a] -> [a]
++ State
copychangeprops
newlaw :: Bdd
newlaw = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> [Bdd] -> Bdd
forall a b. (a -> b) -> a -> b
$ [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
copyrel (Bdd -> Bdd -> Bdd
con Bdd
law (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
addlaw))
Bdd -> [Bdd] -> [Bdd]
forall a. a -> [a] -> [a]
: [Int -> Bdd
var (Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
q) Bdd -> Bdd -> Bdd
`equ` [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
copyrel (Map Prp Bdd
changelaw Map Prp Bdd -> Prp -> Bdd
forall k a. Ord k => Map k a -> k -> a
! Prp
q) | Prp
q <- State
changeprops]
newobs :: Tagged s Bdd
newobs = (Tagged s Bdd -> Tagged s Bdd -> Tagged s Bdd)
-> Tagged s Bdd -> [Tagged s Bdd] -> Tagged s Bdd
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Tagged s Bdd
x Tagged s Bdd
y -> Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> Tagged s Bdd -> Tagged s (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged s Bdd
x Tagged s (Bdd -> Bdd) -> Tagged s Bdd -> Tagged s Bdd
forall a b. Tagged s (a -> b) -> Tagged s a -> Tagged s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tagged s Bdd
y) (Bdd -> Tagged s Bdd
forall {k} (s :: k) b. b -> Tagged s b
Tagged Bdd
top) [Tagged s Bdd]
forall {s}. [Tagged s Bdd]
newobdds
newobdds :: [Tagged s Bdd]
newobdds = [(Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> (Bdd -> Bdd) -> Bdd -> Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
copyrelMVCP (Bdd -> Bdd -> Bdd) -> Tagged s Bdd -> Tagged s (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> Tagged s Bdd
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> (Int, Bool) -> Bdd
restrict (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
obdds) (Map Agent Int
ag Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
! Agent
i, Bool
True))) Tagged s (Bdd -> Bdd) -> Tagged s Bdd -> Tagged s Bdd
forall a b. Tagged s (a -> b) -> Tagged s a -> Tagged s b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bdd -> Tagged s Bdd
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> (Int, Bool) -> Bdd
restrict (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
addObs) (Map Agent Int
ag Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
! Agent
i, Bool
True)) | Agent
i <- Map Agent Int -> [Agent]
forall k a. Map k a -> [k]
M.keys Map Agent Int
ag]
news :: State
news = State -> State
forall a. Ord a => [a] -> [a]
sort (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ [State] -> State
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ State
s State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ State
changeprops
, (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map ([(Prp, Prp)] -> Prp -> Prp
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Prp, Prp)]
copyrel) (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ State
s State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
`intersect` State
changeprops
, State
eventFacts
, (Prp -> Bool) -> State -> State
forall a. (a -> Bool) -> [a] -> [a]
filter (\ Prp
p -> State -> Bdd -> Bool
bddEval (State
s State -> State -> State
forall a. [a] -> [a] -> [a]
++ State
eventFacts) (Map Prp Bdd
changelaw Map Prp Bdd -> Prp -> Bdd
forall k a. Ord k => Map k a -> k -> a
! Prp
p)) State
changeprops ]
instance Update BelStruct Transformer where
checks :: [BelStruct -> Transformer -> Bool]
checks = [BelStruct -> Transformer -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents]
unsafeUpdate :: BelStruct -> Transformer -> BelStruct
unsafeUpdate BelStruct
bls Transformer
ctrf = State -> Bdd -> (Map Agent Int, RelBDD) -> BelStruct
BlS State
newprops Bdd
newlaw (Map Agent Int, RelBDD)
newobs where
(BlS State
newprops Bdd
newlaw (Map Agent Int, RelBDD)
newobs, State
_) = BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
unsafeUpdate (BelStruct
bls,State
forall a. HasCallStack => a
undefined::State) (Transformer
ctrf,State
forall a. HasCallStack => a
undefined::State)
instance Update BelScene MultipointedEvent where
unsafeUpdate :: BelScene -> MultipointedEvent -> BelScene
unsafeUpdate (BelStruct
bls,State
s) (Transformer
trfUnshifted, Bdd
eventFactsBddUnshifted) =
BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
update (BelStruct
bls,State
s) (Transformer
trf,State
selectedEventState) where
(trf :: Transformer
trf@(Trf State
addprops Form
addlaw Map Prp Bdd
_ (Map Agent Int, RelBDD)
_), [(Prp, Prp)]
shiftRel) = BelStruct -> Transformer -> (Transformer, [(Prp, Prp)])
shiftPrepare BelStruct
bls Transformer
trfUnshifted
eventFactsBdd :: Bdd
eventFactsBdd = [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftRel Bdd
eventFactsBddUnshifted
selectedEventState :: State
selectedEventState :: State
selectedEventState = ((Int, Bool) -> Prp) -> [(Int, Bool)] -> State
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prp
P (Int -> Prp) -> ((Int, Bool) -> Int) -> (Int, Bool) -> Prp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Bool) -> Int
forall a b. (a, b) -> a
fst) ([(Int, Bool)] -> State) -> [(Int, Bool)] -> State
forall a b. (a -> b) -> a -> b
$ ((Int, Bool) -> Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd [(Int, Bool)]
selectedEvent
selectedEvent :: [(Int, Bool)]
selectedEvent = case
[Int] -> Bdd -> [[(Int, Bool)]]
allSatsWith
((Prp -> Int) -> State -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum State
addprops)
(Bdd
eventFactsBdd Bdd -> Bdd -> Bdd
`con` Bdd -> [(Int, Bool)] -> Bdd
restrictSet (BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
addlaw) [ (Int
k, Int -> Prp
P Int
k Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` State
s) | P Int
k <- BelStruct -> State
forall a. HasVocab a => a -> State
vocabOf BelStruct
bls ])
of
[] -> Agent -> [(Int, Bool)]
forall a. HasCallStack => Agent -> a
error Agent
"no selected event"
[[(Int, Bool)]
this] -> [(Int, Bool)]
this
[[(Int, Bool)]]
more -> Agent -> [(Int, Bool)]
forall a. HasCallStack => Agent -> a
error (Agent -> [(Int, Bool)]) -> Agent -> [(Int, Bool)]
forall a b. (a -> b) -> a -> b
$ Agent
"too many selected events: " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ [[(Int, Bool)]] -> Agent
forall a. Show a => a -> Agent
show [[(Int, Bool)]]
more
trfPost :: Event -> Prp -> Bdd
trfPost :: Event -> Prp -> Bdd
trfPost (Trf State
addprops Form
_ Map Prp Bdd
changelaw (Map Agent Int, RelBDD)
_, State
x) Prp
p
| Prp
p Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map Prp Bdd -> State
forall k a. Map k a -> [k]
M.keys Map Prp Bdd
changelaw = Bdd -> Bdd -> Bdd
restrictLaw (Map Prp Bdd
changelaw Map Prp Bdd -> Prp -> Bdd
forall k a. Ord k => Map k a -> k -> a
! Prp
p) (State -> State -> Bdd
booloutof State
x State
addprops)
| Bool
otherwise = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF Prp
p
reduce :: Event -> Form -> Maybe Form
reduce :: Event -> Form -> Maybe Form
reduce Event
_ Form
Top = Form -> Maybe Form
forall a. a -> Maybe a
Just Form
Top
reduce Event
e Form
Bot = Form -> Maybe Form
forall a. a -> Maybe a
Just (Form -> Maybe Form) -> Form -> Maybe Form
forall a b. (a -> b) -> a -> b
$ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Event -> Form
forall a. HasPrecondition a => a -> Form
preOf Event
e
reduce Event
e (PrpF Prp
p) = Form -> Form -> Form
Impl (Event -> Form
forall a. HasPrecondition a => a -> Form
preOf Event
e) (Form -> Form) -> Maybe Form -> Maybe Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Form -> Maybe Form
forall a. a -> Maybe a
Just (Bdd -> Form
formOf (Bdd -> Form) -> Bdd -> Form
forall a b. (a -> b) -> a -> b
$ Event -> Prp -> Bdd
trfPost Event
e Prp
p)
reduce Event
e (Neg Form
f) = Form -> Form -> Form
Impl (Event -> Form
forall a. HasPrecondition a => a -> Form
preOf Event
e) (Form -> Form) -> (Form -> Form) -> Form -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
Neg (Form -> Form) -> Maybe Form -> Maybe Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Event -> Form -> Maybe Form
reduce Event
e Form
f
reduce Event
e (Conj [Form]
fs) = [Form] -> Form
Conj ([Form] -> Form) -> Maybe [Form] -> Maybe Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Form -> Maybe Form) -> [Form] -> Maybe [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Event -> Form -> Maybe Form
reduce Event
e) [Form]
fs
reduce Event
e (Disj [Form]
fs) = [Form] -> Form
Disj ([Form] -> Form) -> Maybe [Form] -> Maybe Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Form -> Maybe Form) -> [Form] -> Maybe [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Event -> Form -> Maybe Form
reduce Event
e) [Form]
fs
reduce Event
e (Xor [Form]
fs) = Form -> Form -> Form
Impl (Event -> Form
forall a. HasPrecondition a => a -> Form
preOf Event
e) (Form -> Form) -> ([Form] -> Form) -> [Form] -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> Form
Xor ([Form] -> Form) -> Maybe [Form] -> Maybe Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Form -> Maybe Form) -> [Form] -> Maybe [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Event -> Form -> Maybe Form
reduce Event
e) [Form]
fs
reduce Event
e (Impl Form
f1 Form
f2) = Form -> Form -> Form
Impl (Form -> Form -> Form) -> Maybe Form -> Maybe (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Event -> Form -> Maybe Form
reduce Event
e Form
f1 Maybe (Form -> Form) -> Maybe Form -> Maybe Form
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Event -> Form -> Maybe Form
reduce Event
e Form
f2
reduce Event
e (Equi Form
f1 Form
f2) = Form -> Form -> Form
Equi (Form -> Form -> Form) -> Maybe Form -> Maybe (Form -> Form)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Event -> Form -> Maybe Form
reduce Event
e Form
f1 Maybe (Form -> Form) -> Maybe Form -> Maybe Form
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Event -> Form -> Maybe Form
reduce Event
e Form
f2
reduce Event
_ (Forall State
_ Form
_) = Maybe Form
forall a. Maybe a
Nothing
reduce Event
_ (Exists State
_ Form
_) = Maybe Form
forall a. Maybe a
Nothing
reduce e :: Event
e@(t :: Transformer
t@(Trf State
addprops Form
_ Map Prp Bdd
_ (Map Agent Int
ags, RelBDD
eventObs)), State
x) (K Agent
a Form
f) =
Form -> Form -> Form
Impl (Event -> Form
forall a. HasPrecondition a => a -> Form
preOf Event
e) (Form -> Form) -> ([Form] -> Form) -> [Form] -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> Form
Conj ([Form] -> Form) -> Maybe [Form] -> Maybe Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe Form] -> Maybe [Form]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
[ Agent -> Form -> Form
K Agent
a (Form -> Form) -> Maybe Form -> Maybe Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Event -> Form -> Maybe Form
reduce (Transformer
t,State
y) Form
f | State
y <- State -> [State]
forall a. [a] -> [[a]]
powerset State
addprops
, State -> RelBDD -> Bool
forall a. TagBdd a => State -> Tagged a Bdd -> Bool
tagBddEval (Int -> State -> State
mv (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
x State -> State -> State
forall a. [a] -> [a] -> [a]
++ Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
y) (Bdd -> RelBDD
forall {k} (s :: k) b. b -> Tagged s b
Tagged (Bdd -> RelBDD) -> Bdd -> RelBDD
forall a b. (a -> b) -> a -> b
$ Bdd -> (Int, Bool) -> Bdd
restrict (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
eventObs) (Map Agent Int
ags Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
! Agent
a, Bool
True) :: Tagged Dubbel Bdd)
]
reduce Event
e (Kw Agent
a Form
f) = Event -> Form -> Maybe Form
reduce Event
e ([Form] -> Form
Disj [Agent -> Form -> Form
K Agent
a Form
f, Agent -> Form -> Form
K Agent
a (Form -> Form
Neg Form
f)])
reduce Event
_ Ck {} = Maybe Form
forall a. Maybe a
Nothing
reduce Event
_ Ckw {} = Maybe Form
forall a. Maybe a
Nothing
reduce e :: Event
e@(t :: Transformer
t@(Trf State
addprops Form
_ Map Prp Bdd
_ (Map Agent Int
ags, RelBDD
eventObs)), State
x) (Dk [Agent]
agents Form
f) =
Form -> Form -> Form
Impl (Event -> Form
forall a. HasPrecondition a => a -> Form
preOf Event
e) (Form -> Form) -> ([Form] -> Form) -> [Form] -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> Form
Conj ([Form] -> Form) -> Maybe [Form] -> Maybe Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe Form] -> Maybe [Form]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence
[[Agent] -> Form -> Form
Dk [Agent]
agents (Form -> Form) -> Maybe Form -> Maybe Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Event -> Form -> Maybe Form
reduce (Transformer
t, State
y) Form
f |
let omegai :: RelBDD
omegai
= Bdd -> RelBDD
forall {k} (s :: k) b. b -> Tagged s b
Tagged
(Bdd -> RelBDD) -> Bdd -> RelBDD
forall a b. (a -> b) -> a -> b
$ Bdd -> [(Int, Bool)] -> Bdd
restrictSet (RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag RelBDD
eventObs)
([(Int, Bool)] -> Bdd) -> [(Int, Bool)] -> Bdd
forall a b. (a -> b) -> a -> b
$ (Agent -> (Int, Bool)) -> [Agent] -> [(Int, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ Agent
a -> (Map Agent Int
ags Map Agent Int -> Agent -> Int
forall k a. Ord k => Map k a -> k -> a
! Agent
a, Agent
a Agent -> [Agent] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Agent]
agents)) ([Agent] -> [(Int, Bool)]) -> [Agent] -> [(Int, Bool)]
forall a b. (a -> b) -> a -> b
$ Map Agent Int -> [Agent]
forall k a. Map k a -> [k]
M.keys Map Agent Int
ags ::
Tagged Dubbel Bdd,
State
y <- State -> [State]
forall a. [a] -> [[a]]
powerset State
addprops,
State -> RelBDD -> Bool
forall a. TagBdd a => State -> Tagged a Bdd -> Bool
tagBddEval (Int -> State -> State
mv (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
x State -> State -> State
forall a. [a] -> [a] -> [a]
++ Int -> State -> State
cp (Map Agent Int -> Int
forall k a. Map k a -> Int
M.size Map Agent Int
ags) State
y) RelBDD
omegai]
reduce Event
e (Dkw [Agent]
ags Form
f) = Event -> Form -> Maybe Form
reduce Event
e ([Form] -> Form
Disj [[Agent] -> Form -> Form
Dk [Agent]
ags Form
f, [Agent] -> Form -> Form
Dk [Agent]
ags (Form -> Form
Neg Form
f)])
reduce Event
_ PubAnnounce {} = Maybe Form
forall a. Maybe a
Nothing
reduce Event
_ PubAnnounceW {} = Maybe Form
forall a. Maybe a
Nothing
reduce Event
_ Announce {} = Maybe Form
forall a. Maybe a
Nothing
reduce Event
_ AnnounceW {} = Maybe Form
forall a. Maybe a
Nothing
reduce Event
_ Dia {} = Maybe Form
forall a. Maybe a
Nothing
bddReduce :: BelScene -> Event -> Form -> Bdd
bddReduce :: BelScene -> Event -> Form -> Bdd
bddReduce scn :: BelScene
scn@(BelStruct
oldBls,State
_) event :: Event
event@(Trf State
addprops Form
_ Map Prp Bdd
changelaw (Map Agent Int, RelBDD)
_, State
eventFacts) Form
f =
let
changeprops :: State
changeprops = Map Prp Bdd -> State
forall k a. Map k a -> [k]
M.keys Map Prp Bdd
changelaw
shiftaddprops :: State
shiftaddprops = [(State -> Prp
freshp (State -> Prp) -> State -> Prp
forall a b. (a -> b) -> a -> b
$ BelScene -> State
forall a. HasVocab a => a -> State
vocabOf BelScene
scn)..]
shiftrel :: [(Prp, Prp)]
shiftrel = [(Prp, Prp)] -> [(Prp, Prp)]
forall a. Ord a => [a] -> [a]
sort ([(Prp, Prp)] -> [(Prp, Prp)]) -> [(Prp, Prp)] -> [(Prp, Prp)]
forall a b. (a -> b) -> a -> b
$ State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip State
addprops State
shiftaddprops
changelawShifted :: Map Prp Bdd
changelawShifted = (Bdd -> Bdd) -> Map Prp Bdd -> Map Prp Bdd
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ([(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftrel) Map Prp Bdd
changelaw
(BelStruct
newBlS,State
_) = BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
update BelScene
scn Event
event
actualAss :: [(Int, Bool)]
actualAss = [ (Int
shifted, Int -> Prp
P Int
orig Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` State
eventFacts) | (P Int
orig, P Int
shifted) <- [(Prp, Prp)]
shiftrel ]
postconrel :: [(Int, Bdd)]
postconrel = [ (Int
n, Map Prp Bdd
changelawShifted Map Prp Bdd -> Prp -> Bdd
forall k a. Ord k => Map k a -> k -> a
! Int -> Prp
P Int
n) | (P Int
n) <- State
changeprops ]
copychangeprops :: State
copychangeprops = [(State -> Prp
freshp (State -> Prp) -> State -> Prp
forall a b. (a -> b) -> a -> b
$ BelScene -> State
forall a. HasVocab a => a -> State
vocabOf BelScene
scn State -> State -> State
forall a. [a] -> [a] -> [a]
++ ((Prp, Prp) -> Prp) -> [(Prp, Prp)] -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Prp) -> Prp
forall a b. (a, b) -> b
snd [(Prp, Prp)]
shiftrel)..]
copyrelInverse :: [(Prp, Prp)]
copyrelInverse = State -> State -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip State
copychangeprops State
changeprops
in
Bdd -> Bdd -> Bdd
imp (BelStruct -> Form -> Bdd
bddOf BelStruct
oldBls (Event -> Form
forall a. HasPrecondition a => a -> Form
preOf Event
event)) (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$
[(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
copyrelInverse (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$
(Bdd -> [(Int, Bool)] -> Bdd
`restrictSet` [(Int, Bool)]
actualAss) (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$
[(Int, Bdd)] -> Bdd -> Bdd
substitSimul [(Int, Bdd)]
postconrel (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$
BelStruct -> Form -> Bdd
bddOf BelStruct
newBlS Form
f
evalViaBddReduce :: BelScene -> Event -> Form -> Bool
evalViaBddReduce :: BelScene -> Event -> Form -> Bool
evalViaBddReduce (BelStruct
bls,State
s) Event
event Form
f = Bdd -> (Int -> Bool) -> Bool
evaluateFun (BelScene -> Event -> Form -> Bdd
bddReduce (BelStruct
bls,State
s) Event
event Form
f) (\Int
n -> Int -> Prp
P Int
n Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` State
s)