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

module SMCDEL.Symbolic.S5_DD where

import Control.Arrow (first,second,(***))
import Data.Char (isSpace)
import Data.DecisionDiagram.BDD hiding (existsSet,restrict,restrictSet,lfp)
import qualified Data.DecisionDiagram.BDD
import Data.Dynamic
import qualified Data.IntMap
import qualified Data.IntSet
import Data.List ((\\),delete,dropWhileEnd,intercalate,intersect,nub,sort)
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.TexDisplay
import SMCDEL.Language

-- * Renaming functions from `decision-diagrams` to be like HasCacBDD.

type Bdd = BDD AscOrder

top, bot :: Bdd
top :: Bdd
top = Bdd
forall a. BDD a
true
bot :: Bdd
bot = Bdd
forall a. BDD a
false
neg :: Bdd -> Bdd
neg :: Bdd -> Bdd
neg = Bdd -> Bdd
forall a. BDD a -> BDD a
notB

con, dis, imp, equ :: Bdd -> Bdd -> Bdd
con :: Bdd -> Bdd -> Bdd
con = Bdd -> Bdd -> Bdd
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
(Data.DecisionDiagram.BDD..&&.)
dis :: Bdd -> Bdd -> Bdd
dis = Bdd -> Bdd -> Bdd
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
(Data.DecisionDiagram.BDD..||.)
imp :: Bdd -> Bdd -> Bdd
imp = Bdd -> Bdd -> Bdd
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
(Data.DecisionDiagram.BDD..=>.)
equ :: Bdd -> Bdd -> Bdd
equ = Bdd -> Bdd -> Bdd
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
(Data.DecisionDiagram.BDD..<=>.)
conSet, disSet, xorSet :: [Bdd] -> Bdd
conSet :: [Bdd] -> Bdd
conSet = [Bdd] -> Bdd
forall (f :: * -> *) a.
(Foldable f, ItemOrder a) =>
f (BDD a) -> BDD a
andB
disSet :: [Bdd] -> Bdd
disSet = [Bdd] -> Bdd
forall (f :: * -> *) a.
(Foldable f, ItemOrder a) =>
f (BDD a) -> BDD a
orB
xorSet :: [Bdd] -> Bdd
xorSet [] = Bdd
bot
xorSet (Bdd
b:[Bdd]
bs) = (Bdd -> Bdd -> Bdd) -> Bdd -> [Bdd] -> Bdd
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Bdd -> Bdd -> Bdd
forall a. ItemOrder a => BDD a -> BDD a -> BDD a
xor Bdd
b [Bdd]
bs

forallSet, existsSet :: [Int] -> Bdd -> Bdd
forallSet :: [Int] -> Bdd -> Bdd
forallSet [Int]
l = IntSet -> Bdd -> Bdd
forall a. ItemOrder a => IntSet -> BDD a -> BDD a
forAllSet ([Int] -> IntSet
Data.IntSet.fromList [Int]
l)
existsSet :: [Int] -> Bdd -> Bdd
existsSet [Int]
l = IntSet -> Bdd -> Bdd
forall a. ItemOrder a => IntSet -> BDD a -> BDD a
Data.DecisionDiagram.BDD.existsSet ([Int] -> IntSet
Data.IntSet.fromList [Int]
l)

ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd
ifthenelse :: Bdd -> Bdd -> Bdd -> Bdd
ifthenelse = Bdd -> Bdd -> Bdd -> Bdd
forall a. ItemOrder a => BDD a -> BDD a -> BDD a -> BDD a
Data.DecisionDiagram.BDD.ite

substit :: Int -> Bdd -> Bdd -> Bdd
substit :: Int -> Bdd -> Bdd -> Bdd
substit = Int -> Bdd -> Bdd -> Bdd
forall a. ItemOrder a => Int -> BDD a -> BDD a -> BDD a
subst

substitSimul :: [(Int, Bdd)] -> Bdd -> Bdd
substitSimul :: [(Int, Bdd)] -> Bdd -> Bdd
substitSimul [(Int, Bdd)]
ibs = IntMap Bdd -> Bdd -> Bdd
forall a. ItemOrder a => IntMap (BDD a) -> BDD a -> BDD a
substSet ([(Int, Bdd)] -> IntMap Bdd
forall a. [(Int, a)] -> IntMap a
Data.IntMap.fromList [(Int, Bdd)]
ibs)

