{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables #-}

{- |

The implementation in "SMCDEL.Symbolic.S5" only works for models where the
epistemic accessibility relation is an equivalence relation.
This is because only those can be described by sets of observational variables.
In fact, not even every S5 relation on distinctly valuated worlds can be modeled with observational variables --- this is why our translation procedure `SMCDEL.Translation.S5` has to add additional atomic propositions.

To overcome this limitation, here we generalize the definition of knowledge structures.
Using well-known methods from temporal model checking, arbitrary relations can also be represented as BDDs.
See for example~\cite{GoroRyan02:BelRevBDD}.
Remember that in a knowledge structure we can identify states with boolean assignments and those are just sets of propositions.
Hence a relation on states with unique valuations can be seen as a relation between sets of propositions.
We can therefore represent it with the BDD of a characteristic function on a double vocabulary, as described in~\cite[Section 5.2]{ClarkeGrumbergPeled1999:MC}.
Intuitively, we construct (the BDD of) a formula which is true exactly for the pairs of boolean assignments that are connected by the relation.

Our symbolic model checker can then also be used for non-S5 models.

For further explanations, see~\cite[Section 8]{BEGS17:SMCDELbeyond}.

-}

module SMCDEL.Symbolic.K where

import Data.Tagged

import Control.Arrow ((&&&),first)
import Data.Dynamic (fromDynamic)
import Data.HasCacBDD hiding (Top,Bot)
import Data.List (delete,intercalate,sort,intersect,nub,(\\))
import qualified Data.Map.Strict as M
import Data.Map.Strict ((!))
import Test.QuickCheck

import SMCDEL.Explicit.K
import SMCDEL.Internal.Help (apply,lfp,powerset)
import SMCDEL.Internal.TexDisplay
import SMCDEL.Language
import SMCDEL.Other.BDD2Form
import SMCDEL.Symbolic.S5 (State,texBDD,boolBddOf,texBddWith,bddEval,relabelWith)
import SMCDEL.Translations.S5 (booloutof)

-- * Translating relations to type-safe BDDs

mvP, cpP :: Prp -> Prp
mvP :: Prp -> Prp
mvP (P Int
n) = Int -> Prp
P  (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
n)      -- represent p  in the double vocabulary
cpP :: Prp -> Prp
cpP (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
1) -- represent p' in the double vocabulary

-- | Map p or p' in double vocabulary to p in single vocabulary.
unmvcpP :: Prp -> Prp
unmvcpP :: Prp -> Prp
unmvcpP (P Int
m) | Int -> Bool
forall a. Integral a => a -> Bool
even Int
m    = Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ 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
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 :: [Prp] -> [Prp]
mv :: State -> State
mv = (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Prp
mvP
cp :: State -> State
cp = (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Prp
cpP

unmv, uncp :: [Prp] -> [Prp]
-- | Go from p in double vocabulary to p in single vocabulary.
unmv :: State -> State
unmv = (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Prp
f where
  f :: Prp -> Prp
f (P Int
m) | 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
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 :: State -> State
uncp = (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Prp
f where
  f :: Prp -> Prp
f (P Int
m) | 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
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 :: [Prp] -> RelBDD
allsamebdd :: State -> RelBDD
allsamebdd 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 (State -> State
mv State
ps) (State -> State
cp 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 :: Bdd -> RelBDD
cpBdd :: Bdd -> RelBDD
cpBdd 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
1) Bdd
b

mvBdd :: Bdd -> RelBDD
mvBdd :: Bdd -> RelBDD
mvBdd 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
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
*) Bdd
b

unmvBdd :: RelBDD -> Bdd
unmvBdd :: RelBDD -> Bdd
unmvBdd (Tagged Bdd
b) =
  (Int -> Int) -> Bdd -> Bdd
relabelFun (\Int
n -> if Int -> Bool
forall a. Integral a => a -> Bool
even Int
n then Int
n 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 Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"in the RelBDD " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Bdd -> Agent
forall a. Show a => a -> Agent
show Bdd
b)) Bdd
b

propRel2bdd :: [Prp] -> M.Map State [State] -> RelBDD
propRel2bdd :: State -> Map State [State] -> RelBDD
propRel2bdd State
props Map State [State]
relation = 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
disSet (Map State Bdd -> [Bdd]
forall k a. Map k a -> [a]
M.elems (Map State Bdd -> [Bdd]) -> Map State Bdd -> [Bdd]
forall a b. (a -> b) -> a -> b
$ (State -> [State] -> Bdd) -> Map State [State] -> Map State Bdd
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey State -> [State] -> Bdd
linkbdd Map State [State]
relation) where
  linkbdd :: State -> [State] -> Bdd
linkbdd State
here [State]
theres =
    Bdd -> Bdd -> Bdd
con (State -> State -> Bdd
booloutof (State -> State
mv State
here) (State -> State
mv State
props))
        ([Bdd] -> Bdd
disSet [ State -> State -> Bdd
booloutof (State -> State
cp State
there) (State -> State
cp State
props) | State
there <- [State]
theres ] )

samplerel ::  M.Map State [State]
samplerel :: Map State [State]
samplerel = [(State, [State])] -> Map State [State]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [
  ( []        , [ [],[Int -> Prp
P Int
1],[Int -> Prp
P Int
2],[Int -> Prp
P Int
1, Int -> Prp
P Int
2] ] ),
  ( [Int -> Prp
P Int
1]     , [    [Int -> Prp
P Int
1],      [Int -> Prp
P Int
1, Int -> Prp
P Int
2] ] ),
  ( [Int -> Prp
P Int
2]     , [    [Int -> Prp
P Int
2],      [Int -> Prp
P Int
1, Int -> Prp
P Int
2] ] ),
  ( [Int -> Prp
P Int
1, Int -> Prp
P Int
2], [                [Int -> Prp
P Int
1, Int -> Prp
P Int
2] ] )  ]


-- * Describing Kripke Models with BDDs

{- $
We now want to use BDDs to represent the relations of multiple agents
in a general Kripke Model. Suppose we have a model for the vocabulary
$V$ in which the valuation function assigns to every state a distinct
set of true propositions. To simplify the notation we also write $s$
for the set of propositions true at $s$.
-}

-- | Translate an agent's relation of worlds to a relation of sets of propositions.
-- The given model must have distinct valuations.
relBddOfIn :: Agent -> KripkeModel -> RelBDD
relBddOfIn :: Agent -> KripkeModel -> RelBDD
relBddOfIn Agent
i (KrM Map Int (Map Prp Bool, Map Agent [Int])
m)
  | Bool -> Bool
not (KripkeModel -> Bool
distinctVal (Map Int (Map Prp Bool, Map Agent [Int]) -> KripkeModel
KrM Map Int (Map Prp Bool, Map Agent [Int])
m)) = Agent -> RelBDD
forall a. HasCallStack => Agent -> a
error Agent
"m does not have distinct valuations."
  | Bool
otherwise = 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
disSet (Map Int Bdd -> [Bdd]
forall k a. Map k a -> [a]
M.elems (Map Int Bdd -> [Bdd]) -> Map Int Bdd -> [Bdd]
forall a b. (a -> b) -> a -> b
$ ((Map Prp Bool, Map Agent [Int]) -> Bdd)
-> Map Int (Map Prp Bool, Map Agent [Int]) -> Map Int Bdd
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Map Prp Bool, Map Agent [Int]) -> Bdd
linkbdd Map Int (Map Prp Bool, Map Agent [Int])
m) where
    linkbdd :: (Map Prp Bool, Map Agent [Int]) -> Bdd
linkbdd (Map Prp Bool
mapPropBool,Map Agent [Int]
mapAgentReach)  =
      Bdd -> Bdd -> Bdd
con
        (State -> State -> Bdd
booloutof (State -> State
mv State
here) (State -> State
mv State
props))
        ([Bdd] -> Bdd
disSet [ State -> State -> Bdd
booloutof (State -> State
cp State
there) (State -> State
cp State
props) | State
there<-[State]
theres ] )
      where
        props :: State
props = Map Prp Bool -> State
forall k a. Map k a -> [k]
M.keys Map Prp Bool
mapPropBool
        here :: State
here = Map Prp Bool -> State
forall k a. Map k a -> [k]
M.keys ((Bool -> Bool) -> Map Prp Bool -> Map Prp Bool
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter Bool -> Bool
forall a. a -> a
id Map Prp Bool
mapPropBool)
        theres :: [State]
theres = (Int -> State) -> [Int] -> [State]
forall a b. (a -> b) -> [a] -> [b]
map (KripkeModel -> Int -> State
truthsInAt (Map Int (Map Prp Bool, Map Agent [Int]) -> KripkeModel
KrM Map Int (Map Prp Bool, Map Agent [Int])
m)) (Map Agent [Int]
mapAgentReach Map Agent [Int] -> Agent -> [Int]
forall k a. Ord k => Map k a -> k -> a
! Agent
i)

-- * Belief Structures

data BelStruct = BlS [Prp]              -- vocabulary
                     Bdd                -- state law
                     (M.Map Agent 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 RelBDD
_) = State
voc

instance HasAgents BelStruct where
  agentsOf :: BelStruct -> [Agent]
agentsOf (BlS State
_ Bdd
_ Map Agent RelBDD
obdds) = Map Agent RelBDD -> [Agent]
forall k a. Map k a -> [k]
M.keys Map Agent RelBDD
obdds

-- | Given a formula, compute a BDD that is equivalent to that formula, on a given belief structure.
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 RelBDD
obdds) (K Agent
i Form
form) = RelBDD -> Bdd
unmvBdd 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
<$> Bdd -> RelBDD
cpBdd 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
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
<*> Bdd -> RelBDD
cpBdd (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
$ State -> State
cp State
allprops
  omegai :: RelBDD
omegai = Map Agent RelBDD
obdds Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
i

bddOf bls :: BelStruct
bls@(BlS State
allprops Bdd
lawbdd Map Agent RelBDD
obdds) (Kw Agent
i Form
form) = RelBDD -> Bdd
unmvBdd 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
<$> Bdd -> RelBDD
cpBdd 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
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
<*> Bdd -> RelBDD
cpBdd (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
$ State -> State
cp State
allprops
  omegai :: RelBDD
omegai = Map Agent RelBDD
obdds Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
i

bddOf bls :: BelStruct
bls@(BlS State
voc Bdd
lawbdd Map Agent 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
$ State -> State
cp State
voc
  lambda :: Bdd -> Bdd
  lambda :: Bdd -> Bdd
lambda Bdd
z = RelBDD -> Bdd
unmvBdd (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
<$> Bdd -> RelBDD
cpBdd 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 [Map Agent RelBDD
obdds Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
i | 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
<*>
          Bdd -> RelBDD
cpBdd (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 RelBDD
obdds) (Dk [Agent]
ags Form
form) = RelBDD -> Bdd
unmvBdd 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
<$> Bdd -> RelBDD
cpBdd 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
<*> Bdd -> RelBDD
cpBdd (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
$ State -> State
cp 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
$ (RelBDD -> Bdd -> Bdd) -> Bdd -> [RelBDD] -> Bdd
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> (RelBDD -> Bdd) -> RelBDD -> Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag) Bdd
top [Map Agent RelBDD
obdds Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
i | Agent
i <- [Agent]
ags]

bddOf bls :: BelStruct
bls@(BlS State
allprops Bdd
lawbdd Map Agent RelBDD
obdds) (Dkw [Agent]
ags Form
form) = RelBDD -> Bdd
unmvBdd 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
<$> Bdd -> RelBDD
cpBdd 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
<*> Bdd -> RelBDD
cpBdd (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
$ State -> State
cp 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
$ (RelBDD -> Bdd -> Bdd) -> Bdd -> [RelBDD] -> Bdd
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> (RelBDD -> Bdd) -> RelBDD -> Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag) Bdd
top [Map Agent RelBDD
obdds Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
i | Agent
i <- [Agent]
ags]

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 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 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 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 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 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 RelBDD
_),Bdd
statesBdd) Form
f =
    let a :: Bdd
a = Bdd
lawBdd Bdd -> Bdd -> Bdd
`imp` (Bdd
statesBdd Bdd -> Bdd -> Bdd
`imp` 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
props Bdd
lawbdd Map Agent RelBDD
obs) Form
psi =
    State -> Bdd -> Map Agent RelBDD -> BelStruct
BlS State
props (Bdd
lawbdd Bdd -> Bdd -> Bdd
`con` BelStruct -> Form -> Bdd
bddOf BelStruct
bls Form
psi) Map Agent 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 RelBDD
obdds) [Agent]
ags Form
psi = State -> Bdd -> Map Agent RelBDD -> BelStruct
BlS State
newprops Bdd
newlawbdd Map Agent 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 :: Map Agent RelBDD
newobdds  = (Agent -> RelBDD -> RelBDD) -> Map Agent RelBDD -> Map Agent RelBDD
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey Agent -> RelBDD -> RelBDD
newOfor Map Agent RelBDD
obdds
  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
<$> Bdd -> RelBDD
mvBdd (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
<*> Bdd -> RelBDD
cpBdd (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
<$> Bdd -> RelBDD
cpBdd (Int -> Bdd
var Int
k)) -- p_psi'

-- | Get all states of a knowledge structure.
statesOf :: BelStruct -> [State]
statesOf :: BelStruct -> [State]
statesOf (BlS State
allprops Bdd
lawbdd Map Agent 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

-- * Visualizing Belief Structures

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"

instance TexAble BelStruct where
  tex :: BelStruct -> Agent
tex (BlS State
props Bdd
lawbdd Map Agent RelBDD
obdds) = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Agent
" \\left( \n"
    , State -> Agent
forall a. TexAble a => a -> Agent
tex State
props, Agent
", "
    , Agent
bddprefix, Bdd -> Agent
texBDD Bdd
lawbdd, Agent
bddsuffix
    , Agent
", "
    , Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
", " [Agent]
obddstrings
    , Agent
" \\right) \n"
    ] where
        obddstrings :: [Agent]
obddstrings = ((Agent, RelBDD) -> Agent) -> [(Agent, RelBDD)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map ((Agent, Agent) -> Agent
bddstring ((Agent, Agent) -> Agent)
-> ((Agent, RelBDD) -> (Agent, Agent)) -> (Agent, RelBDD) -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Agent, RelBDD) -> Agent
forall a b. (a, b) -> a
fst ((Agent, RelBDD) -> Agent)
-> ((Agent, RelBDD) -> Agent) -> (Agent, RelBDD) -> (Agent, Agent)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (RelBDD -> Agent
texRelBDD (RelBDD -> Agent)
-> ((Agent, RelBDD) -> RelBDD) -> (Agent, RelBDD) -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Agent, RelBDD) -> RelBDD
forall a b. (a, b) -> b
snd))) (Map Agent RelBDD -> [(Agent, RelBDD)]
forall k a. Map k a -> [(k, a)]
M.toList Map Agent RelBDD
obdds)
        bddstring :: (Agent, Agent) -> Agent
bddstring (Agent
i,Agent
os) = Agent
"\\Omega_{\\text{" Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
i Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"}} = " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
bddprefix Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
os Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
bddsuffix

instance TexAble BelScene where
  tex :: BelScene -> Agent
tex (BelStruct
bls, State
state) = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Agent
" \\left( \n", BelStruct -> Agent
forall a. TexAble a => a -> Agent
tex BelStruct
bls, Agent
", ", State -> Agent
forall a. TexAble a => a -> Agent
tex State
state, Agent
" \\right) \n" ]

instance TexAble MultipointedBelScene where
  tex :: MultipointedBelScene -> Agent
tex (BelStruct
bls, Bdd
statesBdd) = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Agent
" \\left( \n"
    , BelStruct -> Agent
forall a. TexAble a => a -> Agent
tex BelStruct
bls Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
", "
    , Agent
" \\begin{array}{l} \\scalebox{0.4}{"
    , Bdd -> Agent
texBDD Bdd
statesBdd
    , Agent
"} \\end{array}\n "
    , Agent
" \\right)" ]

