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

{- | In this module we define a symbolic represenation of Kripke models, called knoweldge structures.
To represent Boolean functions we use the CacBDD library via the Haskell bindings HasCacBDD.
An alternative to this module here is `SMCDEL.Symbolic.S5_CUDD` which uses CUDD instead of CacBDD.
-}

module SMCDEL.Symbolic.S5 where

import Control.Arrow (first,second,(***))
import Data.Char (isSpace)
import Data.Dynamic
import Data.HasCacBDD hiding (Top,Bot)
import Data.HasCacBDD.Visuals
import Data.List ((\\),delete,dropWhileEnd,intercalate,intersect,nub,sort)
import Data.Tagged
import System.Directory (findExecutable)
import System.IO (hPutStr, hGetContents, hClose)
import System.IO.Unsafe (unsafePerformIO)
import System.Process (runInteractiveCommand)
import Test.QuickCheck

import SMCDEL.Internal.Help ((!),alleqWith,apply,applyPartial,lfp,powerset,rtc,seteq)
import SMCDEL.Internal.TaggedBDD
import SMCDEL.Internal.TexDisplay
import SMCDEL.Language
import SMCDEL.Other.BDD2Form

-- * Boolean Reasoning

-- | Translate a Boolean formula to a BDD.
-- The function will raise an error if it is given an epistemic or dynamic formula.
boolBddOf :: Form -> Bdd
boolBddOf :: Form -> Bdd
boolBddOf Form
Top           = Bdd
top
boolBddOf Form
Bot           = Bdd
bot
boolBddOf (PrpF (P Int
n))  = Int -> Bdd
var Int
n
boolBddOf (Neg Form
form)    = Bdd -> Bdd
neg(Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ Form -> Bdd
boolBddOf Form
form
boolBddOf (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 Form -> Bdd
boolBddOf [Form]
forms
boolBddOf (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 Form -> Bdd
boolBddOf [Form]
forms
boolBddOf (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 Form -> Bdd
boolBddOf [Form]
forms
boolBddOf (Impl Form
f Form
g)    = Bdd -> Bdd -> Bdd
imp (Form -> Bdd
boolBddOf Form
f) (Form -> Bdd
boolBddOf Form
g)
boolBddOf (Equi Form
f Form
g)    = Bdd -> Bdd -> Bdd
equ (Form -> Bdd
boolBddOf Form
f) (Form -> Bdd
boolBddOf Form
g)
boolBddOf (Forall [Prp]
ps Form
f) = [Int] -> Bdd -> Bdd
forallSet ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
ps) (Form -> Bdd
boolBddOf Form
f)
boolBddOf (Exists [Prp]
ps Form
f) = [Int] -> Bdd -> Bdd
existsSet ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
ps) (Form -> Bdd
boolBddOf Form
f)
boolBddOf Form
_             = Agent -> Bdd
forall a. HasCallStack => Agent -> a
error Agent
"boolBddOf failed: Not a boolean formula."

-- | Given a set of true atomic propositions, evaluate a Boolean formula.
boolEvalViaBdd :: [Prp] -> Form -> Bool
boolEvalViaBdd :: [Prp] -> Form -> Bool
boolEvalViaBdd [Prp]
truths = [Prp] -> Bdd -> Bool
bddEval [Prp]
truths (Bdd -> Bool) -> (Form -> Bdd) -> Form -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Bdd
boolBddOf

-- | Given a set of true atomic propositions, evaluate a BDD.
bddEval :: [Prp] -> Bdd -> Bool
bddEval :: [Prp] -> Bdd -> Bool
bddEval [Prp]
truths Bdd
querybdd = Bdd -> (Int -> Bool) -> Bool
evaluateFun Bdd
querybdd (\Int
n -> Int -> Prp
P Int
n Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
truths)

-- | Size of a BDD, also counting terminal nodes (which CacBDD does not).
size :: Bdd -> Int
size :: Bdd -> Int
size Bdd
b = if Bdd -> Int
sizeOf Bdd
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Bdd -> Int
sizeOf Bdd
b Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 else Bdd -> Int
sizeOf Bdd
b Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2

-- | Given a mapping between atomic propositions, relabel them inside a BDD.
relabelWith :: [(Prp,Prp)] -> Bdd -> Bdd
relabelWith :: [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
r = [(Int, Int)] -> Bdd -> Bdd
relabel ([(Int, Int)] -> [(Int, Int)]
forall a. Ord a => [a] -> [a]
sort ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ ((Prp, Prp) -> (Int, Int)) -> [(Prp, Prp)] -> [(Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Prp -> Int
forall a. Enum a => a -> Int
fromEnum (Prp -> Int) -> (Prp -> Int) -> (Prp, Prp) -> (Int, Int)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Prp -> Int
forall a. Enum a => a -> Int
fromEnum) [(Prp, Prp)]
r)

-- * Knowledge Structures

{- | Knowledge structures are a compact representation of S5 Kripke models.
Their set of states is defined by a Boolean formula. Instead of accessibility relations we use observational variables.
Formal proofs that knowledge structures are indeed equivalent to S5 Kripke models can be found in the references from the Readme.
-}

-- | A /knowledge structure/ is a tuple \(\mathcal{F} = (V,\theta,O_1,\dots,O_n)\) where
-- \(V\) is the /vocabulary/, a finite set of propositional variables,
-- \(\theta\) is the /state law/, a Boolean formula over $V$ (represented as its BDD) and
-- for each agent \(i\), we have /observational variables/ \(O_i \subseteq V\).
data KnowStruct = KnS [Prp]            -- vocabulary
                      Bdd              -- state law
                      [(Agent,[Prp])]  -- observational variables
                    deriving (KnowStruct -> KnowStruct -> Bool
(KnowStruct -> KnowStruct -> Bool)
-> (KnowStruct -> KnowStruct -> Bool) -> Eq KnowStruct
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: KnowStruct -> KnowStruct -> Bool
== :: KnowStruct -> KnowStruct -> Bool
$c/= :: KnowStruct -> KnowStruct -> Bool
/= :: KnowStruct -> KnowStruct -> Bool
Eq,Int -> KnowStruct -> ShowS
[KnowStruct] -> ShowS
KnowStruct -> Agent
(Int -> KnowStruct -> ShowS)
-> (KnowStruct -> Agent)
-> ([KnowStruct] -> ShowS)
-> Show KnowStruct
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> KnowStruct -> ShowS
showsPrec :: Int -> KnowStruct -> ShowS
$cshow :: KnowStruct -> Agent
show :: KnowStruct -> Agent
$cshowList :: [KnowStruct] -> ShowS
showList :: [KnowStruct] -> ShowS
Show)

-- | A /state/ of \(\mathcal{F}\) is a list of true atomic propositions.
-- It should satisfy \(\theta\).
type State = [Prp]

instance Pointed KnowStruct State

-- | A pair $(\mathcal{F},s)$ where $s$ is a state of $\mathcal{F}$, is a /scene/.
type KnowScene = (KnowStruct,State)

instance Pointed KnowStruct Bdd
type MultipointedKnowScene = (KnowStruct,Bdd)

-- | Given a knowledge structure, generate the finite list of its states.
statesOf :: KnowStruct -> [State]
statesOf :: KnowStruct -> [[Prp]]
statesOf (KnS [Prp]
props Bdd
lawbdd [(Agent, [Prp])]
_) = ([(Prp, Bool)] -> [Prp]) -> [[(Prp, Bool)]] -> [[Prp]]
forall a b. (a -> b) -> [a] -> [b]
map ([Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort([Prp] -> [Prp])
-> ([(Prp, Bool)] -> [Prp]) -> [(Prp, Bool)] -> [Prp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[(Prp, Bool)] -> [Prp]
forall {b}. [(b, Bool)] -> [b]
translate) [[(Prp, Bool)]]
resultlists where
  resultlists :: [[(Prp, Bool)]]
  resultlists :: [[(Prp, Bool)]]
resultlists = (Assignment -> [(Prp, Bool)]) -> [Assignment] -> [[(Prp, Bool)]]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Bool) -> (Prp, Bool)) -> Assignment -> [(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)) ([Assignment] -> [[(Prp, Bool)]])
-> [Assignment] -> [[(Prp, Bool)]]
forall a b. (a -> b) -> a -> b
$ [Int] -> Bdd -> [Assignment]
allSatsWith ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
props) Bdd
lawbdd
  translate :: [(b, Bool)] -> [b]
translate [(b, Bool)]
l = ((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) -> Bool) -> [(b, Bool)] -> [(b, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (b, Bool) -> Bool
forall a b. (a, b) -> b
snd [(b, Bool)]
l)

instance HasAgents KnowStruct where
  agentsOf :: KnowStruct -> [Agent]
agentsOf (KnS [Prp]
_ Bdd
_ [(Agent, [Prp])]
obs)= ((Agent, [Prp]) -> Agent) -> [(Agent, [Prp])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, [Prp]) -> Agent
forall a b. (a, b) -> a
fst [(Agent, [Prp])]
obs

instance HasVocab KnowStruct where
  vocabOf :: KnowStruct -> [Prp]
vocabOf (KnS [Prp]
props Bdd
_ [(Agent, [Prp])]
_) = [Prp]
props

numberOfStates :: KnowStruct -> Int
numberOfStates :: KnowStruct -> Int
numberOfStates (KnS [Prp]
props Bdd
lawbdd [(Agent, [Prp])]
_) = [Int] -> Bdd -> Int
satCountWith ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
props) Bdd
lawbdd

-- * Semantics

{- $
Semantics on `KnowScene`s are defined inductively as follows.

- \( (\mathcal{F},s)\vDash p\) iff \(s \vDash p\)
- \( (\mathcal{F},s)\vDash \neg \varphi\) iff not \((\mathcal{F},s)\vDash \varphi\)
- \( (\mathcal{F},s)\vDash \varphi \land \psi\) iff \((\mathcal{F},s)\vDash \varphi\) and \((\mathcal{F},s)\vDash \psi\)
- \( (\mathcal{F},s)\vDash { K}_i \varphi\) iff
    for all \(t\) of \(\mathcal{F}\), if \(s\cap O_i=t\cap O_i\), then \((\mathcal{F},t)\vDash \varphi\)
- \((\mathcal{F},s)\vDash {C}_\Delta \varphi\) iff
    for all \(t\) of \(\mathcal{F}\), if \((s,t)\in {\cal E}_\Delta^\ast\), then \(({\cal F},t)\vDash \varphi\)
- \((\mathcal{F},s)\vDash [\psi] \varphi\) iff \((\mathcal{F},s)\vDash \psi\) implies \((\mathcal{F}^\psi, s) \vDash \varphi\)
    where
      \(\| \psi \|_\mathcal{F}\) is given by `bddOf`
      and \[\mathcal{F}^\psi:=(V,\theta \land \| \psi \|_\mathcal{F}, O_1, \dots, O_n)\]
- \((\mathcal{F},s)\vDash [\psi]_\Delta \varphi\) iff
    \((\mathcal{F},s)\vDash \psi\) implies \((\mathcal{F}^\Delta_\psi, s\cup \{ p_\psi \} ) \vDash \varphi\)
    where
      \(p_\psi\) is a new propositional variable,
      \(\| \psi \|_\mathcal{F}\) is a boolean formula given by Definition~\ref{def-boolEquiv}
      and \[\mathcal{F}^\Delta_\psi:= (V\cup \{ p_\psi \},\theta \land (p_\psi \leftrightarrow \| \psi \|_\mathcal{F}), O^\ast_1, \dots, O^\ast_n) \]
      where
        \(O^\ast_i := \left\{ \begin{array}{ll}
          O_i \cup \{ p_\psi \} & \text{if } i \in \Delta \\
          O_i & \text{otherwise}
        \end{array} \right. \)

If we have \(({\cal F},s) \vDash \phi\) for all states \(s\) of \(\cal F\), then we say that \(\phi\) is valid on \(\cal F\) and write \(\cal F \vDash \phi\).
-}

-- | The function `eval` implements the semantics.
-- An important warning: This function is not a symbolic algorithm!
-- It is a direct translation of the Definition above.
-- In particular it calls `statesOf` which means that the set of stats is explicitly generated.
-- The symbolic (and much faster) counterpart of `eval` is `evalViaBdd` below.
eval :: KnowScene -> Form -> Bool
eval :: KnowScene -> Form -> Bool
eval KnowScene
_       Form
Top           = Bool
True
eval KnowScene
_       Form
Bot           = Bool
False
eval (KnowStruct
_,[Prp]
s)   (PrpF Prp
p)      = Prp
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
s
eval (KnowStruct
kns,[Prp]
s) (Neg Form
form)    = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s) Form
form
eval (KnowStruct
kns,[Prp]
s) (Conj [Form]
forms)  = (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s)) [Form]
forms
eval (KnowStruct
kns,[Prp]
s) (Disj [Form]
forms)  = (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s)) [Form]
forms
eval (KnowStruct
kns,[Prp]
s) (Xor  [Form]
forms)  = Int -> Bool
forall a. Integral a => a -> Bool
odd (Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
forall a. a -> a
id ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ (Form -> Bool) -> [Form] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s)) [Form]
forms)
eval KnowScene
scn     (Impl Form
f Form
g)    = Bool -> Bool
not (KnowScene -> Form -> Bool
eval KnowScene
scn Form
f) Bool -> Bool -> Bool
|| KnowScene -> Form -> Bool
eval KnowScene
scn Form
g
eval KnowScene
scn     (Equi Form
f Form
g)    = KnowScene -> Form -> Bool
eval KnowScene
scn Form
f Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== KnowScene -> Form -> Bool
eval KnowScene
scn Form
g
eval KnowScene
scn     (Forall [Prp]
ps Form
f) = KnowScene -> Form -> Bool
eval KnowScene
scn ((Form -> Prp -> Form) -> Form -> [Prp] -> Form
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Form -> Prp -> Form
singleForall Form
f [Prp]
ps) where
  singleForall :: Form -> Prp -> Form
