{-# 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)     -- represent p  in the double vocabulary
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) -- represent p' in the double vocabulary

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]
-- | Go from p in double vocabulary to p in single vocabulary.
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
-- | Go from p' in double vocabulary to p in single vocabulary.
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]              -- vocabulary
                     Bdd                -- state law
                     (M.Map Agent Int, RelBDD) -- observation laws
                  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)                    -- 5. Prefix with "precon AND ..." (diamond!)
    (Bdd -> Bdd) -> (Form -> Bdd) -> Form -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
copyrelInverse              -- 4. Copy back changeProps V_-^o to V_-
    (Bdd -> Bdd) -> (Form -> Bdd) -> Form -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> Bdd
simulateActualEvents                    -- 3. Simulate actual event(s) [see below]
    (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)       -- 2. Replace changeProps V_- with postcons
                   | p :: Prp
p@(P Int
k) <- State
changeProps]  --    (no "relabelWith copyrel", undone in 4)
    (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)                -- 1. boolean equivalent wrt new struct
    (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
        -- 3. For a single pointed event, simulate actual event x outof V+
        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
          -- 3. For a multipointed event, simulate a set of actual events by ...
          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)  -- ... replacing addProps with assigments
                (Bdd -> Bdd) -> (Bdd -> Bdd) -> Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> Bdd -> Bdd
con Bdd
actualsBdd                   -- ... that satisfy 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)           -- ... and a precondition.
              ) 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 = [ ] -- unpointed structures can be updated with anything
  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)) -- p_psi'

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"

-- TODO: Optimization of Ki structures

-- TODO: Generating Arbitrary Ki structures

data Transformer = Trf
  [Prp] -- addprops
  Form  -- event law
  (M.Map Prp Bdd) -- changelaw
  (M.Map Agent Int, RelBDD) -- eventObs
  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 ])

-- TODO: TexAble Transformer

-- | shift addprops to ensure that props and newprops are disjoint:
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
    -- apply the shifting to addlaw, changelaw and eventObs:
    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
    -- to shift addObs we need shiftrel in the double vocabulary:
    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
    -- PART 1: SHIFTING addprops to ensure props and newprops are disjoint
    (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
    -- the actual event:
    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
    -- PART 2: COPYING the modified propositions
    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)
    -- PART 3: actual transformation
    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) -- using laziness!

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 -- FIXME this is inefficient
                             , 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
    -- same as in 'transform', to ensure props and addprops are disjoint
    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
    -- apply the shifting to addlaw and changelaw:
    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
    -- the actual event, shifted
    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 ]
    -- reversing V^o to V
    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
$ -- 0. check if precondition holds
      [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
copyrelInverse (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$     -- 4. changepropscopies -> original changeprops
        (Bdd -> [(Int, Bool)] -> Bdd
`restrictSet` [(Int, Bool)]
actualAss) (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$    -- 3. restrict to actual event x outof V+
          [(Int, Bdd)] -> Bdd -> Bdd
substitSimul [(Int, Bdd)]
postconrel (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$    -- 2. replace changeprops with postconditions
            BelStruct -> Form -> Bdd
bddOf BelStruct
newBlS Form
f             -- 1. boolean equivalent wrt new structure

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)