cleanupObsLaw :: BelScene -> BelScene
cleanupObsLaw :: BelScene -> BelScene
cleanupObsLaw (BlS State
vocab Bdd
law Map Agent RelBDD
obs, State
s) = (State -> Bdd -> Map Agent RelBDD -> BelStruct
BlS State
vocab Bdd
law ((RelBDD -> RelBDD) -> Map Agent RelBDD -> Map Agent RelBDD
forall a b k. (a -> b) -> Map k a -> Map k b
M.map RelBDD -> RelBDD
clean Map Agent RelBDD
obs), State
s) where
  clean :: RelBDD -> RelBDD
clean RelBDD
relbdd = Bdd -> Bdd -> Bdd
restrictLaw (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelBDD
relbdd Tagged Dubbel (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b.
Tagged Dubbel (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> RelBDD
cpBdd Bdd
law Tagged Dubbel (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b.
Tagged Dubbel (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bdd -> RelBDD
mvBdd Bdd
law)

determinedVocabOf :: BelStruct -> [Prp]
determinedVocabOf :: BelStruct -> State
determinedVocabOf BelStruct
strct = (Prp -> Bool) -> State -> State
forall a. (a -> Bool) -> [a] -> [a]
filter (\Prp
p -> BelStruct -> Form -> Bool
validViaBdd BelStruct
strct (Prp -> Form
PrpF Prp
p) Bool -> Bool -> Bool
|| BelStruct -> Form -> Bool
validViaBdd BelStruct
strct (Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF Prp
p)) (BelStruct -> State
forall a. HasVocab a => a -> State
vocabOf BelStruct
strct)

nonobsVocabOf  :: BelStruct -> [Prp]
nonobsVocabOf :: BelStruct -> State
nonobsVocabOf (BlS State
vocab Bdd
_law Map Agent RelBDD
obs) = (Prp -> Bool) -> State -> State
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp -> State -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` State
usedVars) State
vocab where
  usedVars :: State
usedVars =
    (Prp -> Prp) -> State -> State
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Prp
unmvcpP
    (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ State -> State
forall a. Ord a => [a] -> [a]
sort
    (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ State -> State
forall a. Eq a => [a] -> [a]
nub
    (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ (RelBDD -> State) -> [RelBDD] -> State
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Int -> Prp) -> [Int] -> State
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P ([Int] -> State) -> (RelBDD -> [Int]) -> RelBDD -> State
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> [Int]
Data.HasCacBDD.allVarsOf (Bdd -> [Int]) -> (RelBDD -> Bdd) -> RelBDD -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag)
    ([RelBDD] -> State) -> [RelBDD] -> State
forall a b. (a -> b) -> a -> b
$ Map Agent RelBDD -> [RelBDD]
forall k a. Map k a -> [a]
M.elems Map Agent RelBDD
obs

withoutProps :: [Prp] -> BelStruct -> BelStruct
withoutProps :: State -> BelStruct -> BelStruct
withoutProps State
propsToDel (BlS State
oldProps Bdd
oldLawBdd Map Agent RelBDD
oldObs) =
  State -> Bdd -> Map Agent RelBDD -> BelStruct
BlS
    (State
oldProps State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ State
propsToDel)
    ([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
propsToDel) Bdd
oldLawBdd)
    ((RelBDD -> RelBDD) -> Map Agent RelBDD -> Map Agent RelBDD
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b. (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bdd -> Bdd) -> RelBDD -> RelBDD)
-> (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b. (a -> b) -> a -> b
$ [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
propsToDel)) Map Agent RelBDD
oldObs)

equivExtraVocabOf :: [Prp] -> BelStruct -> [(Prp,Prp)]
equivExtraVocabOf :: State -> BelStruct -> [(Prp, Prp)]
equivExtraVocabOf State
mainVocab BelStruct
bls =
  [ (Prp
p,Prp
q) | Prp
p <- BelStruct -> State
forall a. HasVocab a => a -> State
vocabOf BelStruct
bls State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ State
mainVocab, Prp
q <- BelStruct -> State
forall a. HasVocab a => a -> State
vocabOf BelStruct
bls, Prp
p Prp -> Prp -> Bool
forall a. Ord a => a -> a -> Bool
> Prp
q, BelStruct -> Form -> Bool
validViaBdd BelStruct
bls (Prp -> Form
PrpF Prp
p Form -> Form -> Form
`Equi` Prp -> Form
PrpF Prp
q) ]

replaceWithIn :: (Prp,Prp) -> BelStruct -> BelStruct
replaceWithIn :: (Prp, Prp) -> BelStruct -> BelStruct
replaceWithIn (Prp
p,Prp
q) (BlS State
oldProps Bdd
oldLaw Map Agent RelBDD
oldObs) =
  State -> Bdd -> Map Agent RelBDD -> BelStruct
BlS (Prp -> State -> State
forall a. Eq a => a -> [a] -> [a]
delete Prp
p State
oldProps) (Bdd -> Bdd
changeBdd Bdd
oldLaw) ((RelBDD -> RelBDD) -> Map Agent RelBDD -> Map Agent RelBDD
forall a b. (a -> b) -> Map Agent a -> Map Agent b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b. (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bdd -> Bdd
changeRelBdd) Map Agent RelBDD
oldObs) where
  changeBdd :: Bdd -> Bdd
changeBdd    = [(Int, Int)] -> Bdd -> Bdd
Data.HasCacBDD.relabel [ (Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
p, Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
q) ]
  changeRelBdd :: Bdd -> Bdd
changeRelBdd = [(Int, Int)] -> Bdd -> Bdd
Data.HasCacBDD.relabel ([(Int, Int)] -> Bdd -> Bdd) -> [(Int, Int)] -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ [(Int, Int)] -> [(Int, Int)]
forall a. Ord a => [a] -> [a]
sort [ (Prp -> Int
forall a. Enum a => a -> Int
fromEnum (Prp -> Int) -> Prp -> Int
forall a b. (a -> b) -> a -> b
$ Prp -> Prp
mvP Prp
p, Prp -> Int
forall a. Enum a => a -> Int
fromEnum (Prp -> Int) -> Prp -> Int
forall a b. (a -> b) -> a -> b
$ Prp -> Prp
mvP Prp
q)
                                               , (Prp -> Int
forall a. Enum a => a -> Int
fromEnum (Prp -> Int) -> Prp -> Int
forall a b. (a -> b) -> a -> b
$ Prp -> Prp
cpP Prp
p, Prp -> Int
forall a. Enum a => a -> Int
fromEnum (Prp -> Int) -> Prp -> Int
forall a b. (a -> b) -> a -> b
$ Prp -> Prp
cpP Prp
q) ]

replaceEquivExtra :: [Prp] -> BelStruct -> (BelStruct,[(Prp,Prp)])
replaceEquivExtra :: State -> BelStruct -> (BelStruct, [(Prp, Prp)])
replaceEquivExtra State
mainVocab BelStruct
startBls = ((BelStruct, [(Prp, Prp)]) -> (BelStruct, [(Prp, Prp)]))
-> (BelStruct, [(Prp, Prp)]) -> (BelStruct, [(Prp, Prp)])
forall a. Eq a => (a -> a) -> a -> a
lfp (BelStruct, [(Prp, Prp)]) -> (BelStruct, [(Prp, Prp)])
step (BelStruct
startBls,[]) where
  step :: (BelStruct, [(Prp, Prp)]) -> (BelStruct, [(Prp, Prp)])
step (BelStruct
bls,[(Prp, Prp)]
replRel) = case State -> BelStruct -> [(Prp, Prp)]
equivExtraVocabOf State
mainVocab BelStruct
bls of
               []        -> (BelStruct
bls,[(Prp, Prp)]
replRel)
               ((Prp
p,Prp
q):[(Prp, Prp)]
_) -> ((Prp, Prp) -> BelStruct -> BelStruct
replaceWithIn (Prp
p,Prp
q) BelStruct
bls, (Prp
p,Prp
q)(Prp, Prp) -> [(Prp, Prp)] -> [(Prp, Prp)]
forall a. a -> [a] -> [a]
:[(Prp, Prp)]
replRel)

instance Optimizable BelStruct where
  optimize :: State -> BelStruct -> BelStruct
optimize State
myVocab BelStruct
bls = (BelStruct, [(Prp, Prp)]) -> BelStruct
forall a b. (a, b) -> a
fst ((BelStruct, [(Prp, Prp)]) -> BelStruct)
-> (BelStruct, [(Prp, Prp)]) -> BelStruct
forall a b. (a -> b) -> a -> b
$ State -> BelStruct -> (BelStruct, [(Prp, Prp)])
replaceEquivExtra State
myVocab (BelStruct -> (BelStruct, [(Prp, Prp)]))
-> BelStruct -> (BelStruct, [(Prp, Prp)])
forall a b. (a -> b) -> a -> b
$
    State -> BelStruct -> BelStruct
withoutProps ((BelStruct -> State
determinedVocabOf BelStruct
bls State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
`intersect` BelStruct -> State
nonobsVocabOf BelStruct
bls) State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ State
myVocab) BelStruct
bls

instance Optimizable MultipointedBelScene where
  optimize :: State -> MultipointedBelScene -> MultipointedBelScene
optimize State
myVocab (BelStruct
oldBls,Bdd
oldStatesBdd) = (BelStruct
newKns,Bdd
newStatesBdd) where
    intermediateBls :: BelStruct
intermediateBls = State -> BelStruct -> BelStruct
withoutProps ((BelStruct -> State
determinedVocabOf BelStruct
oldBls State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
`intersect` BelStruct -> State
nonobsVocabOf BelStruct
oldBls) State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ State
myVocab) BelStruct
oldBls
    removedProps :: State
removedProps = BelStruct -> State
forall a. HasVocab a => a -> State
vocabOf BelStruct
oldBls State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ BelStruct -> State
forall a. HasVocab a => a -> State
vocabOf BelStruct
intermediateBls
    intermediateStatesBdd :: Bdd
intermediateStatesBdd = [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
removedProps) Bdd
oldStatesBdd
    (BelStruct
newKns,[(Prp, Prp)]
replRel) = State -> BelStruct -> (BelStruct, [(Prp, Prp)])
replaceEquivExtra State
myVocab BelStruct
intermediateBls
    newStatesBdd :: Bdd
newStatesBdd = [(Int, Int)] -> Bdd -> Bdd
Data.HasCacBDD.relabel [ (Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
p, Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
q) | (Prp
p,Prp
q) <-[(Prp, Prp)]
replRel ] Bdd
intermediateStatesBdd

instance Arbitrary BelStruct where
  arbitrary :: Gen BelStruct
arbitrary = do
    Int
numExtraVars <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0,Int
2)
    let myVocabulary :: State
myVocabulary = State
defaultVocabulary State -> State -> State
forall a. [a] -> [a] -> [a]
++ Int -> State -> State
forall a. Int -> [a] -> [a]
take Int
numExtraVars [State -> Prp
freshp State
defaultVocabulary ..]
    (BF Form
statelaw) <- (Int -> Gen BF) -> Gen BF
forall a. (Int -> Gen a) -> Gen a
sized (State -> Int -> Gen BF
randomboolformWith State
myVocabulary) Gen BF -> (BF -> Bool) -> Gen BF
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\(BF Form
bf) -> Form -> Bdd
boolBddOf Form
bf Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
/= Bdd
bot)
    [(Agent, RelBDD)]
obs <- (Agent -> Gen (Agent, RelBDD)) -> [Agent] -> Gen [(Agent, RelBDD)]
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 (\Agent
i -> do
      BF Form
obsLaw <- (Int -> Gen BF) -> Gen BF
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen BF) -> Gen BF) -> (Int -> Gen BF) -> Gen BF
forall a b. (a -> b) -> a -> b
$ State -> Int -> Gen BF
randomboolformWith (State -> State
forall a. Ord a => [a] -> [a]
sort (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ State -> State
mv State
myVocabulary State -> State -> State
forall a. [a] -> [a] -> [a]
++ State -> State
cp State
myVocabulary) -- FIXME should rather be a random BDD?
      (Agent, RelBDD) -> Gen (Agent, RelBDD)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Agent
i,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
obsLaw)
      ) [Agent]
defaultAgents
    BelStruct -> Gen BelStruct
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (BelStruct -> Gen BelStruct) -> BelStruct -> Gen BelStruct
forall a b. (a -> b) -> a -> b
$ State -> Bdd -> Map Agent RelBDD -> BelStruct
BlS State
myVocabulary (Form -> Bdd
boolBddOf Form
statelaw) ([(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent, RelBDD)]
obs)
  shrink :: BelStruct -> [BelStruct]
shrink BelStruct
bls = [ State -> BelStruct -> BelStruct
withoutProps [Prp
p] BelStruct
bls | State -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (BelStruct -> State
forall a. HasVocab a => a -> State
vocabOf BelStruct
bls) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1, Prp
p <- BelStruct -> State
forall a. HasVocab a => a -> State
vocabOf BelStruct
bls State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ State
defaultVocabulary ]

data Transformer = Trf
  [Prp] -- addprops
  Form  -- addlaw
  (M.Map Prp Bdd) -- changelaw
  (M.Map Agent 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)

noChange :: ([Prp] -> Form -> M.Map Prp Bdd -> M.Map Agent RelBDD -> Transformer)
          -> [Prp] -> Form                  -> M.Map Agent RelBDD -> Transformer
noChange :: (State -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer)
-> State -> Form -> Map Agent RelBDD -> Transformer
noChange State -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
kntrf State
addprops Form
addlaw = State -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
kntrf State
addprops Form
addlaw Map Prp Bdd
forall k a. Map k a
M.empty

instance HasAgents Transformer where
  agentsOf :: Transformer -> [Agent]
agentsOf (Trf State
_ Form
_ Map Prp Bdd
_ Map Agent RelBDD
obdds) = Map Agent RelBDD -> [Agent]
forall k a. Map k a -> [k]
M.keys Map Agent RelBDD
obdds

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 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 Bdd
type MultipointedEvent = (Transformer,Bdd)

instance HasPrecondition MultipointedEvent where
  preOf :: MultipointedEvent -> Form
preOf (Trf State
addprops Form
addlaw Map Prp Bdd
_ Map Agent 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 ])

instance TexAble Transformer where
  tex :: Transformer -> Agent
tex (Trf State
addprops Form
addlaw Map Prp Bdd
changelaw Map Agent RelBDD
eventObs) = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Agent
" \\left( \n"
    , State -> Agent
forall a. TexAble a => a -> Agent
tex State
addprops, Agent
", "
    , Form -> Agent
forall a. TexAble a => a -> Agent
tex Form
addlaw, Agent
", "
    , State -> Agent
forall a. TexAble a => a -> Agent
tex State
changeprops, Agent
", "
    , Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
", " ([Agent] -> Agent) -> [Agent] -> Agent
forall a b. (a -> b) -> a -> b
$ ((Prp, Agent) -> Agent) -> [(Prp, Agent)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Agent) -> Agent
forall a b. (a, b) -> b
snd ([(Prp, Agent)] -> [Agent])
-> (Map Prp Agent -> [(Prp, Agent)]) -> Map Prp Agent -> [Agent]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Prp Agent -> [(Prp, Agent)]
forall k a. Map k a -> [(k, a)]
M.toList (Map Prp Agent -> [Agent]) -> Map Prp Agent -> [Agent]
forall a b. (a -> b) -> a -> b
$ (Prp -> Bdd -> Agent) -> Map Prp Bdd -> Map Prp Agent
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey Prp -> Bdd -> Agent
forall {a}. TexAble a => a -> Bdd -> Agent
texChange Map Prp Bdd
changelaw, Agent
", "
    , Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
", " [Agent]
eobddstrings
    , Agent
" \\right) \n"
    ] where
        changeprops :: State
changeprops = Map Prp Bdd -> State
forall k a. Map k a -> [k]
M.keys Map Prp Bdd
changelaw
        texChange :: a -> Bdd -> Agent
texChange a
prop Bdd
changebdd = a -> Agent
forall a. TexAble a => a -> Agent
tex a
prop Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
" := " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Form -> Agent
forall a. TexAble a => a -> Agent
tex (Bdd -> Form
formOf Bdd
changebdd)
        eobddstrings :: [Agent]
eobddstrings = ((Agent, RelBDD) -> Agent) -> [(Agent, RelBDD)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map ((Agent, Agent) -> Agent
bddstring ((Agent, Agent) -> Agent)
-> ((Agent, RelBDD) -> (Agent, Agent)) -> (Agent, RelBDD) -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Agent, RelBDD) -> Agent
forall a b. (a, b) -> a
fst ((Agent, RelBDD) -> Agent)
-> ((Agent, RelBDD) -> Agent) -> (Agent, RelBDD) -> (Agent, Agent)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& (RelBDD -> Agent
texRelBDD (RelBDD -> Agent)
-> ((Agent, RelBDD) -> RelBDD) -> (Agent, RelBDD) -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Agent, RelBDD) -> RelBDD
forall a b. (a, b) -> b
snd))) (Map Agent RelBDD -> [(Agent, RelBDD)]
forall k a. Map k a -> [(k, a)]
M.toList Map Agent RelBDD
eventObs)
        bddstring :: (Agent, Agent) -> Agent
bddstring (Agent
i,Agent
os) = Agent
"\\Omega^+_{\\text{" Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
i Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
"}} = " Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
bddprefix Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
os Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
bddsuffix

instance TexAble Event where
  tex :: Event -> Agent
tex (Transformer
trf, State
eventFacts) = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Agent
" \\left( \n", Transformer -> Agent
forall a. TexAble a => a -> Agent
tex Transformer
trf, Agent
", ", State -> Agent
forall a. TexAble a => a -> Agent
tex State
eventFacts, Agent
" \\right) \n" ]

instance TexAble MultipointedEvent where
  tex :: MultipointedEvent -> Agent
tex (Transformer
trf, Bdd
eventStates) = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Agent
" \\left( \n"
    , Transformer -> Agent
forall a. TexAble a => a -> Agent
tex Transformer
trf Agent -> Agent -> Agent
forall a. [a] -> [a] -> [a]
++ Agent
", \\ "
    , Agent
" \\begin{array}{l} \\scalebox{0.4}{"
    , Bdd -> Agent
texBDD Bdd
eventStates
    , Agent
"} \\end{array}\n "
    , Agent
" \\right)" ]

-- | 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 RelBDD
_) (Trf State
addprops Form
addlaw Map Prp Bdd
changelaw Map Agent RelBDD
eventObs) =
  (State -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
Trf State
shiftaddprops Form
addlawShifted Map Prp Bdd
changelawShifted Map Agent RelBDD
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 (State -> State
mv State
addprops) (State -> State
mv 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 (State -> State
cp State
addprops) (State -> State
cp State
shiftaddprops)
    eventObsShifted :: Map Agent RelBDD
eventObsShifted  = (RelBDD -> RelBDD) -> Map Agent RelBDD -> Map Agent RelBDD
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b. (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bdd -> Bdd) -> RelBDD -> RelBDD)
-> (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b. (a -> b) -> a -> b
$ [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftrelMVCP) Map Agent RelBDD
eventObs

instance Update BelScene Event where
  unsafeUpdate :: BelScene -> Event -> BelScene
unsafeUpdate (bls :: BelStruct
bls@(BlS State
props Bdd
law Map Agent RelBDD
obdds),State
s) (Transformer
trf, State
eventFactsUnshifted) = (State -> Bdd -> Map Agent RelBDD -> BelStruct
BlS State
newprops Bdd
newlaw Map Agent RelBDD
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 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 (State -> State
mv State
changeprops) (State -> State
mv 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 (State -> State
cp State
changeprops) (State -> State
cp 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 :: Map Agent RelBDD
newobs = (Agent -> RelBDD -> RelBDD) -> Map Agent RelBDD -> Map Agent RelBDD
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (\Agent
i RelBDD
oldobs -> (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) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RelBDD
oldobs) 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
<*> (Map Agent RelBDD
addObs Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
i)) Map Agent RelBDD
obdds
    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 RelBDD -> BelStruct
BlS State
newprops Bdd
newlaw Map Agent RelBDD
newobs where
    (BlS State
newprops Bdd
newlaw Map Agent 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 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

-- TODO: test this!
instance Update MultipointedBelScene MultipointedEvent where
  checks :: [MultipointedBelScene -> MultipointedEvent -> Bool]
checks = [MultipointedBelScene -> MultipointedEvent -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents] -- no need to check precondition, we allow an empty set of actual states
  unsafeUpdate :: MultipointedBelScene -> MultipointedEvent -> MultipointedBelScene
unsafeUpdate (bls :: BelStruct
bls@(BlS State
props Bdd
_ Map Agent RelBDD
_),Bdd
statesBdd) (Transformer
trfUnshifted, Bdd
eventsBddUnshifted) =
    (BelStruct
newBls, Bdd
newStatesBdd) where
      -- shiftPrepare first to ensure that eventsBdd is also shifted
      (trf :: Transformer
trf@(Trf State
addprops Form
_ Map Prp Bdd
changelaw Map Agent RelBDD
_), [(Prp, Prp)]
shiftRel) = BelStruct -> Transformer -> (Transformer, [(Prp, Prp)])
shiftPrepare BelStruct
bls Transformer
trfUnshifted
      eventsBdd :: Bdd
eventsBdd = [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftRel Bdd
eventsBddUnshifted
      (BelStruct
newBls, State
_) = BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
unsafeUpdate (BelStruct
bls,State
forall a. HasCallStack => a
undefined::State) (Transformer
trf,State
forall a. HasCallStack => a
undefined::State) -- using laziness!
      -- the actual event:
      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)..]
      newStatesBdd :: Bdd
newStatesBdd = [Bdd] -> Bdd
conSet [ [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
copyrel Bdd
statesBdd, Bdd
eventsBdd ]

trfPost :: Event -> Prp -> Bdd
trfPost :: Event -> Prp -> Bdd
trfPost (Trf State
addprops Form
_ Map Prp Bdd
changelaw Map Agent 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 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 is this a bit much?
                             , State -> RelBDD -> Bool
forall a. TagBdd a => State -> Tagged a Bdd -> Bool
tagBddEval (State -> State
mv State
x State -> State -> State
forall a. [a] -> [a] -> [a]
++ State -> State
cp State
y) (Map Agent RelBDD
eventObs Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
a)
    ]
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 RelBDD
eventObs), State
x) (Dk [Agent]
ags 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]
ags (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
$ (RelBDD -> Bdd -> Bdd) -> Bdd -> [RelBDD] -> Bdd
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> (RelBDD -> Bdd) -> RelBDD -> Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelBDD -> Bdd
forall {k} (s :: k) b. Tagged s b -> b
untag) Bdd
top [Map Agent RelBDD
eventObs Map Agent RelBDD -> Agent -> RelBDD
forall k a. Ord k => Map k a -> k -> a
! Agent
i | Agent
i <- [Agent]
ags] :: RelBDD,
       State
y <- State -> [State]
forall a. [a] -> [[a]]
powerset State
addprops,
       State -> RelBDD -> Bool
forall a. TagBdd a => State -> Tagged a Bdd -> Bool
tagBddEval (State -> State
mv State
x State -> State -> State
forall a. [a] -> [a] -> [a]
++ State -> State
cp 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 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)