relabel :: [(Int,Int)] -> Bdd -> Bdd
relabel :: [(Int, Int)] -> Bdd -> Bdd
relabel = [(Int, Bdd)] -> Bdd -> Bdd
substitSimul ([(Int, Bdd)] -> Bdd -> Bdd)
-> ([(Int, Int)] -> [(Int, Bdd)]) -> [(Int, Int)] -> Bdd -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Int) -> (Int, Bdd)) -> [(Int, Int)] -> [(Int, Bdd)]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Bdd) -> (Int, Int) -> (Int, Bdd)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Bdd
forall a. Int -> BDD a
var)

sizeOf :: Bdd -> Int
sizeOf :: Bdd -> Int
sizeOf = Bdd -> Int
forall a. BDD a -> Int
numNodes

evaluateFun :: Bdd -> (Int -> Bool) -> Bool
evaluateFun :: Bdd -> (Int -> Bool) -> Bool
evaluateFun = ((Int -> Bool) -> Bdd -> Bool) -> Bdd -> (Int -> Bool) -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Int -> Bool) -> Bdd -> Bool
forall a. (Int -> Bool) -> BDD a -> Bool
evaluate

allSatsWith :: [Int] -> Bdd -> [[(Int,Bool)]]
allSatsWith :: [Int] -> Bdd -> [[(Int, Bool)]]
allSatsWith [Int]
ints = (IntMap Bool -> [(Int, Bool)]) -> [IntMap Bool] -> [[(Int, Bool)]]
forall a b. (a -> b) -> [a] -> [b]
map IntMap Bool -> [(Int, Bool)]
forall a. IntMap a -> [(Int, a)]
Data.IntMap.toList ([IntMap Bool] -> [[(Int, Bool)]])
-> (Bdd -> [IntMap Bool]) -> Bdd -> [[(Int, Bool)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Bdd -> [IntMap Bool]
forall a. ItemOrder a => IntSet -> BDD a -> [IntMap Bool]
allSatComplete ([Int] -> IntSet
Data.IntSet.fromList [Int]
ints)

satCountWith :: [Int] -> Bdd -> Integer
satCountWith :: [Int] -> Bdd -> Integer
satCountWith [Int]
ps = IntSet -> Bdd -> Integer
forall a b.
(ItemOrder a, Num b, Bits b, HasCallStack) =>
IntSet -> BDD a -> b
countSat ([Int] -> IntSet
Data.IntSet.fromList [Int]
ps)

restrict :: Bdd -> (Int,Bool) -> Bdd
restrict :: Bdd -> (Int, Bool) -> Bdd
restrict Bdd
b (Int
k,Bool
bit) = Int -> Bool -> Bdd -> Bdd
forall a. ItemOrder a => Int -> Bool -> BDD a -> BDD a
Data.DecisionDiagram.BDD.restrict Int
k Bool
bit Bdd
b

restrictSet :: Bdd -> [(Int,Bool)] -> Bdd
restrictSet :: Bdd -> [(Int, Bool)] -> Bdd
restrictSet Bdd
b [(Int, Bool)]
ass = IntMap Bool -> Bdd -> Bdd
forall a. ItemOrder a => IntMap Bool -> BDD a -> BDD a
Data.DecisionDiagram.BDD.restrictSet ([(Int, Bool)] -> IntMap Bool
forall a. [(Int, a)] -> IntMap a
Data.IntMap.fromList [(Int, Bool)]
ass) Bdd
b

genGraphWith :: (Int -> String) -> Bdd -> String
genGraphWith :: (Int -> Agent) -> Bdd -> Agent
genGraphWith = (Int -> Agent) -> Bdd -> Agent
forall a. HasCallStack => a
undefined -- TODO, via graph library?

formOf :: Bdd -> Form
formOf :: Bdd -> Form
formOf = Form -> Form
simplify (Form -> Form) -> (Bdd -> Form) -> Bdd -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bdd -> Form
formOf' where
  formOf' :: Bdd -> Form
  formOf' :: Bdd -> Form
formOf' (Leaf Bool
False) = Form
SMCDEL.Language.Bot
  formOf' (Leaf Bool
True) = Form
SMCDEL.Language.Top
  formOf' (Branch Int
n (Leaf Bool
True)  (Leaf Bool
False)) = Prp -> Form
PrpF (Int -> Prp
P Int
n)
  formOf' (Branch Int