singleForall Form
g Prp
p = [Form] -> Form
Conj [ Prp -> Form -> Form -> Form
SMCDEL.Language.substit Prp
p Form
Top Form
g, Prp -> Form -> Form -> Form
SMCDEL.Language.substit Prp
p Form
Bot Form
g ]
eval KnowScene
scn     (Exists [Prp]
ps Form
f) = KnowScene -> Form -> Bool
eval KnowScene
scn ((Form -> Prp -> Form) -> Form -> [Prp] -> Form
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Form -> Prp -> Form
singleExists Form
f [Prp]
ps) where
  singleExists :: Form -> Prp -> Form
singleExists Form
g Prp
p = [Form] -> Form
Disj [ Prp -> Form -> Form -> Form
SMCDEL.Language.substit Prp
p Form
Top Form
g, Prp -> Form -> Form -> Form
SMCDEL.Language.substit Prp
p Form
Bot Form
g ]
eval (kns :: KnowStruct
kns@(KnS [Prp]
_ Bdd
_ [(Agent, [Prp])]
obs),[Prp]
s) (K Agent
i Form
form) = ([Prp] -> Bool) -> [[Prp]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[Prp]
s' -> KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s') Form
form) [[Prp]]
theres where
  theres :: [[Prp]]
theres = ([Prp] -> Bool) -> [[Prp]] -> [[Prp]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\[Prp]
s' -> [Prp] -> [Prp] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
seteq ([Prp]
s' [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi) ([Prp]
s [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi)) (KnowStruct -> [[Prp]]
statesOf KnowStruct
kns)
  oi :: [Prp]
oi = [(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i
eval (kns :: KnowStruct
kns@(KnS [Prp]
_ Bdd
_ [(Agent, [Prp])]
obs),[Prp]
s) (Kw Agent
i Form
form) = ([Prp] -> Bool) -> [[Prp]] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (\[Prp]
s' -> KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s') Form
form) [[Prp]]
theres where
  theres :: [[Prp]]
theres = ([Prp] -> Bool) -> [[Prp]] -> [[Prp]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\[Prp]
s' -> [Prp] -> [Prp] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
seteq ([Prp]
s' [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi) ([Prp]
s [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi)) (KnowStruct -> [[Prp]]
statesOf KnowStruct
kns)
  oi :: [Prp]
oi = [(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i
eval (KnowStruct
kns,[Prp]
s) (Ck [Agent]
ags Form
form)  = ([Prp] -> Bool) -> [[Prp]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[Prp]
s' -> KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s') Form
form) [[Prp]]
theres where
  theres :: [[Prp]]
theres = [ [Prp]
s' | ([Prp]
s0,[Prp]
s') <- KnowStruct -> [Agent] -> [([Prp], [Prp])]
comknow KnowStruct
kns [Agent]
ags, [Prp]
s0 [Prp] -> [Prp] -> Bool
forall a. Eq a => a -> a -> Bool
== [Prp]
s ]
eval (KnowStruct
kns,[Prp]
s) (Ckw [Agent]
ags Form
form)  = ([Prp] -> Bool) -> [[Prp]] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (\[Prp]
s' -> KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s') Form
form) [[Prp]]
theres where
  theres :: [[Prp]]
theres = [ [Prp]
s' | ([Prp]
s0,[Prp]
s') <- KnowStruct -> [Agent] -> [([Prp], [Prp])]
comknow KnowStruct
kns [Agent]
ags, [Prp]
s0 [Prp] -> [Prp] -> Bool
forall a. Eq a => a -> a -> Bool
== [Prp]
s ]
eval (kns :: KnowStruct
kns@(KnS [Prp]
_ Bdd
_ [(Agent, [Prp])]
obs),[Prp]
s) (Dk [Agent]
ags Form
form) = ([Prp] -> Bool) -> [[Prp]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[Prp]
s' -> KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s') Form
form) [[Prp]]
theres where
  theres :: [[Prp]]
theres = ([Prp] -> Bool) -> [[Prp]] -> [[Prp]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\[Prp]
s' -> [Prp] -> [Prp] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
seteq ([Prp]
s' [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi) ([Prp]
s [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi)) (KnowStruct -> [[Prp]]
statesOf KnowStruct
kns)
  oi :: [Prp]
oi = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [[Prp]] -> [Prp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i | Agent
i <- [Agent]
ags]
eval (kns :: KnowStruct
kns@(KnS [Prp]
_ Bdd
_ [(Agent, [Prp])]
obs),[Prp]
s) (Dkw [Agent]
ags Form
form) = ([Prp] -> Bool) -> [[Prp]] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (\[Prp]
s' -> KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s') Form
form) [[Prp]]
theres where
  theres :: [[Prp]]
theres = ([Prp] -> Bool) -> [[Prp]] -> [[Prp]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\[Prp]
s' -> [Prp] -> [Prp] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
seteq ([Prp]
s' [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi) ([Prp]
s [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi)) (KnowStruct -> [[Prp]]
statesOf KnowStruct
kns)
  oi :: [Prp]
oi = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [[Prp]] -> [Prp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i | Agent
i <- [Agent]
ags]
eval KnowScene
scn (PubAnnounce Form
form1 Form
form2) =
  Bool -> Bool
not (KnowScene -> Form -> Bool
eval KnowScene
scn Form
form1) Bool -> Bool -> Bool
|| KnowScene -> Form -> Bool
eval (KnowScene -> Form -> KnowScene
forall a b. Update a b => a -> b -> a
update KnowScene
scn Form
form1) Form
form2
eval (KnowStruct
kns,[Prp]
s) (PubAnnounceW Form
form1 Form
form2) =
  if KnowScene -> Form -> Bool
eval (KnowStruct
kns, [Prp]
s) Form
form1
    then KnowScene -> Form -> Bool
eval (KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
update KnowStruct
kns Form
form1, [Prp]
s) Form
form2
    else KnowScene -> Form -> Bool
eval (KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
update KnowStruct
kns (Form -> Form
Neg Form
form1), [Prp]
s) Form
form2
eval KnowScene
scn (Announce [Agent]
ags Form
form1 Form
form2) =
  Bool -> Bool
not (KnowScene -> Form -> Bool
eval KnowScene
scn Form
form1) Bool -> Bool -> Bool
|| KnowScene -> Form -> Bool
eval (KnowScene -> [Agent] -> Form -> KnowScene
announceOnScn KnowScene
scn [Agent]
ags Form
form1) Form
form2
eval KnowScene
scn (AnnounceW [Agent]
ags Form
form1 Form
form2) =
  if KnowScene -> Form -> Bool
eval KnowScene
scn Form
form1
    then KnowScene -> Form -> Bool
eval (KnowScene -> [Agent] -> Form -> KnowScene
announceOnScn KnowScene
scn [Agent]
ags Form
form1      ) Form
form2
    else KnowScene -> Form -> Bool
eval (KnowScene -> [Agent] -> Form -> KnowScene
announceOnScn KnowScene
scn [Agent]
ags (Form -> Form
Neg Form
form1)) Form
form2
eval KnowScene
scn (Dia (Dyn Agent
dynLabel Dynamic
d) Form
f) = case Dynamic -> Maybe Event
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
  Just Event
event -> KnowScene -> Form -> Bool
eval KnowScene
scn (Event -> Form
forall a. HasPrecondition a => a -> Form
preOf (Event
event :: Event))
                Bool -> Bool -> Bool
&& KnowScene -> Form -> Bool
eval (KnowScene
scn KnowScene -> Event -> KnowScene
forall a b. Update a b => a -> b -> a
`update` Event
event) Form
f
  Maybe Event
Nothing    -> Agent -> Bool
forall a. HasCallStack => Agent -> a
error (Agent -> Bool) -> Agent -> Bool
forall a b. (a -> b) -> a -> b
$ Agent
"cannot update knowledge structure with '" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
dynLabel Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"':\n  " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Dynamic -> Agent
forall a. Show a => a -> Agent
show Dynamic
d


-- ** Common Knowledge

{- $
To interpret common knowledge we use the following definitions.
Given a /knowledge structure/ \((V,\theta,O_1,\dots,O_n)\) and a set of agents \(\Delta\),
let \(\mathcal{E}_\Delta\) be the relation on states of \(\mathcal{F}\) defined by
  \((s,t) \in {\cal E}_\Delta\) iff
    there exists an \(i\in {\Delta}\) with \(s \cap O_i = t \cap O_i\).
and let \({\cal E}_{\cal V}^\ast\) to denote the transitive closure of \({\cal E}_{\cal V}\).

In our data type for knowledge structures we represent the state law \(\theta\) not as a formula but as a Binary Decision Diagram.
-}

-- | The relation for shared knowledge.
shareknow :: KnowStruct -> [[Prp]] -> [(State,State)]
shareknow :: KnowStruct -> [[Prp]] -> [([Prp], [Prp])]
shareknow KnowStruct
kns [[Prp]]
sets = (([Prp], [Prp]) -> Bool) -> [([Prp], [Prp])] -> [([Prp], [Prp])]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Prp], [Prp]) -> Bool
rel [ ([Prp]
s,[Prp]
t) | [Prp]
s <- KnowStruct -> [[Prp]]
statesOf KnowStruct
kns, [Prp]
t <- KnowStruct -> [[Prp]]
statesOf KnowStruct
kns ] where
  rel :: ([Prp], [Prp]) -> Bool
rel ([Prp]
x,[Prp]
y) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ [Prp] -> [Prp] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
seteq ([Prp]
x [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
set) ([Prp]
y [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
set) | [Prp]
set <- [[Prp]]
sets ]

-- | The relation for common knowledge.
comknow :: KnowStruct -> [Agent] -> [(State,State)]
comknow :: KnowStruct -> [Agent] -> [([Prp], [Prp])]
comknow kns :: KnowStruct
kns@(KnS [Prp]
_ Bdd
_ [(Agent, [Prp])]
obs) [Agent]
ags = [([Prp], [Prp])] -> [([Prp], [Prp])]
forall a. (Ord a, Eq a) => Rel a a -> Rel a a
rtc ([([Prp], [Prp])] -> [([Prp], [Prp])])
-> [([Prp], [Prp])] -> [([Prp], [Prp])]
forall a b. (a -> b) -> a -> b
$ KnowStruct -> [[Prp]] -> [([Prp], [Prp])]
shareknow KnowStruct
kns ((Agent -> [Prp]) -> [Agent] -> [[Prp]]
forall a b. (a -> b) -> [a] -> [b]
map ([(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [Prp])]
obs) [Agent]
ags)

-- ** Announcements

{- $
We also have to define how knowledge structures are changed by public and group announcements.
The following functions correspond to the last two points of the semantics Definition above.
-}

-- TODO remove these, replace with transformers. (at least remove group announcement)

announce :: KnowStruct -> [Agent] -> Form -> KnowStruct
announce :: KnowStruct -> [Agent] -> Form -> KnowStruct
announce kns :: KnowStruct
kns@(KnS [Prp]
props Bdd
lawbdd [(Agent, [Prp])]
obs) [Agent]
ags Form
psi = [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
newprops Bdd
newlawbdd [(Agent, [Prp])]
newobs where
  proppsi :: Prp
proppsi@(P Int
k) = [Prp] -> Prp
freshp [Prp]
props
  newprops :: [Prp]
newprops  = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ Prp
proppsi Prp -> [Prp] -> [Prp]
forall a. a -> [a] -> [a]
: [Prp]
props
  newlawbdd :: Bdd
newlawbdd = Bdd -> Bdd -> Bdd
con Bdd
lawbdd (Bdd -> Bdd -> Bdd
equ (Int -> Bdd
var Int
k) (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
psi))
  newobs :: [(Agent, [Prp])]
newobs    = [(Agent
i, [(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp
proppsi | 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]) | Agent
i <- ((Agent, [Prp]) -> Agent) -> [(Agent, [Prp])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, [Prp]) -> Agent
forall a b. (a, b) -> a
fst [(Agent, [Prp])]
obs]

announceOnScn :: KnowScene -> [Agent] -> Form -> KnowScene
announceOnScn :: KnowScene -> [Agent] -> Form -> KnowScene
announceOnScn (kns :: KnowStruct
kns@(KnS [Prp]
props Bdd
_ [(Agent, [Prp])]
_),[Prp]
s) [Agent]
ags Form
psi
  | KnowScene -> Form -> Bool
eval (KnowStruct
kns,[Prp]
s) Form
psi = (KnowStruct -> [Agent] -> Form -> KnowStruct
announce KnowStruct
kns [Agent]
ags Form
psi, [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp] -> Prp
freshp [Prp]
props Prp -> [Prp] -> [Prp]
forall a. a -> [a] -> [a]
: [Prp]
s)
  | Bool
otherwise        = Agent -> KnowScene
forall a. HasCallStack => Agent -> a
error Agent
"Liar!"


-- * Symbolic Evaluation

bddOf :: KnowStruct -> Form -> Bdd
bddOf :: KnowStruct -> Form -> Bdd
bddOf KnowStruct
_   Form
Top           = Bdd
top
bddOf KnowStruct
_   Form
Bot           = Bdd
bot
bddOf KnowStruct
_   (PrpF (P Int
n))  = Int -> Bdd
var Int
n
bddOf KnowStruct
kns (Neg Form
form)    = Bdd -> Bdd
neg (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
form
bddOf KnowStruct
kns (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 (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns) [Form]
forms
bddOf KnowStruct
kns (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 (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns) [Form]
forms
bddOf KnowStruct
kns (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 (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns) [Form]
forms
bddOf KnowStruct
kns (Impl Form
f Form
g)    = Bdd -> Bdd -> Bdd
imp (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f) (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
g)
bddOf KnowStruct
kns (Equi Form
f Form
g)    = Bdd -> Bdd -> Bdd
equ (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f) (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
g)
bddOf KnowStruct
kns (Forall [Prp]
ps Form
f) = [Int] -> Bdd -> Bdd
forallSet ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
ps) (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f)
bddOf KnowStruct
kns (Exists [Prp]
ps Form
f) = [Int] -> Bdd -> Bdd
existsSet ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
ps) (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f)
bddOf kns :: KnowStruct
kns@(KnS [Prp]
allprops Bdd
lawbdd [(Agent, [Prp])]
obs) (K Agent
i Form
form) =
  [Int] -> Bdd -> Bdd
forallSet [Int]
otherps (Bdd -> Bdd -> Bdd
imp Bdd
lawbdd (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
form)) where
    otherps :: [Int]
otherps = (Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(P Int
n) -> Int
n) ([Prp] -> [Int]) -> [Prp] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Prp]
allprops [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i
bddOf kns :: KnowStruct
kns@(KnS [Prp]
allprops Bdd
lawbdd [(Agent, [Prp])]
obs) (Kw Agent
i Form
form) =
  [Bdd] -> Bdd
disSet [ [Int] -> Bdd -> Bdd
forallSet [Int]
otherps (Bdd -> Bdd -> Bdd
imp Bdd
lawbdd (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f)) | Form
f <- [Form
form, Form -> Form
Neg Form
form] ] where
    otherps :: [Int]
otherps = (Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(P Int
n) -> Int
n) ([Prp] -> [Int]) -> [Prp] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Prp]
allprops [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i
bddOf kns :: KnowStruct
kns@(KnS [Prp]
allprops Bdd
lawbdd [(Agent, [Prp])]
obs) (Ck [Agent]
ags Form
form) = (Bdd -> Bdd) -> Bdd
gfp Bdd -> Bdd
lambda where
  lambda :: Bdd -> Bdd
lambda Bdd
z = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> [Bdd] -> Bdd
forall a b. (a -> b) -> a -> b
$ KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
form Bdd -> [Bdd] -> [Bdd]
forall a. a -> [a] -> [a]
: [ [Int] -> Bdd -> Bdd
forallSet (Agent -> [Int]
otherps Agent
i) (Bdd -> Bdd -> Bdd
imp Bdd
lawbdd Bdd
z) | Agent
i <- [Agent]
ags ]
  otherps :: Agent -> [Int]
otherps Agent
i = (Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(P Int
n) -> Int
n) ([Prp] -> [Int]) -> [Prp] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Prp]
allprops [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i
bddOf KnowStruct
kns (Ckw [Agent]
ags Form
form) = Bdd -> Bdd -> Bdd
dis (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns ([Agent] -> Form -> Form
Ck [Agent]
ags Form
form)) (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns ([Agent] -> Form -> Form
Ck [Agent]
ags (Form -> Form
Neg Form
form)))
bddOf kns :: KnowStruct
kns@(KnS [Prp]
allprops Bdd
lawbdd [(Agent, [Prp])]
obs) (Dk [Agent]
ags Form
form) =
  [Int] -> Bdd -> Bdd
forallSet [Int]
otherps (Bdd -> Bdd -> Bdd
imp Bdd
lawbdd (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
form)) where
    otherps :: [Int]
otherps = (Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(P Int
n) -> Int
n) ([Prp] -> [Int]) -> [Prp] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Prp]
allprops [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
uoi
    uoi :: [Prp]
uoi = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([[Prp]] -> [Prp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i | Agent
i <- [Agent]
ags])
bddOf kns :: KnowStruct
kns@(KnS [Prp]
allprops Bdd
lawbdd [(Agent, [Prp])]
obs) (Dkw [Agent]
ags Form
form) =
  [Bdd] -> Bdd
disSet [ [Int] -> Bdd -> Bdd
forallSet [Int]
otherps (Bdd -> Bdd -> Bdd
imp Bdd
lawbdd (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f)) | Form
f <- [Form
form, Form -> Form
Neg Form
form] ] where
    otherps :: [Int]
otherps = (Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(P Int
n) -> Int
n) ([Prp] -> [Int]) -> [Prp] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Prp]
allprops [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
uoi
    uoi :: [Prp]
uoi = [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub ([[Prp]] -> [Prp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i | Agent
i <- [Agent]
ags])
bddOf kns :: KnowStruct
kns@(KnS [Prp]
props Bdd
_ [(Agent, [Prp])]
_) (Announce [Agent]
ags Form
form1 Form
form2) =
  Bdd -> Bdd -> Bdd
imp (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
form1) (Bdd -> (Int, Bool) -> Bdd
restrict Bdd
bdd2 (Int
k,Bool
True)) where
    bdd2 :: Bdd
bdd2  = KnowStruct -> Form -> Bdd
bddOf (KnowStruct -> [Agent] -> Form -> KnowStruct
announce KnowStruct
kns [Agent]
ags Form
form1) Form
form2
    (P Int
k) = [Prp] -> Prp
freshp [Prp]
props
bddOf kns :: KnowStruct
kns@(KnS [Prp]
props Bdd
_ [(Agent, [Prp])]
_) (AnnounceW [Agent]
ags Form
form1 Form
form2) =
  Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
form1) Bdd
bdd2a Bdd
bdd2b where
    bdd2a :: Bdd
bdd2a = Bdd -> (Int, Bool) -> Bdd
restrict (KnowStruct -> Form -> Bdd
bddOf (KnowStruct -> [Agent] -> Form -> KnowStruct
announce KnowStruct
kns [Agent]
ags Form
form1) Form
form2) (Int
k,Bool
True)
    bdd2b :: Bdd
bdd2b = Bdd -> (Int, Bool) -> Bdd
restrict (KnowStruct -> Form -> Bdd
bddOf (KnowStruct -> [Agent] -> Form -> KnowStruct
announce KnowStruct
kns [Agent]
ags Form
form1) Form
form2) (Int
k,Bool
False)
    (P Int
k) = [Prp] -> Prp
freshp [Prp]
props
bddOf KnowStruct
kns (PubAnnounce Form
form1 Form
form2) =
  Bdd -> Bdd -> Bdd
imp (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
form1) (KnowStruct -> Form -> Bdd
bddOf (KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
update KnowStruct
kns Form
form1) Form
form2)
bddOf KnowStruct
kns (PubAnnounceW Form
form1 Form
form2) =
  Bdd -> Bdd -> Bdd -> Bdd
ifthenelse (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
form1) Bdd
newform2a Bdd
newform2b where
    newform2a :: Bdd
newform2a = KnowStruct -> Form -> Bdd
bddOf (KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
update KnowStruct
kns Form
form1) Form
form2
    newform2b :: Bdd
newform2b = KnowStruct -> Form -> Bdd
bddOf (KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
update KnowStruct
kns (Form -> Form
Neg Form
form1)) Form
form2

bddOf KnowStruct
kns (Dia (Dyn Agent
dynLabel Dynamic
d) Form
f) =
    Bdd -> Bdd -> Bdd
con (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns 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, [(Prp, Bdd)]
changeLaw [(Prp, Bdd)] -> Prp -> Bdd
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Prp
p)       -- 2. Replace changeProps V_ with postcons
                   | p :: Prp
p@(P Int
k) <- [Prp]
changeProps]  --    (no "relabelWith copyrel", undone in 4)
    (Bdd -> Bdd) -> (Form -> Bdd) -> Form -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KnowStruct -> Form -> Bdd
bddOf (KnowStruct
kns KnowStruct -> KnowTransformer -> KnowStruct
forall a b. Update a b => a -> b -> a
`update` KnowTransformer
trf)                -- 1. boolean equivalent wrt new struct
    (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Form
f
  where
    changeProps :: [Prp]
changeProps = ((Prp, Bdd) -> Prp) -> [(Prp, Bdd)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bdd) -> Prp
forall a b. (a, b) -> a
fst [(Prp, Bdd)]
changeLaw
    copychangeProps :: [Prp]
copychangeProps = [([Prp] -> Prp
freshp ([Prp] -> Prp) -> [Prp] -> Prp
forall a b. (a -> b) -> a -> b
$ KnowStruct -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KnowStruct
kns [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
addProps)..]
    copyrelInverse :: [(Prp, Prp)]
copyrelInverse  = [Prp] -> [Prp] -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Prp]
copychangeProps [Prp]
changeProps
    (trf :: KnowTransformer
trf@(KnTrf [Prp]
addProps Form
addLaw [(Prp, Bdd)]
changeLaw [(Agent, [Prp])]
_), [(Prp, Prp)]
shiftrel) = KnowStruct -> KnowTransformer -> (KnowTransformer, [(Prp, Prp)])
shiftPrepare KnowStruct
kns KnowTransformer
trfUnshifted
    (Form
preCon,KnowTransformer
trfUnshifted,Bdd -> Bdd
simulateActualEvents) =
      case Dynamic -> Maybe Event
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
        -- 3. For a single event, simulate actual event x outof V+
        Just ((KnowTransformer
t,[Prp]
x) :: Event) -> ( Event -> Form
forall a. HasPrecondition a => a -> Form
preOf (KnowTransformer
t,[Prp]
x), KnowTransformer
t, (Bdd -> Assignment -> Bdd
`restrictSet` Assignment
actualAss) )
          where actualAss :: Assignment
actualAss = [(Int
newK, Int -> Prp
P Int
k Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
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 ((KnowTransformer
t,Bdd
xsBdd) :: MultipointedEvent) ->
              ( MultipointedEvent -> Form
forall a. HasPrecondition a => a -> Form
preOf (KnowTransformer
t,Bdd
xsBdd), KnowTransformer
t
              , [Int] -> Bdd -> Bdd
existsSet ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
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 (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
addLaw)           -- ... and a precondition.
              ) where actualsBdd :: Bdd
actualsBdd = [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftrel Bdd
xsBdd
          Maybe MultipointedEvent
Nothing -> Agent -> (Form, KnowTransformer, Bdd -> Bdd)
forall a. HasCallStack => Agent -> a
error (Agent -> (Form, KnowTransformer, Bdd -> Bdd))
-> Agent -> (Form, KnowTransformer, Bdd -> Bdd)
forall a b. (a -> b) -> a -> b
$ Agent
"cannot update knowledge structure with '" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
dynLabel Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"':\n " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Dynamic -> Agent
forall a. Show a => a -> Agent
show Dynamic
d

evalViaBdd :: KnowScene -> Form -> Bool
evalViaBdd :: KnowScene -> Form -> Bool
evalViaBdd (KnowStruct
kns,[Prp]
s) Form
f = Bdd -> (Int -> Bool) -> Bool
evaluateFun (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f) (\Int
n -> Int -> Prp
P Int
n Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
s)

instance Semantics KnowStruct where
  isTrue :: KnowStruct -> Form -> Bool
isTrue = KnowStruct -> Form -> Bool
validViaBdd

instance Semantics KnowScene where
  isTrue :: KnowScene -> Form -> Bool
isTrue = KnowScene -> Form -> Bool
evalViaBdd

instance Semantics MultipointedKnowScene where
  isTrue :: MultipointedKnowScene -> Form -> Bool
isTrue (kns :: KnowStruct
kns@(KnS [Prp]
_ Bdd
lawBdd [(Agent, [Prp])]
_),Bdd
statesBdd) Form
f =
    let a :: Bdd
a = Bdd
lawBdd Bdd -> Bdd -> Bdd
`imp` (Bdd
statesBdd Bdd -> Bdd -> Bdd
`imp` KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f)
     in Bdd
a Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
top

instance Update KnowStruct Form where
  checks :: [KnowStruct -> Form -> Bool]
checks = [ ] -- unpointed structures can be updated with anything
  unsafeUpdate :: KnowStruct -> Form -> KnowStruct
unsafeUpdate kns :: KnowStruct
kns@(KnS [Prp]
props Bdd
lawbdd [(Agent, [Prp])]
obs) Form
psi =
    [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
props (Bdd
lawbdd Bdd -> Bdd -> Bdd
`con` KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
psi) [(Agent, [Prp])]
obs

instance Update KnowScene Form where
  unsafeUpdate :: KnowScene -> Form -> KnowScene
unsafeUpdate (KnowStruct
kns,[Prp]
s) Form
psi = (KnowStruct -> Form -> KnowStruct
forall a b. Update a b => a -> b -> a
unsafeUpdate KnowStruct
kns Form
psi,[Prp]
s)

validViaBdd :: KnowStruct -> Form -> Bool
validViaBdd :: KnowStruct -> Form -> Bool
validViaBdd kns :: KnowStruct
kns@(KnS [Prp]
_ Bdd
lawbdd [(Agent, [Prp])]
_) Form
f = Bdd
top Bdd -> Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== Bdd
lawbdd Bdd -> Bdd -> Bdd
`imp` KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f

whereViaBdd :: KnowStruct -> Form -> [State]
whereViaBdd :: KnowStruct -> Form -> [[Prp]]
whereViaBdd kns :: KnowStruct
kns@(KnS [Prp]
props Bdd
lawbdd [(Agent, [Prp])]
_) Form
f =
 (Assignment -> [Prp]) -> [Assignment] -> [[Prp]]
forall a b. (a -> b) -> [a] -> [b]
map ([Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> (Assignment -> [Prp]) -> Assignment -> [Prp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Bool) -> Prp) -> Assignment -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Prp
forall a. Enum a => Int -> a
toEnum (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) (Assignment -> [Prp])
-> (Assignment -> Assignment) -> Assignment -> [Prp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Bool) -> Bool) -> Assignment -> Assignment
forall a. (a -> Bool) -> [a] -> [a]
filter (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd) ([Assignment] -> [[Prp]]) -> [Assignment] -> [[Prp]]
forall a b. (a -> b) -> a -> b
$
   [Int] -> Bdd -> [Assignment]
allSatsWith ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
props) (Bdd -> [Assignment]) -> Bdd -> [Assignment]
forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd -> Bdd
con Bdd
lawbdd (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f)

-- * Minimization and Optimization

-- | Knowledge structures can contain unnecessary vocabulary, i.e. atomic propositions that are determined by the state law and not used as observational propositions.

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

nonobsVocabOf  :: KnowStruct -> [Prp]
nonobsVocabOf :: KnowStruct -> [Prp]
nonobsVocabOf (KnS [Prp]
vocab Bdd
_ [(Agent, [Prp])]
obs) = (Prp -> Bool) -> [Prp] -> [Prp]
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp -> [Prp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((Agent, [Prp]) -> [Prp]) -> [(Agent, [Prp])] -> [Prp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Agent, [Prp]) -> [Prp]
forall a b. (a, b) -> b
snd [(Agent, [Prp])]
obs) [Prp]
vocab

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

replaceWithIn :: (Prp,Prp) -> KnowStruct -> KnowStruct
replaceWithIn :: (Prp, Prp) -> KnowStruct -> KnowStruct
replaceWithIn (Prp
p,Prp
q) (KnS [Prp]
oldProps Bdd
oldLaw [(Agent, [Prp])]
oldObs) =
  [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS
    (Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete Prp
p [Prp]
oldProps)
    (Int -> Bdd -> Bdd -> Bdd
Data.HasCacBDD.substit (Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
p) (Int -> Bdd
var (Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
q)) Bdd
oldLaw)
    [(Agent
i, if Prp
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
os then [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp] -> [Prp]
forall a. Eq a => [a] -> [a]
nub (Prp
q Prp -> [Prp] -> [Prp]
forall a. a -> [a] -> [a]
: Prp -> [Prp] -> [Prp]
forall a. Eq a => a -> [a] -> [a]
delete Prp
p [Prp]
os) else [Prp]
os) | (Agent
i,[Prp]
os) <- [(Agent, [Prp])]
oldObs]

replaceEquivExtra :: [Prp] -> KnowStruct -> (KnowStruct,[(Prp,Prp)])
replaceEquivExtra :: [Prp] -> KnowStruct -> (KnowStruct, [(Prp, Prp)])
replaceEquivExtra [Prp]
mainVocab KnowStruct
startKns = ((KnowStruct, [(Prp, Prp)]) -> (KnowStruct, [(Prp, Prp)]))
-> (KnowStruct, [(Prp, Prp)]) -> (KnowStruct, [(Prp, Prp)])
forall a. Eq a => (a -> a) -> a -> a
lfp (KnowStruct, [(Prp, Prp)]) -> (KnowStruct, [(Prp, Prp)])
step (KnowStruct
startKns,[]) where
  step :: (KnowStruct, [(Prp, Prp)]) -> (KnowStruct, [(Prp, Prp)])
step (KnowStruct
kns,[(Prp, Prp)]
replRel) = case [Prp] -> KnowStruct -> [(Prp, Prp)]
equivExtraVocabOf [Prp]
mainVocab KnowStruct
kns of
               []        -> (KnowStruct
kns,[(Prp, Prp)]
replRel)
               ((Prp
p,Prp
q):[(Prp, Prp)]
_) -> ((Prp, Prp) -> KnowStruct -> KnowStruct
replaceWithIn (Prp
p,Prp
q) KnowStruct
kns, (Prp
p,Prp
q)(Prp, Prp) -> [(Prp, Prp)] -> [(Prp, Prp)]
forall a. a -> [a] -> [a]
:[(Prp, Prp)]
replRel)

-- | Remove determined and unused atomic propositions from a structure to make the state law smaller.
withoutProps :: [Prp] -> KnowStruct -> KnowStruct
withoutProps :: [Prp] -> KnowStruct -> KnowStruct
withoutProps [Prp]
propsToDel (KnS [Prp]
oldProps Bdd
oldLawBdd [(Agent, [Prp])]
oldObs) =
  [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS
    ([Prp]
oldProps [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
propsToDel)
    ([Int] -> Bdd -> Bdd
existsSet ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
propsToDel) Bdd
oldLawBdd)
    [(Agent
i,[Prp]
os [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
propsToDel) | (Agent
i,[Prp]
os) <- [(Agent, [Prp])]
oldObs]

instance Optimizable KnowStruct where
  optimize :: [Prp] -> KnowStruct -> KnowStruct
optimize [Prp]
myVocab KnowStruct
oldKns = KnowStruct
newKns where
    intermediateKns :: KnowStruct
intermediateKns = [Prp] -> KnowStruct -> KnowStruct
withoutProps (KnowStruct -> [Prp]
determinedVocabOf KnowStruct
oldKns [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
myVocab) KnowStruct
oldKns
    newKns :: KnowStruct
newKns = (KnowStruct, [(Prp, Prp)]) -> KnowStruct
forall a b. (a, b) -> a
fst ((KnowStruct, [(Prp, Prp)]) -> KnowStruct)
-> (KnowStruct, [(Prp, Prp)]) -> KnowStruct
forall a b. (a -> b) -> a -> b
$ [Prp] -> KnowStruct -> (KnowStruct, [(Prp, Prp)])
replaceEquivExtra [Prp]
myVocab KnowStruct
intermediateKns

instance Optimizable KnowScene where
  optimize :: [Prp] -> KnowScene -> KnowScene
optimize [Prp]
myVocab (KnowStruct
oldKns,[Prp]
oldState) = (KnowStruct
newKns,[Prp]
newState) where
    intermediateKns :: KnowStruct
intermediateKns = [Prp] -> KnowStruct -> KnowStruct
withoutProps (KnowStruct -> [Prp]
determinedVocabOf KnowStruct
oldKns [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
myVocab) KnowStruct
oldKns
    removedProps :: [Prp]
removedProps = KnowStruct -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KnowStruct
oldKns [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ KnowStruct -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KnowStruct
intermediateKns
    intermediateState :: [Prp]
intermediateState = [Prp]
oldState [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
removedProps
    (KnowStruct
newKns,[(Prp, Prp)]
replRel) = [Prp] -> KnowStruct -> (KnowStruct, [(Prp, Prp)])
replaceEquivExtra [Prp]
myVocab KnowStruct
intermediateKns
    newState :: [Prp]
newState = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ ([Prp]
intermediateState [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ ((Prp, Prp) -> Prp) -> [(Prp, Prp)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Prp) -> Prp
forall a b. (a, b) -> a
fst [(Prp, Prp)]
replRel) [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [ Prp
q | (Prp
p,Prp
q) <- [(Prp, Prp)]
replRel, Prp
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
intermediateState ]

instance Optimizable MultipointedKnowScene where
  optimize :: [Prp] -> MultipointedKnowScene -> MultipointedKnowScene
optimize [Prp]
myVocab (KnowStruct
oldKns,Bdd
oldStatesBdd) = (KnowStruct
newKns,Bdd
newStatesBdd) where
    intermediateKns :: KnowStruct
intermediateKns = [Prp] -> KnowStruct -> KnowStruct
withoutProps (KnowStruct -> [Prp]
determinedVocabOf KnowStruct
oldKns [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
myVocab) KnowStruct
oldKns
    removedProps :: [Prp]
removedProps = KnowStruct -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KnowStruct
oldKns [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ KnowStruct -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KnowStruct
intermediateKns
    intermediateStatesBdd :: Bdd
intermediateStatesBdd = [Int] -> Bdd -> Bdd
existsSet ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum [Prp]
removedProps) Bdd
oldStatesBdd
    (KnowStruct
newKns,[(Prp, Prp)]
replRel) = [Prp] -> KnowStruct -> (KnowStruct, [(Prp, Prp)])
replaceEquivExtra [Prp]
myVocab KnowStruct
intermediateKns
    newStatesBdd :: Bdd
newStatesBdd = ((Int, Bdd) -> Bdd -> Bdd) -> Bdd -> [(Int, Bdd)] -> Bdd
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Int -> Bdd -> Bdd -> Bdd) -> (Int, Bdd) -> Bdd -> Bdd
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Bdd -> Bdd -> Bdd
Data.HasCacBDD.substit) Bdd
intermediateStatesBdd [ (Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
p, Int -> Bdd
var (Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
q)) | (Prp
p,Prp
q) <-[(Prp, Prp)]
replRel ]

generatedSubstructure :: MultipointedKnowScene -> MultipointedKnowScene
generatedSubstructure :: MultipointedKnowScene -> MultipointedKnowScene
generatedSubstructure kns :: MultipointedKnowScene
kns@(KnS [Prp]
props Bdd
oldLaw [(Agent, [Prp])]
obs, Bdd
curBdd) = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
props Bdd
newLaw [(Agent, [Prp])]
obs, Bdd
curBdd) where
  extend :: Bdd -> Bdd
extend Bdd
this = [Bdd] -> Bdd
disSet (Bdd
this Bdd -> [Bdd] -> [Bdd]
forall a. a -> [a] -> [a]
: [ [Int] -> Bdd -> Bdd
existsSet ((Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum ([Prp] -> [Int]) -> [Prp] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Prp]
props [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i) Bdd
this | Agent
i <- MultipointedKnowScene -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf MultipointedKnowScene
kns ])
  reachable :: Bdd
reachable = (Bdd -> Bdd) -> Bdd -> Bdd
forall a. Eq a => (a -> a) -> a -> a
lfp Bdd -> Bdd
extend Bdd
curBdd
  newLaw :: Bdd
newLaw = Bdd
oldLaw Bdd -> Bdd -> Bdd
`con` Bdd
reachable

-- * Symbolic Bisimulations f
--
-- | See Section 2.11 from https://malv.in/phdthesis for details.

-- | To distinguish explicit and symbolic bisimulations in the implementation we call symbolic bisimulations /propulations/.
type Propulation = Tagged Quadrupel Bdd

($$) :: Monad m => ([a] -> b) -> [m a] -> m b
$$ :: forall (m :: * -> *) a b. Monad m => ([a] -> b) -> [m a] -> m b
($$) [a] -> b
f [m a]
xs = [a] -> b
f ([a] -> b) -> m [a] -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [m a] -> m [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [m a]
xs

checkPropu :: Propulation -> KnowStruct -> KnowStruct -> [Prp] -> Bool
checkPropu :: Tagged Quadrupel Bdd -> KnowStruct -> KnowStruct -> [Prp] -> Bool
checkPropu Tagged Quadrupel Bdd
propu kns1 :: KnowStruct
kns1@(KnS [Prp]
_ Bdd
law1 [(Agent, [Prp])]
obs1) kns2 :: KnowStruct
kns2@(KnS [Prp]
_ Bdd
law2 [(Agent, [Prp])]
obs2) [Prp]
voc =
  Bdd -> Tagged Quadrupel Bdd
forall a. a -> Tagged Quadrupel a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bdd
top Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd -> Bool
forall a. Eq a => a -> a -> Bool
== (Bdd -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged Quadrupel Bdd
lhs Tagged Quadrupel (Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd
forall a b.
Tagged Quadrupel (a -> b)
-> Tagged Quadrupel a -> Tagged Quadrupel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tagged Quadrupel Bdd
rhs) where
    lhs :: Tagged Quadrupel Bdd
lhs = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> [Tagged Quadrupel Bdd] -> Tagged Quadrupel Bdd
forall (m :: * -> *) a b. Monad m => ([a] -> b) -> [m a] -> m b
$$ [Bdd -> Tagged Quadrupel Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
mv Bdd
law1, Bdd -> Tagged Quadrupel Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
cp Bdd
law2, Tagged Quadrupel Bdd
propu]
    rhs :: Tagged Quadrupel Bdd
rhs = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> [Tagged Quadrupel Bdd] -> Tagged Quadrupel Bdd
forall (m :: * -> *) a b. Monad m => ([a] -> b) -> [m a] -> m b
$$ [Tagged Quadrupel Bdd
propAgree, Tagged Quadrupel Bdd
forth, Tagged Quadrupel Bdd
back]
    propAgree :: Tagged Quadrupel Bdd
propAgree = [Prp] -> Tagged Quadrupel Bdd
forall a. TagForBDDs a => [Prp] -> Tagged a Bdd
allsamebdd [Prp]
voc
    forth :: Tagged Quadrupel Bdd
forth = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> [Tagged Quadrupel Bdd] -> Tagged Quadrupel Bdd
forall (m :: * -> *) a b. Monad m => ([a] -> b) -> [m a] -> m b
$$ [ [Int] -> Bdd -> Bdd
forallSet (Agent -> [(Agent, [Prp])] -> [Int]
forall {a}. (Show a, Eq a) => a -> Rel a [Prp] -> [Int]
nonObs Agent
i [(Agent, [Prp])]
obs1) (Bdd -> Bdd) -> Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                          (Bdd -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> Tagged Quadrupel Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
mv Bdd
law1 Tagged Quadrupel (Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd
forall a b.
Tagged Quadrupel (a -> b)
-> Tagged Quadrupel a -> Tagged Quadrupel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Int] -> Bdd -> Bdd
existsSet (Agent -> [(Agent, [Prp])] -> [Int]
forall {a}. (Show a, Eq a) => a -> Rel a [Prp] -> [Int]
nonObs Agent
i [(Agent, [Prp])]
obs2) (Bdd -> Bdd) -> Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> Tagged Quadrupel Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
cp Bdd
law2 Tagged Quadrupel (Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd
forall a b.
Tagged Quadrupel (a -> b)
-> Tagged Quadrupel a -> Tagged Quadrupel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tagged Quadrupel Bdd
propu)))
                      | Agent
i <- KnowStruct -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KnowStruct
kns1 ]
    back :: Tagged Quadrupel Bdd
back  = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> [Tagged Quadrupel Bdd] -> Tagged Quadrupel Bdd
forall (m :: * -> *) a b. Monad m => ([a] -> b) -> [m a] -> m b
$$ [ [Int] -> Bdd -> Bdd
forallSet (Agent -> [(Agent, [Prp])] -> [Int]
forall {a}. (Show a, Eq a) => a -> Rel a [Prp] -> [Int]
nonObs Agent
i [(Agent, [Prp])]
obs1) (Bdd -> Bdd) -> Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                          (Bdd -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> Tagged Quadrupel Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
mv Bdd
law2 Tagged Quadrupel (Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd
forall a b.
Tagged Quadrupel (a -> b)
-> Tagged Quadrupel a -> Tagged Quadrupel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Int] -> Bdd -> Bdd
existsSet (Agent -> [(Agent, [Prp])] -> [Int]
forall {a}. (Show a, Eq a) => a -> Rel a [Prp] -> [Int]
nonObs Agent
i [(Agent, [Prp])]
obs1) (Bdd -> Bdd) -> Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> Tagged Quadrupel Bdd
forall a. TagForBDDs a => Bdd -> Tagged a Bdd
cp Bdd
law1 Tagged Quadrupel (Bdd -> Bdd)
-> Tagged Quadrupel Bdd -> Tagged Quadrupel Bdd
forall a b.
Tagged Quadrupel (a -> b)
-> Tagged Quadrupel a -> Tagged Quadrupel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tagged Quadrupel Bdd
propu)))
                      | Agent
i <- KnowStruct -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KnowStruct
kns2 ]
    nonObs :: a -> Rel a [Prp] -> [Int]
nonObs a
i Rel a [Prp]
obs = (Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(P Int
n) -> Int
n) ([Prp] -> [Int]) -> [Prp] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Prp]
voc [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ Rel a [Prp]
obs Rel a [Prp] -> a -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! a
i

-- * Knowledge Transformers

data KnowTransformer = KnTrf
  [Prp]            -- addProps
  Form             -- addLaw
  [(Prp,Bdd)]      -- changeLaw
  [(Agent,[Prp])]  -- addObs
  deriving (KnowTransformer -> KnowTransformer -> Bool
(KnowTransformer -> KnowTransformer -> Bool)
-> (KnowTransformer -> KnowTransformer -> Bool)
-> Eq KnowTransformer
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: KnowTransformer -> KnowTransformer -> Bool
== :: KnowTransformer -> KnowTransformer -> Bool
$c/= :: KnowTransformer -> KnowTransformer -> Bool
/= :: KnowTransformer -> KnowTransformer -> Bool
Eq,Int -> KnowTransformer -> ShowS
[KnowTransformer] -> ShowS
KnowTransformer -> Agent
(Int -> KnowTransformer -> ShowS)
-> (KnowTransformer -> Agent)
-> ([KnowTransformer] -> ShowS)
-> Show KnowTransformer
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> KnowTransformer -> ShowS
showsPrec :: Int -> KnowTransformer -> ShowS
$cshow :: KnowTransformer -> Agent
show :: KnowTransformer -> Agent
$cshowList :: [KnowTransformer] -> ShowS
showList :: [KnowTransformer] -> ShowS
Show)

noChange :: ([Prp] -> Form -> [(Prp,Bdd)] -> [(Agent,[Prp])] -> KnowTransformer)
          -> [Prp] -> Form                -> [(Agent,[Prp])] -> KnowTransformer
noChange :: ([Prp]
 -> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer)
-> [Prp] -> Form -> [(Agent, [Prp])] -> KnowTransformer
noChange [Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer
kntrf [Prp]
addprops Form
addlaw = [Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer
kntrf [Prp]
addprops Form
addlaw []

instance HasAgents KnowTransformer where
  agentsOf :: KnowTransformer -> [Agent]
agentsOf (KnTrf [Prp]
_ Form
_ [(Prp, Bdd)]
_ [(Agent, [Prp])]
obdds) = ((Agent, [Prp]) -> Agent) -> [(Agent, [Prp])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, [Prp]) -> Agent
forall a b. (a, b) -> a
fst [(Agent, [Prp])]
obdds

instance HasPrecondition KnowTransformer where
  preOf :: KnowTransformer -> Form
preOf KnowTransformer
_ = Form
Top

instance Pointed KnowTransformer State
type Event = (KnowTransformer,State)

instance HasPrecondition Event where
  preOf :: Event -> Form
preOf (KnTrf [Prp]
addprops Form
addlaw [(Prp, Bdd)]
_ [(Agent, [Prp])]
_, [Prp]
x) = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Prp] -> [Prp] -> Form -> Form
substitOutOf [Prp]
x [Prp]
addprops Form
addlaw

instance Pointed KnowTransformer Bdd
type MultipointedEvent = (KnowTransformer,Bdd)

instance HasPrecondition MultipointedEvent where
  preOf :: MultipointedEvent -> Form
preOf (KnTrf [Prp]
addprops Form
addlaw [(Prp, Bdd)]
_ [(Agent, [Prp])]
_, Bdd
xsBdd) =
    Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Prp] -> Form -> Form
Exists [Prp]
addprops ([Form] -> Form
Conj [ Bdd -> Form
formOf Bdd
xsBdd, Form
addlaw ])

-- | A public announcement, the easiest example of a knowledge transformer.
publicAnnounce :: [Agent] -> Form -> Event
publicAnnounce :: [Agent] -> Form -> Event
publicAnnounce [Agent]
agents Form
f = (([Prp]
 -> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer)
-> [Prp] -> Form -> [(Agent, [Prp])] -> KnowTransformer
noChange [Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer
KnTrf [] Form
f [(Agent, [Prp])]
forall {a}. [(Agent, [a])]
myobs, []) where
  myobs :: [(Agent, [a])]
myobs = [ (Agent
i,[]) | Agent
i <- [Agent]
agents ]

-- | shift addprops to ensure that props and newprops are disjoint:
shiftPrepare :: KnowStruct -> KnowTransformer -> (KnowTransformer, [(Prp,Prp)])
shiftPrepare :: KnowStruct -> KnowTransformer -> (KnowTransformer, [(Prp, Prp)])
shiftPrepare (KnS [Prp]
props Bdd
_ [(Agent, [Prp])]
_) (KnTrf [Prp]
addprops Form
addlaw [(Prp, Bdd)]
changelaw [(Agent, [Prp])]
eventObs) =
  ([Prp]
-> Form -> [(Prp, Bdd)] -> [(Agent, [Prp])] -> KnowTransformer
KnTrf [Prp]
shiftaddprops Form
addlawShifted [(Prp, Bdd)]
changelawShifted [(Agent, [Prp])]
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
$ [Prp] -> [Prp] -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Prp]
addprops [([Prp] -> Prp
freshp [Prp]
props)..]
    shiftaddprops :: [Prp]
shiftaddprops = ((Prp, Prp) -> Prp) -> [(Prp, Prp)] -> [Prp]
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 :: [(Prp, Bdd)]
changelawShifted = ((Prp, Bdd) -> (Prp, Bdd)) -> [(Prp, Bdd)] -> [(Prp, Bdd)]
forall a b. (a -> b) -> [a] -> [b]
map ((Bdd -> Bdd) -> (Prp, Bdd) -> (Prp, Bdd)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ([(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftrel)) [(Prp, Bdd)]
changelaw
    eventObsShifted :: [(Agent, [Prp])]
eventObsShifted  = ((Agent, [Prp]) -> (Agent, [Prp]))
-> [(Agent, [Prp])] -> [(Agent, [Prp])]
forall a b. (a -> b) -> [a] -> [b]
map (([Prp] -> [Prp]) -> (Agent, [Prp]) -> (Agent, [Prp])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((Prp -> Prp) -> [Prp] -> [Prp]
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))) [(Agent, [Prp])]
eventObs

instance Update KnowScene Event where
  unsafeUpdate :: KnowScene -> Event -> KnowScene
unsafeUpdate (kns :: KnowStruct
kns@(KnS [Prp]
props Bdd
_ [(Agent, [Prp])]
_),[Prp]
s) (KnowTransformer
ctrf, [Prp]
eventFactsUnshifted) = ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
newprops Bdd
newlaw [(Agent, [Prp])]
newobs, [Prp]
news) where
    -- PART 1: SHIFTING addprops to ensure props and newprops are disjoint
    (KnTrf [Prp]
addprops Form
_ [(Prp, Bdd)]
changelaw [(Agent, [Prp])]
_, [(Prp, Prp)]
shiftrel) = KnowStruct -> KnowTransformer -> (KnowTransformer, [(Prp, Prp)])
shiftPrepare KnowStruct
kns KnowTransformer
ctrf
    -- the actual event:
    eventFacts :: [Prp]
eventFacts = (Prp -> Prp) -> [Prp] -> [Prp]
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) [Prp]
eventFactsUnshifted
    -- PART 2: COPYING the modified propositions
    changeprops :: [Prp]
changeprops = ((Prp, Bdd) -> Prp) -> [(Prp, Bdd)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bdd) -> Prp
forall a b. (a, b) -> a
fst [(Prp, Bdd)]
changelaw
    copyrel :: [(Prp, Prp)]
copyrel = [Prp] -> [Prp] -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Prp]
changeprops [([Prp] -> Prp
freshp ([Prp] -> Prp) -> [Prp] -> Prp
forall a b. (a -> b) -> a -> b
$ [Prp]
props [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
addprops)..]
    -- do the pointless update and calculate new actual state
    KnS [Prp]
newprops Bdd
newlaw [(Agent, [Prp])]
newobs = KnowStruct -> KnowTransformer -> KnowStruct
forall a b. Update a b => a -> b -> a
unsafeUpdate KnowStruct
kns KnowTransformer
ctrf
    news :: [Prp]
news = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [[Prp]] -> [Prp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ [Prp]
s [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
changeprops
            , (Prp -> Prp) -> [Prp] -> [Prp]
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) ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp]
s [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
changeprops
            , [Prp]
eventFacts
            , (Prp -> Bool) -> [Prp] -> [Prp]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ Prp
p -> [Prp] -> Bdd -> Bool
bddEval ([Prp]
s [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
eventFacts) ([(Prp, Bdd)]
changelaw [(Prp, Bdd)] -> Prp -> Bdd
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Prp
p)) [Prp]
changeprops ]

instance Update KnowStruct KnowTransformer where
  checks :: [KnowStruct -> KnowTransformer -> Bool]
checks = [KnowStruct -> KnowTransformer -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents]
  unsafeUpdate :: KnowStruct -> KnowTransformer -> KnowStruct
unsafeUpdate KnowStruct
kns KnowTransformer
ctrf = [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
newprops Bdd
newlaw [(Agent, [Prp])]
newobs where
    (KnS [Prp]
newprops Bdd
newlaw [(Agent, [Prp])]
newobs, Bdd
_) = MultipointedKnowScene -> MultipointedEvent -> MultipointedKnowScene
forall a b. Update a b => a -> b -> a
unsafeUpdate (KnowStruct
kns,Bdd
forall a. HasCallStack => a
undefined::Bdd) (KnowTransformer
ctrf,Bdd
forall a. HasCallStack => a
undefined::Bdd) -- using laziness!

instance Update MultipointedKnowScene MultipointedEvent where
  unsafeUpdate :: MultipointedKnowScene -> MultipointedEvent -> MultipointedKnowScene
unsafeUpdate (kns :: KnowStruct
kns@(KnS [Prp]
props Bdd
law [(Agent, [Prp])]
obs),Bdd
statesBdd) (KnowTransformer
ctrf,Bdd
eventsBddUnshifted)  =
    ([Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
newprops Bdd
newlaw [(Agent, [Prp])]
newobs, Bdd
newStatesBDD) where
      (KnTrf [Prp]
addprops Form
addlaw [(Prp, Bdd)]
changelaw [(Agent, [Prp])]
eventObs, [(Prp, Prp)]
shiftrel) = KnowStruct -> KnowTransformer -> (KnowTransformer, [(Prp, Prp)])
shiftPrepare KnowStruct
kns KnowTransformer
ctrf
      -- apply the shifting to eventsBdd:
      eventsBdd :: Bdd
eventsBdd = [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
shiftrel Bdd
eventsBddUnshifted
      -- PART 2: COPYING the modified propositions
      changeprops :: [Prp]
changeprops = ((Prp, Bdd) -> Prp) -> [(Prp, Bdd)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bdd) -> Prp
forall a b. (a, b) -> a
fst [(Prp, Bdd)]
changelaw
      copyrel :: [(Prp, Prp)]
copyrel = [Prp] -> [Prp] -> [(Prp, Prp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Prp]
changeprops [([Prp] -> Prp
freshp ([Prp] -> Prp) -> [Prp] -> Prp
forall a b. (a -> b) -> a -> b
$ [Prp]
props [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
addprops)..]
      copychangeprops :: [Prp]
copychangeprops = ((Prp, Prp) -> Prp) -> [(Prp, Prp)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Prp) -> Prp
forall a b. (a, b) -> b
snd [(Prp, Prp)]
copyrel
      newprops :: [Prp]
newprops = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [Prp]
props [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
addprops [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [Prp]
copychangeprops -- V u V^+ u V^o
      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 (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns 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 ([(Prp, Bdd)]
changelaw [(Prp, Bdd)] -> Prp -> Bdd
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Prp
q) | Prp
q <- [Prp]
changeprops]
      newobs :: [(Agent, [Prp])]
newobs = [ (Agent
i , [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Prp -> Prp) -> [Prp] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map ([(Prp, Prp)] -> Prp -> Prp
forall a. Eq a => [(a, a)] -> a -> a
applyPartial [(Prp, Prp)]
copyrel) ([(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i) [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [(Agent, [Prp])]
eventObs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i) | Agent
i <- ((Agent, [Prp]) -> Agent) -> [(Agent, [Prp])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, [Prp]) -> Agent
forall a b. (a, b) -> a
fst [(Agent, [Prp])]
obs ]
      newStatesBDD :: Bdd
newStatesBDD = [Bdd] -> Bdd
conSet [ [(Prp, Prp)] -> Bdd -> Bdd
relabelWith [(Prp, Prp)]
copyrel Bdd
statesBdd, Bdd
eventsBdd ]

-- * /LaTeX/ functions

texBddWith :: (Int -> String) -> Bdd -> String
texBddWith :: (Int -> Agent) -> Bdd -> Agent
texBddWith Int -> Agent
myShow Bdd
b = IO Agent -> Agent
forall a. IO a -> a
unsafePerformIO (IO Agent -> Agent) -> IO Agent -> Agent
forall a b. (a -> b) -> a -> b
$ do
  Maybe Agent
haveDot2tex <- Agent -> IO (Maybe Agent)
findExecutable Agent
"dot2tex"
  case Maybe Agent
haveDot2tex of
    Maybe Agent
Nothing -> Agent -> IO Agent
forall a. HasCallStack => Agent -> a
error Agent
"Please install dot2tex which is needed to show BDDs."
    Just Agent
d2t -> do
      (Handle
i,Handle
o,Handle
_,ProcessHandle
_) <- Agent -> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveCommand (Agent -> IO (Handle, Handle, Handle, ProcessHandle))
-> Agent -> IO (Handle, Handle, Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$ Agent
d2t Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" --figpreamble=\"\\huge\" --figonly -traw"
      Handle -> Agent -> IO ()
hPutStr Handle
i ((Int -> Agent) -> Bdd -> Agent
genGraphWith Int -> Agent
myShow Bdd
b Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"\n")
      Handle -> IO ()
hClose Handle
i
      Agent
result <- Handle -> IO Agent
hGetContents Handle
o
      Agent -> IO Agent
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Agent -> IO Agent) -> Agent -> IO Agent
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhileEnd Char -> Bool
isSpace ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace Agent
result

texBDD :: Bdd -> String
texBDD :: Bdd -> Agent
texBDD = (Int -> Agent) -> Bdd -> Agent
texBddWith Int -> Agent
forall a. Show a => a -> Agent
show

newtype WrapBdd = Wrap Bdd

instance TexAble WrapBdd where
  tex :: WrapBdd -> Agent
tex (Wrap Bdd
b) = Bdd -> Agent
texBDD Bdd
b

instance TexAble KnowStruct where
  tex :: KnowStruct -> Agent
tex (KnS [Prp]
props Bdd
lawbdd [(Agent, [Prp])]
obs) = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Agent
" \\left( \n"
    , [Prp] -> Agent
forall a. TexAble a => a -> Agent
tex [Prp]
props Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
", "
    , Agent
" \\begin{array}{l} \\scalebox{0.4}{"
    , Bdd -> Agent
texBDD Bdd
lawbdd
    , Agent
"} \\end{array}\n "
    , Agent
", \\begin{array}{l}\n"
    , Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
" \\\\\n " (((Agent, [Prp]) -> Agent) -> [(Agent, [Prp])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (\(Agent
_,[Prp]
os) -> [Prp] -> Agent
forall a. TexAble a => a -> Agent
tex [Prp]
os) [(Agent, [Prp])]
obs)
    , Agent
"\\end{array}\n"
    , Agent
" \\right)" ]

instance TexAble KnowScene where
  tex :: KnowScene -> Agent
tex (KnowStruct
kns, [Prp]
state) = KnowStruct -> Agent
forall a. TexAble a => a -> Agent
tex KnowStruct
kns Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" , " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Prp] -> Agent
forall a. TexAble a => a -> Agent
tex [Prp]
state

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

instance TexAble KnowTransformer where
  tex :: KnowTransformer -> Agent
tex (KnTrf [Prp]
addprops Form
addlaw [(Prp, Bdd)]
changelaw [(Agent, [Prp])]
eventObs) = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ Agent
" \\left( \n"
    , [Prp] -> Agent
forall a. TexAble a => a -> Agent
tex [Prp]
addprops, Agent
", \\ "
    , Form -> Agent
forall a. TexAble a => a -> Agent
tex Form
addlaw, Agent
", \\ "
    , Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
", " ([Agent] -> Agent) -> [Agent] -> Agent
forall a b. (a -> b) -> a -> b
$ ((Prp, Bdd) -> Agent) -> [(Prp, Bdd)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bdd) -> Agent
forall {a}. TexAble a => (a, Bdd) -> Agent
texChange [(Prp, Bdd)]
changelaw
    , Agent
", \\ \\begin{array}{l}\n"
    , Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
" \\\\\n " (((Agent, [Prp]) -> Agent) -> [(Agent, [Prp])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (\(Agent
_,[Prp]
os) -> [Prp] -> Agent
forall a. TexAble a => a -> Agent
tex [Prp]
os) [(Agent, [Prp])]
eventObs)
    , Agent
"\\end{array}\n"
    , Agent
" \\right) \n"
    ] where
        texChange :: (a, Bdd) -> Agent
texChange (a
prop,Bdd
changebdd) = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ a -> Agent
forall a. TexAble a => a -> Agent
tex a
prop Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" := "
          , Agent
" \\begin{array}{l} \\scalebox{0.4}{"
          , Bdd -> Agent
texBDD Bdd
changebdd
          , Agent
"} \\end{array}\n " ]

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

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


-- * Reduction axioms for knowledge transformers

{- |
Adding knowledge transformers does not increase expressivity because we have
the following reductions.

For now we do not implement a separate type of formulas with dynamic operators
but instead implement the reduction axioms directly as a function which takes
an event and ``pushes it through'' a formula.

The following takes an event $\mathcal{X},x$ and a formula $\phi$ and then
``pushes'' $[\mathcal{X},x]$ through all boolean and epistemic operators in
$\phi$ until it disappears in front of atomic propositons.
This translation is global, i.e.\ if there is a reduced formula, then it is
equivalent to the original on all structures.
-}
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
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Form -> Maybe Form) -> Form -> Maybe Form
forall a b. (a -> b) -> a -> b
$ Form -> Form
Neg (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 (Prp -> Form
PrpF Prp
p) -- FIXME use change!
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 [Prp]
_ Form
_) = Maybe Form
forall a. Maybe a
Nothing
reduce Event
_ (Exists [Prp]
_ Form
_) = Maybe Form
forall a. Maybe a
Nothing
reduce event :: Event
event@(trf :: KnowTransformer
trf@(KnTrf [Prp]
addprops Form
_ [(Prp, Bdd)]
_ [(Agent, [Prp])]
obs), [Prp]
x) (K Agent
a Form
f) =
  Form -> Form -> Form
Impl (Event -> Form
forall a. HasPrecondition a => a -> Form
preOf Event
event) (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 (KnowTransformer
trf,[Prp]
y) Form
f | [Prp]
y <- [Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
addprops
                               , ([Prp]
x [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` ([(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
a)) [Prp] -> [Prp] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`seteq` ([Prp]
y [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` ([(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! 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 event :: Event
event@(trf :: KnowTransformer
trf@(KnTrf [Prp]
addprops Form
_ [(Prp, Bdd)]
_ [(Agent, [Prp])]
obs), [Prp]
x) (Dk [Agent]
ags Form
f) =
  Form -> Form -> Form
Impl (Event -> Form
forall a. HasPrecondition a => a -> Form
preOf Event
event) (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 (KnowTransformer
trf,[Prp]
y) Form
f | [Prp]
y <- [Prp] -> [[Prp]]
forall a. [a] -> [[a]]
powerset [Prp]
addprops,
       ([Prp] -> Bool) -> [[Prp]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[Prp]
oi -> ([Prp]
x [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi) [Prp] -> [Prp] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`seteq` ([Prp]
y [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Prp]
oi))
       [[(Agent, [Prp])]
obs [(Agent, [Prp])] -> Agent -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i | Agent
i <- [Agent]
ags]
    ]
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

-- * Random Knowledge Structures

-- | Generating random knowledge structures for QuickCheck. -- FIXME: not showing up in Haddock?
instance Arbitrary KnowStruct where
  arbitrary :: Gen KnowStruct
arbitrary = do
    Int
numExtraVars <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0,Int
2)
    let myVocabulary :: [Prp]
myVocabulary = [Prp]
defaultVocabulary [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ Int -> [Prp] -> [Prp]
forall a. Int -> [a] -> [a]
take Int
numExtraVars [[Prp] -> Prp
freshp [Prp]
defaultVocabulary ..]
    (BF Form
statelaw) <- (Int -> Gen BF) -> Gen BF
forall a. (Int -> Gen a) -> Gen a
sized ([Prp] -> Int -> Gen BF
randomboolformWith [Prp]
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, [Prp])]
obs <- (Agent -> Gen (Agent, [Prp])) -> [Agent] -> Gen [(Agent, [Prp])]
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
      [Prp]
obsVars <- [Prp] -> Gen [Prp]
forall a. [a] -> Gen [a]
sublistOf [Prp]
myVocabulary
      (Agent, [Prp]) -> Gen (Agent, [Prp])
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Agent
i,[Prp]
obsVars)
      ) [Agent]
defaultAgents
    KnowStruct -> Gen KnowStruct
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (KnowStruct -> Gen KnowStruct) -> KnowStruct -> Gen KnowStruct
forall a b. (a -> b) -> a -> b
$ [Prp] -> Bdd -> [(Agent, [Prp])] -> KnowStruct
KnS [Prp]
myVocabulary (Form -> Bdd
boolBddOf Form
statelaw) [(Agent, [Prp])]
obs
  shrink :: KnowStruct -> [KnowStruct]
shrink KnowStruct
kns = [ [Prp] -> KnowStruct -> KnowStruct
withoutProps [Prp
p] KnowStruct
kns | [Prp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (KnowStruct -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KnowStruct
kns) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1, Prp
p <- KnowStruct -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KnowStruct
kns [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
defaultVocabulary ]