n (Leaf Bool
False) (Leaf Bool
True)) = Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
n)
  formOf' (Branch Int
n (Leaf Bool
True) Bdd
right) = [Form] -> Form
Disj [ Prp -> Form
PrpF (Int -> Prp
P Int
n), Bdd -> Form
formOf' Bdd
right ]
  formOf' (Branch Int
n (Leaf Bool
False) Bdd
right) = [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
n), Bdd -> Form
formOf' Bdd
right ]
  formOf' (Branch Int
n Bdd
left (Leaf Bool
True)) = [Form] -> Form
Disj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
n), Bdd -> Form
formOf' Bdd
left ]
  formOf' (Branch Int
n Bdd
left (Leaf Bool
False)) = [Form] -> Form
Conj [ Prp -> Form
PrpF (Int -> Prp
P Int
n), Bdd -> Form
formOf' Bdd
left ]
  formOf' (Branch Int
n Bdd
left Bdd
right) =
    [Form] -> Form
Disj [ [Form] -> Form
Conj [ Prp -> Form
PrpF (Int -> Prp
P Int
n), Bdd -> Form
formOf' Bdd
left ] ,
            [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
n), Bdd -> Form
formOf' Bdd
right ] ]

boolBddOf :: Form -> Bdd
boolBddOf :: Form -> Bdd
boolBddOf Form
Top           = Bdd
top
boolBddOf Form
Bot           = Bdd
bot
boolBddOf (PrpF (P Int
n))  = Int -> Bdd
forall a. Int -> BDD a
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."

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

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.
-- TODO: check if this is correct / agrees with CacBDD.
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

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)

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)

type State = [Prp]

instance Pointed KnowStruct State
type KnowScene = (KnowStruct,State)

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

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 = ([(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)]] -> [[(Prp, Bool)]])
-> [[(Int, Bool)]] -> [[(Prp, Bool)]]
forall a b. (a -> b) -> a -> b
$ [Int] -> Bdd -> [[(Int, Bool)]]
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 -> Integer
numberOfStates :: KnowStruct -> Integer
numberOfStates (KnS [Prp]
props Bdd
lawbdd [(Agent, [Prp])]
_) = [Int] -> Bdd -> Integer
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

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 ]

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)

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

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
forall a. Int -> BDD a
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!"

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
forall a. Int -> BDD a
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
forall a. ItemOrder a => (BDD a -> BDD a) -> BDD a
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 -> [(Int, Bool)] -> Bdd
`restrictSet` [(Int, Bool)]
actualAss) )
          where actualAss :: [(Int, Bool)]
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 =
 ([(Int, Bool)] -> [Prp]) -> [[(Int, Bool)]] -> [[Prp]]
forall a b. (a -> b) -> [a] -> [b]
map ([Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp])
-> ([(Int, Bool)] -> [Prp]) -> [(Int, Bool)] -> [Prp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Bool) -> Prp) -> [(Int, Bool)] -> [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) ([(Int, Bool)] -> [Prp])
-> ([(Int, Bool)] -> [(Int, Bool)]) -> [(Int, Bool)] -> [Prp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((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)]] -> [[Prp]]) -> [[(Int, Bool)]] -> [[Prp]]
forall a b. (a -> b) -> a -> b
$
   [Int] -> Bdd -> [[(Int, Bool)]]
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 -> [[(Int, Bool)]]) -> Bdd -> [[(Int, Bool)]]
forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd -> Bdd
con Bdd
lawbdd (KnowStruct -> Form -> Bdd
bddOf KnowStruct
kns Form
f)

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
SMCDEL.Symbolic.S5_DD.substit (Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
p) (Int -> Bdd
forall a. Int -> BDD a
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)

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
SMCDEL.Symbolic.S5_DD.substit) Bdd
intermediateStatesBdd [ (Prp -> Int
forall a. Enum a => a -> Int
fromEnum Prp
p, Int -> Bdd
forall a. Int -> BDD a
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

-- REMOVED: Propulation etc.

-- * 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 ])

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
forall a. Int -> BDD a
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 ]

-- * Visualization

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)" ]

-- * Syntactic Reduction

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]
a Form
f)     = Event -> Form -> Maybe Form
reduce Event
e ([Form] -> Form
Disj [[Agent] -> Form -> Form
Dk [Agent]
a Form
f, [Agent] -> Form -> Form
Dk [Agent]
a (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

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 ]