{-# LANGUAGE TupleSections #-}

{- | Converting between S5 Kripke Models and Knowledge Structures

In this module we define and implement translation methods to connect the
semantics from the two previous sections. This essentially allows us to switch
back and forth between explicit and symbolic model checking methods.
-}

module SMCDEL.Translations.S5 where

import Data.Containers.ListUtils (nubOrd)
import Data.HasCacBDD hiding (Top,Bot)
import Data.List (groupBy,sort,(\\),elemIndex,intersect)
import Data.Maybe (listToMaybe,fromJust)

import SMCDEL.Language
import SMCDEL.Symbolic.S5
import SMCDEL.Explicit.S5
import SMCDEL.Internal.Help (anydiffWith,alldiff,alleqWith,apply,powerset,(!),seteq,subseteq)
import SMCDEL.Other.BDD2Form

-- * Tools for Equivalence

-- | A function mapping worlds to states.
type StateMap = World -> State

equivalentWith :: PointedModelS5 -> KnowScene -> StateMap -> Bool
equivalentWith :: PointedModelS5 -> KnowScene -> StateMap -> Bool
equivalentWith (KrMS5 [Action]
ws [(Agent, Partition)]
rel [(Action, Assignment)]
val, Action
actw) (kns :: KnowStruct
kns@(KnS State
_ Bdd
_ [(Agent, State)]
obs), State
curs) StateMap
g =
  Bool
c1 Bool -> Bool -> Bool
&& Bool
c2 Bool -> Bool -> Bool
&& Bool
c3 Bool -> Bool -> Bool
&& StateMap
g Action
actw State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
curs where
    c1 :: Bool
c1 = ((Agent, Action, Action) -> Bool)
-> [(Agent, Action, Action)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Agent, Action, Action)
l -> (Agent, Action, Action) -> Bool
knsLink (Agent, Action, Action)
l Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (Agent, Action, Action) -> Bool
kriLink (Agent, Action, Action)
l) [(Agent, Action, Action)]
linkSet where
      linkSet :: [(Agent, Action, Action)]
linkSet = [ (Agent
i,Action
w1,Action
w2) | Action
w1 <- [Action]
ws, Action
w2 <- [Action]
ws, Action
w1 Action -> Action -> Bool
forall a. Ord a => a -> a -> Bool
<= Action
w2, Agent
i <- ((Agent, Partition) -> Agent) -> [(Agent, Partition)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, Partition) -> Agent
forall a b. (a, b) -> a
fst [(Agent, Partition)]
rel ]
      knsLink :: (Agent, Action, Action) -> Bool
knsLink (Agent
i,Action
w1,Action
w2) = let oi :: State
oi = [(Agent, State)]
obs [(Agent, State)] -> Agent -> State
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i in (StateMap
g Action
w1 State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
`intersect` State
oi) State -> State -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`seteq` (StateMap
g Action
w2 State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
`intersect` State
oi)
      kriLink :: (Agent, Action, Action) -> Bool
kriLink (Agent
i,Action
w1,Action
w2) = ([Action] -> Bool) -> Partition -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\[Action]
p -> Action
w1 Action -> [Action] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Action]
p Bool -> Bool -> Bool
&& Action
w2 Action -> [Action] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Action]
p) ([(Agent, Partition)]
rel [(Agent, Partition)] -> Agent -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i)
    c2 :: Bool
c2 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ (Prp
p Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` StateMap
g Action
w) Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (([(Action, Assignment)]
val [(Action, Assignment)] -> Action -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Action
w) Assignment -> Prp -> Bool
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Prp
p) | Action
w <- [Action]
ws, Prp
p <- ((Prp, Bool) -> Prp) -> Assignment -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst ((Action, Assignment) -> Assignment
forall a b. (a, b) -> b
snd ((Action, Assignment) -> Assignment)
-> (Action, Assignment) -> Assignment
forall a b. (a -> b) -> a -> b
$ [(Action, Assignment)] -> (Action, Assignment)
forall a. HasCallStack => [a] -> a
head [(Action, Assignment)]
val) ]
    c3 :: Bool
c3 = KnowStruct -> [State]
statesOf KnowStruct
kns [State] -> [State] -> Bool
forall a. Ord a => [a] -> [a] -> Bool
`seteq` [State] -> [State]
forall a. Ord a => [a] -> [a]
nubOrd (StateMap -> [Action] -> [State]
forall a b. (a -> b) -> [a] -> [b]
map StateMap
g [Action]
ws)

findStateMap :: PointedModelS5 -> KnowScene -> Maybe StateMap
findStateMap :: PointedModelS5 -> KnowScene -> Maybe StateMap
findStateMap pm :: PointedModelS5
pm@(KrMS5 [Action]
_ [(Agent, Partition)]
_ [(Action, Assignment)]
val, Action
w) scn :: KnowScene
scn@(KnowStruct
kns, State
s)
  | PointedModelS5 -> State
forall a. HasVocab a => a -> State
vocabOf PointedModelS5
pm State -> State -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`subseteq` KnowStruct -> State
forall a. HasVocab a => a -> State
vocabOf KnowStruct
kns = [StateMap] -> Maybe StateMap
forall a. [a] -> Maybe a
listToMaybe [StateMap]
goodMaps
  | Bool
otherwise = Agent -> Maybe StateMap
forall a. HasCallStack => Agent -> a
error Agent
"vocabOf pm not subseteq vocabOf kns"
  where
    extraProps :: State
extraProps = KnowStruct -> State
forall a. HasVocab a => a -> State
vocabOf KnowStruct
kns State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ PointedModelS5 -> State
forall a. HasVocab a => a -> State
vocabOf PointedModelS5
pm
    allFuncs :: Eq a => [a] -> [b] -> [a -> b]
    allFuncs :: forall a b. Eq a => [a] -> [b] -> [a -> b]
allFuncs []     [b]
_  = [ b -> a -> b
forall a b. a -> b -> a
const b
forall a. HasCallStack => a
undefined ]
    allFuncs (a
x:[a]
xs) [b]
ys = [ \a
a -> if a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x then b
y else a -> b
f a
a | b
y <- [b]
ys, a -> b
f <- [a] -> [b] -> [a -> b]
forall a b. Eq a => [a] -> [b] -> [a -> b]
allFuncs [a]
xs [b]
ys ]
    allMaps, goodMaps :: [StateMap]
    baseMap :: StateMap
baseMap  = ((Prp, Bool) -> Prp) -> Assignment -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst (Assignment -> State) -> (Action -> Assignment) -> StateMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Prp, Bool) -> Bool) -> Assignment -> Assignment
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp, Bool) -> Bool
forall a b. (a, b) -> b
snd (Assignment -> Assignment)
-> (Action -> Assignment) -> Action -> Assignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Action, Assignment)]
val [(Action, Assignment)] -> Action -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
!)
    allMaps :: [StateMap]
allMaps  = [ \Action
v -> StateMap
baseMap Action
v State -> State -> State
forall a. [a] -> [a] -> [a]
++ StateMap
restf Action
v | StateMap
restf <- [Action] -> [State] -> [StateMap]
forall a b. Eq a => [a] -> [b] -> [a -> b]
allFuncs (PointedModelS5 -> [Action]
forall a. HasWorlds a => a -> [Action]
worldsOf PointedModelS5
pm) (State -> [State]
forall a. [a] -> [[a]]
powerset State
extraProps) ]
    goodMaps :: [StateMap]
goodMaps = (StateMap -> Bool) -> [StateMap] -> [StateMap]
forall a. (a -> Bool) -> [a] -> [a]
filter (\StateMap
g -> StateMap
g Action
w State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
s Bool -> Bool -> Bool
&& PointedModelS5 -> KnowScene -> StateMap -> Bool
equivalentWith PointedModelS5
pm KnowScene
scn StateMap
g) [StateMap]
allMaps

-- * From Knowledge Structures to S5 Kripke Models


knsToKripke :: KnowScene -> PointedModelS5
knsToKripke :: KnowScene -> PointedModelS5
knsToKripke (KnowStruct
kns, State
curState) = (KripkeModelS5
m, Action
curWorld) where
  (m :: KripkeModelS5
m@(KrMS5 [Action]
worlds [(Agent, Partition)]
_ [(Action, Assignment)]
_), StateMap
g) = KnowStruct -> (KripkeModelS5, StateMap)
knsToKripkeWithG KnowStruct
kns
  curWorld :: Action
curWorld = case [ Action
w | Action
w <- [Action]
worlds, StateMap
g Action
w State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
curState ] of
    [Action
cW] -> Action
cW
    [Action]
_    -> Agent -> Action
forall a. HasCallStack => Agent -> a
error Agent
"knsToKripke failed: Invalid current state."

knsToKripkeWithG :: KnowStruct -> (KripkeModelS5, StateMap)
knsToKripkeWithG :: KnowStruct -> (KripkeModelS5, StateMap)
knsToKripkeWithG kns :: KnowStruct
kns@(KnS State
ps Bdd
_ [(Agent, State)]
obs) =
  ([Action]
-> [(Agent, Partition)] -> [(Action, Assignment)] -> KripkeModelS5
KrMS5 [Action]
worlds [(Agent, Partition)]
rel [(Action, Assignment)]
val, StateMap
g) where
    g :: StateMap
g Action
w    = KnowStruct -> [State]
statesOf KnowStruct
kns [State] -> StateMap
forall a. HasCallStack => [a] -> Action -> a
!! Action
w
    lav :: [(State, Action)]
lav    = [State] -> [Action] -> [(State, Action)]
forall a b. [a] -> [b] -> [(a, b)]
zip (KnowStruct -> [State]
statesOf KnowStruct
kns) [Action
0..([State] -> Action
forall a. [a] -> Action
forall (t :: * -> *) a. Foldable t => t a -> Action
length (KnowStruct -> [State]
statesOf KnowStruct
kns)Action -> Action -> Action
forall a. Num a => a -> a -> a
-Action
1)]
    val :: [(Action, Assignment)]
val    = ((State, Action) -> (Action, Assignment))
-> [(State, Action)] -> [(Action, Assignment)]
forall a b. (a -> b) -> [a] -> [b]
map ( \(State
s,Action
n) -> (Action
n,State -> Assignment
forall {t :: * -> *}. Foldable t => t Prp -> Assignment
state2kripkeass State
s) ) [(State, Action)]
lav where
      state2kripkeass :: t Prp -> Assignment
state2kripkeass t Prp
s = (Prp -> (Prp, Bool)) -> State -> Assignment
forall a b. (a -> b) -> [a] -> [b]
map (\Prp
p -> (Prp
p, Prp
p Prp -> t Prp -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Prp
s)) State
ps
    rel :: [(Agent, Partition)]
rel    = [(Agent
i,Agent -> Partition
rfor Agent
i) | Agent
i <- ((Agent, State) -> Agent) -> [(Agent, State)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, State) -> Agent
forall a b. (a, b) -> a
fst [(Agent, State)]
obs]
    rfor :: Agent -> Partition
rfor Agent
i = ([(State, Action)] -> [Action]) -> [[(State, Action)]] -> Partition
forall a b. (a -> b) -> [a] -> [b]
map (((State, Action) -> Action) -> [(State, Action)] -> [Action]
forall a b. (a -> b) -> [a] -> [b]
map (State, Action) -> Action
forall a b. (a, b) -> b
snd) (((State, Action) -> (State, Action) -> Bool)
-> [(State, Action)] -> [[(State, Action)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy ( \ (State
x,Action
_) (State
y,Action
_) -> State
xState -> State -> Bool
forall a. Eq a => a -> a -> Bool
==State
y ) ([(State, Action)] -> [(State, Action)]
forall a. Ord a => [a] -> [a]
sort [(State, Action)]
pairs)) where
      pairs :: [(State, Action)]
pairs = (State -> (State, Action)) -> [State] -> [(State, Action)]
forall a b. (a -> b) -> [a] -> [b]
map (\State
s -> (State
s State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
`intersect` ([(Agent, State)]
obs [(Agent, State)] -> Agent -> State
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i), [(State, Action)]
lav [(State, Action)] -> State -> Action
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! State
s)) (KnowStruct -> [State]
statesOf KnowStruct
kns)
    worlds :: [Action]
worlds = ((State, Action) -> Action) -> [(State, Action)] -> [Action]
forall a b. (a -> b) -> [a] -> [b]
map (State, Action) -> Action
forall a b. (a, b) -> b
snd [(State, Action)]
lav

knsToKripkeMulti :: MultipointedKnowScene -> MultipointedModelS5
knsToKripkeMulti :: MultipointedKnowScene -> MultipointedModelS5
knsToKripkeMulti (KnowStruct
kns,Bdd
statesBdd) = (KripkeModelS5
m, [Action]
ws) where
  (KripkeModelS5
m, StateMap
g) = KnowStruct -> (KripkeModelS5, StateMap)
knsToKripkeWithG KnowStruct
kns
  ws :: [Action]
ws = (Action -> Bool) -> [Action] -> [Action]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Action
w -> Bdd -> (Action -> Bool) -> Bool
evaluateFun Bdd
statesBdd (\Action
k -> Action -> Prp
P Action
k Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` StateMap
g Action
w)) (KripkeModelS5 -> [Action]
forall a. HasWorlds a => a -> [Action]
worldsOf KripkeModelS5
m)

-- *  From S5 Kripke Models to Knowledge Structures


kripkeToKns :: PointedModelS5 -> KnowScene
kripkeToKns :: PointedModelS5 -> KnowScene
kripkeToKns (KripkeModelS5
m, Action
curWorld) = (KnowStruct
kns, State
curState) where
    (KnowStruct
kns, StateMap
g)  = KripkeModelS5 -> (KnowStruct, StateMap)
kripkeToKnsWithG KripkeModelS5
m
    curState :: State
curState  = State -> State
forall a. Ord a => [a] -> [a]
sort (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ StateMap
g Action
curWorld

kripkeToKnsWithG :: KripkeModelS5 -> (KnowStruct, StateMap)
kripkeToKnsWithG :: KripkeModelS5 -> (KnowStruct, StateMap)
kripkeToKnsWithG m :: KripkeModelS5
m@(KrMS5 [Action]
worlds [(Agent, Partition)]
rel [(Action, Assignment)]
val) = (State -> Bdd -> [(Agent, State)] -> KnowStruct
KnS State
ps Bdd
law [(Agent, State)]
obs, StateMap
g) where
  v :: State
v         = KripkeModelS5 -> State
forall a. HasVocab a => a -> State
vocabOf KripkeModelS5
m
  ags :: [Agent]
ags       = ((Agent, Partition) -> Agent) -> [(Agent, Partition)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, Partition) -> Agent
forall a b. (a, b) -> a
fst [(Agent, Partition)]
rel
  newpstart :: Action
newpstart = Prp -> Action
forall a. Enum a => a -> Action
fromEnum (Prp -> Action) -> Prp -> Action
forall a b. (a -> b) -> a -> b
$ State -> Prp
freshp State
v -- start counting new propositions here
  amount :: Agent -> b
amount Agent
i  = Float -> b
forall b. Integral b => Float -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Float -> Float -> Float
forall a. Floating a => a -> a -> a
logBase Float
2 (Action -> Float
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Action -> Float) -> Action -> Float
forall a b. (a -> b) -> a -> b
$ Partition -> Action
forall a. [a] -> Action
forall (t :: * -> *) a. Foldable t => t a -> Action
length ([(Agent, Partition)]
rel [(Agent, Partition)] -> Agent -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i)) :: Float) -- = |O_i|
  newpstep :: Action
newpstep  = [Action] -> Action
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ Agent -> Action
forall {b}. Integral b => Agent -> b
amount Agent
i | Agent
i <- [Agent]
ags ]
  newps :: Agent -> State
newps Agent
i   = (Action -> Prp) -> [Action] -> State
forall a b. (a -> b) -> [a] -> [b]
map (\Action
k -> Action -> Prp
P (Action
newpstart Action -> Action -> Action
forall a. Num a => a -> a -> a
+ (Action
newpstep Action -> Action -> Action
forall a. Num a => a -> a -> a
* Action
inum) Action -> Action -> Action
forall a. Num a => a -> a -> a
+Action
k)) [Action
0..(Agent -> Action
forall {b}. Integral b => Agent -> b
amount Agent
i Action -> Action -> Action
forall a. Num a => a -> a -> a
- Action
1)] -- O_i
    where inum :: Action
inum = Maybe Action -> Action
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Action -> Action) -> Maybe Action -> Action
forall a b. (a -> b) -> a -> b
$ Agent -> [Agent] -> Maybe Action
forall a. Eq a => a -> [a] -> Maybe Action
elemIndex Agent
i (((Agent, Partition) -> Agent) -> [(Agent, Partition)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, Partition) -> Agent
forall a b. (a, b) -> a
fst [(Agent, Partition)]
rel)
  copyrel :: Agent -> [([Action], State)]
copyrel Agent
i = Partition -> [State] -> [([Action], State)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([(Agent, Partition)]
rel [(Agent, Partition)] -> Agent -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i) (State -> [State]
forall a. [a] -> [[a]]
powerset (Agent -> State
newps Agent
i)) -- label equiv.classes with P(O_i)
  gag :: Agent -> StateMap
gag Agent
i Action
w   = ([Action], State) -> State
forall a b. (a, b) -> b
snd (([Action], State) -> State) -> ([Action], State) -> State
forall a b. (a -> b) -> a -> b
$ [([Action], State)] -> ([Action], State)
forall a. HasCallStack => [a] -> a
head ([([Action], State)] -> ([Action], State))
-> [([Action], State)] -> ([Action], State)
forall a b. (a -> b) -> a -> b
$ (([Action], State) -> Bool)
-> [([Action], State)] -> [([Action], State)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\([Action]
ws,State
_) -> Action
w Action -> [Action] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Action]
ws) (Agent -> [([Action], State)]
copyrel Agent
i)
  g :: StateMap
g Action
w       = (Prp -> Bool) -> State -> State
forall a. (a -> Bool) -> [a] -> [a]
filter (Assignment -> Prp -> Bool
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply ([(Action, Assignment)]
val [(Action, Assignment)] -> Action -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Action
w)) State
v State -> State -> State
forall a. [a] -> [a] -> [a]
++ [State] -> State
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Agent -> StateMap
gag Agent
i Action
w | Agent
i <- [Agent]
ags ]
  ps :: State
ps        = State
v State -> State -> State
forall a. [a] -> [a] -> [a]
++ [State] -> State
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Agent -> State
newps Agent
i | Agent
i <- [Agent]
ags ]
  law :: Bdd
law       = [Bdd] -> Bdd
disSet [ State -> State -> Bdd
booloutof (StateMap
g Action
w) State
ps | Action
w <- [Action]
worlds ]
  obs :: [(Agent, State)]
obs       = [ (Agent
i,Agent -> State
newps Agent
i) | Agent
i<- [Agent]
ags ]

-- | BDD to say that exactly this subset of a given vocabulary is true.
booloutof :: [Prp] -> [Prp] -> Bdd
booloutof :: State -> State -> Bdd
booloutof State
ps State
qs = [Bdd] -> Bdd
conSet ([Bdd] -> Bdd) -> [Bdd] -> Bdd
forall a b. (a -> b) -> a -> b
$
  [ Action -> Bdd
var Action
n | (P Action
n) <- State
ps ] [Bdd] -> [Bdd] -> [Bdd]
forall a. [a] -> [a] -> [a]
++
  [ Bdd -> Bdd
neg (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ Action -> Bdd
var Action
n | (P Action
n) <- State
qs State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ State
ps ]

-- | Convert a multipointed S5 Kripke model to a knoweldge structure.
-- See also `smartKripkeToKns`.
kripkeToKnsMulti :: MultipointedModelS5 -> MultipointedKnowScene
kripkeToKnsMulti :: MultipointedModelS5 -> MultipointedKnowScene
kripkeToKnsMulti (KripkeModelS5
model, [Action]
curWorlds) = (KnowStruct
kns, Bdd
curStatesLaw) where
  (KnowStruct
kns, StateMap
g) = KripkeModelS5 -> (KnowStruct, StateMap)
kripkeToKnsWithG KripkeModelS5
model
  curStatesLaw :: Bdd
curStatesLaw = [Bdd] -> Bdd
disSet [ State -> State -> Bdd
booloutof (StateMap
g Action
w) (KnowStruct -> State
forall a. HasVocab a => a -> State
vocabOf KnowStruct
kns) | Action
w <- [Action]
curWorlds ]

uniqueVals :: KripkeModelS5 -> Bool
uniqueVals :: KripkeModelS5 -> Bool
uniqueVals (KrMS5 [Action]
_ [(Agent, Partition)]
_ [(Action, Assignment)]
val) = [Assignment] -> Bool
forall a. Eq a => [a] -> Bool
alldiff (((Action, Assignment) -> Assignment)
-> [(Action, Assignment)] -> [Assignment]
forall a b. (a -> b) -> [a] -> [b]
map (Action, Assignment) -> Assignment
forall a b. (a, b) -> b
snd [(Action, Assignment)]
val)

-- | Get lists of variables which agent i does (not) observe
-- in model m. This does *not* preserve all information, i.e.
-- does not characterize every possible S5 relation!
obsnobs :: KripkeModelS5 -> Agent -> ([Prp],[Prp])
obsnobs :: KripkeModelS5 -> Agent -> (State, State)
obsnobs m :: KripkeModelS5
m@(KrMS5 [Action]
_ [(Agent, Partition)]
rel [(Action, Assignment)]
val) Agent
i = (State
obs,State
nobs) where
  propsets :: [[State]]
propsets = ([Action] -> [State]) -> Partition -> [[State]]
forall a b. (a -> b) -> [a] -> [b]
map (StateMap -> [Action] -> [State]
forall a b. (a -> b) -> [a] -> [b]
map (((Prp, Bool) -> Prp) -> Assignment -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst (Assignment -> State) -> (Action -> Assignment) -> StateMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Prp, Bool) -> Bool) -> Assignment -> Assignment
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp, Bool) -> Bool
forall a b. (a, b) -> b
snd (Assignment -> Assignment)
-> (Action -> Assignment) -> Action -> Assignment
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Action, Assignment)] -> Action -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Action, Assignment)]
val)) ([(Agent, Partition)] -> Agent -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, Partition)]
rel Agent
i)
  obs :: State
obs = (Prp -> Bool) -> State -> State
forall a. (a -> Bool) -> [a] -> [a]
filter (\Prp
p -> ([State] -> Bool) -> [[State]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((State -> Bool) -> [State] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Prp
p)) [[State]]
propsets) (KripkeModelS5 -> State
forall a. HasVocab a => a -> State
vocabOf KripkeModelS5
m)
  nobs :: State
nobs = (Prp -> Bool) -> State -> State
forall a. (a -> Bool) -> [a] -> [a]
filter (\Prp
p -> ([State] -> Bool) -> [[State]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((State -> Bool) -> [State] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
anydiffWith (Prp -> State -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Prp
p)) [[State]]
propsets) (KripkeModelS5 -> State
forall a. HasVocab a => a -> State
vocabOf KripkeModelS5
m)

-- | Test if all relations can be described using observariables.
descableRels :: KripkeModelS5 -> Bool
descableRels :: KripkeModelS5 -> Bool
descableRels m :: KripkeModelS5
m@(KrMS5 [Action]
ws [(Agent, Partition)]
rel [(Action, Assignment)]
val) = ((Agent, Partition) -> Bool) -> [(Agent, Partition)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Agent -> Bool
descable (Agent -> Bool)
-> ((Agent, Partition) -> Agent) -> (Agent, Partition) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Agent, Partition) -> Agent
forall a b. (a, b) -> a
fst) [(Agent, Partition)]
rel where
  wpairs :: [(Action, Action)]
wpairs = [ (Action
v,Action
w) | Action
v <- [Action]
ws, Action
w <- [Action]
ws ]
  descable :: Agent -> Bool
descable Agent
i = Bool
cover Bool -> Bool -> Bool
&& Bool
correct where
    (State
obs,State
nobs) = KripkeModelS5 -> Agent -> (State, State)
obsnobs KripkeModelS5
m Agent
i
    cover :: Bool
cover = State -> State
forall a. Ord a => [a] -> [a]
sort (KripkeModelS5 -> State
forall a. HasVocab a => a -> State
vocabOf KripkeModelS5
m) State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State -> State
forall a. Ord a => [a] -> [a]
sort (State
obs State -> State -> State
forall a. [a] -> [a] -> [a]
++ State
nobs) -- implies disjointness
    correct :: Bool
correct = ((Action, Action) -> Bool) -> [(Action, Action)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Action, Action)
pair -> (Action, Action) -> Bool
oldrel (Action, Action)
pair Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (Action, Action) -> Bool
newrel (Action, Action)
pair) [(Action, Action)]
wpairs
    oldrel :: (Action, Action) -> Bool
oldrel (Action
v,Action
w) = Action
v Action -> [Action] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Partition -> [Action]
forall a. HasCallStack => [a] -> a
head (([Action] -> Bool) -> Partition -> Partition
forall a. (a -> Bool) -> [a] -> [a]
filter (Action -> [Action] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Action
w) ([(Agent, Partition)] -> Agent -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, Partition)]
rel Agent
i))
    newrel :: (Action, Action) -> Bool
newrel (Action
v,Action
w) = (StateMap
factsAt Action
v State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
`intersect` State
obs) State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== (StateMap
factsAt Action
w State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
`intersect` State
obs)
    factsAt :: StateMap
factsAt Action
w = ((Prp, Bool) -> Prp) -> Assignment -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst (Assignment -> State) -> Assignment -> State
forall a b. (a -> b) -> a -> b
$ ((Prp, Bool) -> Bool) -> Assignment -> Assignment
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp, Bool) -> Bool
forall a b. (a, b) -> b
snd (Assignment -> Assignment) -> Assignment -> Assignment
forall a b. (a -> b) -> a -> b
$ [(Action, Assignment)] -> Action -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Action, Assignment)]
val Action
w

-- | Try to find an equivalent knowledge structure without
-- additional propositions. Will succeed iff valuations are
-- unique and relations can be described using observariables.
-- This is an alternative to `kripkeToKnsMulti`.
smartKripkeToKns :: PointedModelS5 -> Maybe KnowScene
smartKripkeToKns :: PointedModelS5 -> Maybe KnowScene
smartKripkeToKns (KripkeModelS5
m, Action
cur) =
  if KripkeModelS5 -> Bool
uniqueVals KripkeModelS5
m Bool -> Bool -> Bool
&& KripkeModelS5 -> Bool
descableRels KripkeModelS5
m
    then KnowScene -> Maybe KnowScene
forall a. a -> Maybe a
Just (PointedModelS5 -> KnowScene
smartKripkeToKnsWithoutChecks (KripkeModelS5
m, Action
cur))
    else Maybe KnowScene
forall a. Maybe a
Nothing

-- | Unsafe version of `smartKripkeToKns`.
smartKripkeToKnsWithoutChecks :: PointedModelS5 -> KnowScene
smartKripkeToKnsWithoutChecks :: PointedModelS5 -> KnowScene
smartKripkeToKnsWithoutChecks (m :: KripkeModelS5
m@(KrMS5 [Action]
worlds [(Agent, Partition)]
rel [(Action, Assignment)]
val), Action
cur) =
  (State -> Bdd -> [(Agent, State)] -> KnowStruct
KnS State
ps Bdd
law [(Agent, State)]
obs, State
curs) where
    ps :: State
ps = KripkeModelS5 -> State
forall a. HasVocab a => a -> State
vocabOf KripkeModelS5
m
    g :: StateMap
g Action
w = (Prp -> Bool) -> State -> State
forall a. (a -> Bool) -> [a] -> [a]
filter (Assignment -> Prp -> Bool
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply ([(Action, Assignment)] -> Action -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Action, Assignment)]
val Action
w)) State
ps
    law :: Bdd
law = [Bdd] -> Bdd
disSet [ State -> State -> Bdd
booloutof (StateMap
g Action
w) State
ps | Action
w <- [Action]
worlds ]
    obs :: [(Agent, State)]
obs = ((Agent, Partition) -> (Agent, State))
-> [(Agent, Partition)] -> [(Agent, State)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Agent
i,Partition
_) -> (Agent
i,Agent -> State
obsOf Agent
i) ) [(Agent, Partition)]
rel
    obsOf :: Agent -> State
obsOf = (State, State) -> State
forall a b. (a, b) -> a
fst((State, State) -> State)
-> (Agent -> (State, State)) -> Agent -> State
forall b c a. (b -> c) -> (a -> b) -> a -> c
.KripkeModelS5 -> Agent -> (State, State)
obsnobs KripkeModelS5
m
    curs :: State
curs = ((Prp, Bool) -> Prp) -> Assignment -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst (Assignment -> State) -> Assignment -> State
forall a b. (a -> b) -> a -> b
$ ((Prp, Bool) -> Bool) -> Assignment -> Assignment
forall a. (a -> Bool) -> [a] -> [a]
filter (Prp, Bool) -> Bool
forall a b. (a, b) -> b
snd (Assignment -> Assignment) -> Assignment -> Assignment
forall a b. (a -> b) -> a -> b
$ [(Action, Assignment)] -> Action -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Action, Assignment)]
val Action
cur

-- TODO: add a translation that uses start if if works, but normal translation otherwise?

-- TODO: test the above on symmetric and random models, how does it perform?

-- * From Knowledge Transformers to S5 Action Models


transformerToActionModelWithG :: KnowTransformer -> (ActionModelS5, StateMap)
transformerToActionModelWithG :: KnowTransformer -> (ActionModelS5, StateMap)
transformerToActionModelWithG trf :: KnowTransformer
trf@(KnTrf State
addprops Form
addlaw [(Prp, Bdd)]
changelaw [(Agent, State)]
addobs) = ([(Action, (Form, PostCondition))]
-> [(Agent, Partition)] -> ActionModelS5
ActMS5 [(Action, (Form, PostCondition))]
acts [(Agent, Partition)]
actrel, StateMap
g) where
  actlist :: [(State, Action)]
actlist = [State] -> [Action] -> [(State, Action)]
forall a b. [a] -> [b] -> [(a, b)]
zip (State -> [State]
forall a. [a] -> [[a]]
powerset State
addprops) [Action
0..(Action
2 Action -> Action -> Action
forall a b. (Num a, Integral b) => a -> b -> a
^ State -> Action
forall a. [a] -> Action
forall (t :: * -> *) a. Foldable t => t a -> Action
length State
addprops Action -> Action -> Action
forall a. Num a => a -> a -> a
- Action
1)]
  acts :: [(Action, (Form, PostCondition))]
acts    = [ (Action
a, (State -> Form
preFor State
ps, State -> PostCondition
forall {t :: * -> *}. Foldable t => t Prp -> PostCondition
postsFor State
ps)) | (State
ps,Action
a) <- [(State, Action)]
actlist, State -> Form
preFor State
ps Form -> Form -> Bool
forall a. Eq a => a -> a -> Bool
/= Form
Bot ] where
    preFor :: State -> Form
preFor State
ps = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ PostCondition -> Form -> Form
substitSet ((Prp -> (Prp, Form)) -> State -> PostCondition
forall a b. (a -> b) -> [a] -> [b]
map (, Form
Top) State
ps PostCondition -> PostCondition -> PostCondition
forall a. [a] -> [a] -> [a]
++ (Prp -> (Prp, Form)) -> State -> PostCondition
forall a b. (a -> b) -> [a] -> [b]
map (, Form
Bot) (State
addprops State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
\\ State
ps)) Form
addlaw
    postsFor :: t Prp -> PostCondition
postsFor t Prp
ps =
      [ (Prp
q, Bdd -> Form
formOf (Bdd -> Form) -> Bdd -> Form
forall a b. (a -> b) -> a -> b
$ Bdd -> Assignment -> Bdd
restrictSet ([(Prp, Bdd)]
changelaw [(Prp, Bdd)] -> Prp -> Bdd
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Prp
q) [(Action
p, Action -> Prp
P Action
p Prp -> t Prp -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Prp
ps) | (P Action
p) <- State
addprops])
      | Prp
q <- ((Prp, Bdd) -> Prp) -> [(Prp, Bdd)] -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bdd) -> Prp
forall a b. (a, b) -> a
fst [(Prp, Bdd)]
changelaw ]
  actrel :: [(Agent, Partition)]
actrel    = [(Agent
i,Agent -> Partition
rFor Agent
i) | Agent
i <- KnowTransformer -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KnowTransformer
trf] where
    rFor :: Agent -> Partition
rFor Agent
i  = ([(State, Action)] -> [Action]) -> [[(State, Action)]] -> Partition
forall a b. (a -> b) -> [a] -> [b]
map (((State, Action) -> Action) -> [(State, Action)] -> [Action]
forall a b. (a -> b) -> [a] -> [b]
map (State, Action) -> Action
forall a b. (a, b) -> b
snd) (((State, Action) -> (State, Action) -> Bool)
-> [(State, Action)] -> [[(State, Action)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy ( \ (State
x,Action
_) (State
y,Action
_) -> State
xState -> State -> Bool
forall a. Eq a => a -> a -> Bool
==State
y ) (Agent -> [(State, Action)]
pairs Agent
i))
    pairs :: Agent -> [(State, Action)]
pairs Agent
i = [(State, Action)] -> [(State, Action)]
forall a. Ord a => [a] -> [a]
sort ([(State, Action)] -> [(State, Action)])
-> [(State, Action)] -> [(State, Action)]
forall a b. (a -> b) -> a -> b
$ ((State, Action) -> (State, Action))
-> [(State, Action)] -> [(State, Action)]
forall a b. (a -> b) -> [a] -> [b]
map (\(State
set,Action
a) -> (State -> State -> State
forall a. Eq a => [a] -> [a] -> [a]
intersect State
set (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ [(Agent, State)]
addobs [(Agent, State)] -> Agent -> State
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
i,Action
a))
                         (((State, Action) -> Bool) -> [(State, Action)] -> [(State, Action)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Action -> [Action] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Action, (Form, PostCondition)) -> Action)
-> [(Action, (Form, PostCondition))] -> [Action]
forall a b. (a -> b) -> [a] -> [b]
map (Action, (Form, PostCondition)) -> Action
forall a b. (a, b) -> a
fst [(Action, (Form, PostCondition))]
acts) (Action -> Bool)
-> ((State, Action) -> Action) -> (State, Action) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State, Action) -> Action
forall a b. (a, b) -> b
snd) [(State, Action)]
actlist)
  g :: Action -> State
  g :: StateMap
g Action
a = [State] -> State
forall a. HasCallStack => [a] -> a
head [ State
x | (State
x, Action
a') <- [(State, Action)]
actlist, Action
a' Action -> Action -> Bool
forall a. Eq a => a -> a -> Bool
== Action
a ]

eventToAction :: Event -> PointedActionModelS5
eventToAction :: Event -> PointedActionModelS5
eventToAction (KnowTransformer
trf, State
event) = (ActionModelS5
actm, Action
faction) where
  (actm :: ActionModelS5
actm@(ActMS5 [(Action, (Form, PostCondition))]
acts [(Agent, Partition)]
_), StateMap
g) = KnowTransformer -> (ActionModelS5, StateMap)
transformerToActionModelWithG KnowTransformer
trf
  faction :: Action
faction = [Action] -> Action
forall a. HasCallStack => [a] -> a
head [ Action
a | (Action
a,(Form, PostCondition)
_) <- [(Action, (Form, PostCondition))]
acts, StateMap
g Action
a State -> State -> Bool
forall a. Eq a => a -> a -> Bool
== State
event ]

eventToActionMulti :: MultipointedEvent -> MultipointedActionModelS5
eventToActionMulti :: MultipointedEvent -> MultipointedActionModelS5
eventToActionMulti (KnowTransformer
trf, Bdd
actualEventLaw) = (ActionModelS5
actm, [Action]
factions) where
  (actm :: ActionModelS5
actm@(ActMS5 [(Action, (Form, PostCondition))]
acts [(Agent, Partition)]
_), StateMap
g) = KnowTransformer -> (ActionModelS5, StateMap)
transformerToActionModelWithG KnowTransformer
trf
  factions :: [Action]
factions = [ Action
a | (Action
a,(Form, PostCondition)
_) <- [(Action, (Form, PostCondition))]
acts, State -> Bdd -> Bool
bddEval (StateMap
g Action
a) Bdd
actualEventLaw ]

-- TODO add tests for the translations of unpointed and multipointed events above!

-- TODO Should "Event" rather be called "Pointed KnowTransformer" ?

-- * From S5 Action Models to Knowledge Transformers


actionToTransformerWithMap :: ActionModelS5 -> (KnowTransformer, StateMap)
actionToTransformerWithMap :: ActionModelS5 -> (KnowTransformer, StateMap)
actionToTransformerWithMap (ActMS5 [(Action, (Form, PostCondition))]
acts [(Agent, Partition)]
actrel) = (State
-> Form -> [(Prp, Bdd)] -> [(Agent, State)] -> KnowTransformer
KnTrf State
addprops Form
addlaw [(Prp, Bdd)]
changelaw [(Agent, State)]
addobs, StateMap
eventMap) where
  actions :: [Action]
actions = ((Action, (Form, PostCondition)) -> Action)
-> [(Action, (Form, PostCondition))] -> [Action]
forall a b. (a -> b) -> [a] -> [b]
map (Action, (Form, PostCondition)) -> Action
forall a b. (a, b) -> a
fst [(Action, (Form, PostCondition))]
acts
  ags :: [Agent]
ags          = ((Agent, Partition) -> Agent) -> [(Agent, Partition)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, Partition) -> Agent
forall a b. (a, b) -> a
fst [(Agent, Partition)]
actrel
  addprops :: State
addprops     = State
actionprops State -> State -> State
forall a. [a] -> [a] -> [a]
++ State
actrelprops
  (P Action
fstnewp)  = State -> Prp
freshp (State -> Prp) -> ([Form] -> State) -> [Form] -> Prp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> State
propsInForms ([Form] -> Prp) -> [Form] -> Prp
forall a b. (a -> b) -> a -> b
$ [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Form
pre Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: ((Prp, Form) -> [Form]) -> PostCondition -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Prp
p,Form
f) -> [Prp -> Form
PrpF Prp
p, Form
f]) PostCondition
posts | (Action
_,(Form
pre,PostCondition
posts)) <- [(Action, (Form, PostCondition))]
acts]  -- avoid props occurring anywhere in the in action model
  actionprops :: State
actionprops  = [Action -> Prp
P Action
fstnewp..Action -> Prp
P Action
maxactprop] -- new props to distinguish all actions
  maxactprop :: Action
maxactprop   = Action
fstnewp Action -> Action -> Action
forall a. Num a => a -> a -> a
+ Float -> Action
forall b. Integral b => Float -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Float -> Float -> Float
forall a. Floating a => a -> a -> a
logBase Float
2 (Action -> Float
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Action -> Float) -> Action -> Float
forall a b. (a -> b) -> a -> b
$ [Action] -> Action
forall a. [a] -> Action
forall (t :: * -> *) a. Foldable t => t a -> Action
length [Action]
actions) :: Float) Action -> Action -> Action
forall a. Num a => a -> a -> a
-Action
1
  actpropsRel :: [(Action, State)]
actpropsRel  = [Action] -> [State] -> [(Action, State)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Action]
actions (State -> [State]
forall a. [a] -> [[a]]
powerset State
actionprops)
  ell :: StateMap
ell          = [(Action, State)] -> StateMap
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Action, State)]
actpropsRel -- label actions with subsets of actionprops
  happens :: Action -> Form
happens Action
a    = State -> State -> Form
booloutofForm (StateMap
ell Action
a) State
actionprops -- boolean formula to say that a happens
  actform :: Form
actform      = [Form] -> Form
Disj [ [Form] -> Form
Conj [ Action -> Form
happens Action
a, Form
pre ] | (Action
a,(Form
pre,PostCondition
_)) <- [(Action, (Form, PostCondition))]
acts ] -- connect new propositions to preconditions
  actrelprops :: State
actrelprops  = [State] -> State
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Agent -> State
newps Agent
i | Agent
i <- [Agent]
ags ] -- new props to distinguish actions for i
  actrelpstart :: Action
actrelpstart = Action
maxactprop Action -> Action -> Action
forall a. Num a => a -> a -> a
+ Action
1
  newps :: Agent -> State
newps Agent
i      = (Action -> Prp) -> [Action] -> State
forall a b. (a -> b) -> [a] -> [b]
map (\Action
k -> Action -> Prp
P (Action
actrelpstart Action -> Action -> Action
forall a. Num a => a -> a -> a
+ (Action
newpstep Action -> Action -> Action
forall a. Num a => a -> a -> a
* Action
inum) Action -> Action -> Action
forall a. Num a => a -> a -> a
+Action
k)) [Action
0..(Agent -> Action
forall {b}. Integral b => Agent -> b
amount Agent
i Action -> Action -> Action
forall a. Num a => a -> a -> a
- Action
1)]
    where inum :: Action
inum = Maybe Action -> Action
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Action -> Action) -> Maybe Action -> Action
forall a b. (a -> b) -> a -> b
$ Agent -> [Agent] -> Maybe Action
forall a. Eq a => a -> [a] -> Maybe Action
elemIndex Agent
i (((Agent, Partition) -> Agent) -> [(Agent, Partition)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, Partition) -> Agent
forall a b. (a, b) -> a
fst [(Agent, Partition)]
actrel)
  amount :: Agent -> b
amount Agent
i     = Float -> b
forall b. Integral b => Float -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Float -> Float -> Float
forall a. Floating a => a -> a -> a
logBase Float
2 (Action -> Float
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Action -> Float) -> Action -> Float
forall a b. (a -> b) -> a -> b
$ Partition -> Action
forall a. [a] -> Action
forall (t :: * -> *) a. Foldable t => t a -> Action
length ([(Agent, Partition)] -> Agent -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, Partition)]
actrel Agent
i)) :: Float)
  newpstep :: Action
newpstep     = [Action] -> Action
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ Agent -> Action
forall {b}. Integral b => Agent -> b
amount Agent
i | Agent
i <- [Agent]
ags ]
  copyactrel :: Agent -> [([Action], State)]
copyactrel Agent
i = Partition -> [State] -> [([Action], State)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([(Agent, Partition)] -> Agent -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, Partition)]
actrel Agent
i) (State -> [State]
forall a. [a] -> [[a]]
powerset (Agent -> State
newps Agent
i)) -- label equclasses-of-actions with subsets-of-newps
  actrelfs :: Agent -> [Form]
actrelfs Agent
i   = [ Form -> Form -> Form
Equi (State -> State -> Form
booloutofForm ([([Action], State)] -> [Action] -> State
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply (Agent -> [([Action], State)]
copyactrel Agent
i) [Action]
as) (Agent -> State
newps Agent
i)) ([Form] -> Form
Disj ((Action -> Form) -> [Action] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Action -> Form
happens [Action]
as)) | [Action]
as <- [(Agent, Partition)] -> Agent -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, Partition)]
actrel Agent
i ]
  actrelforms :: [Form]
actrelforms  = (Agent -> [Form]) -> [Agent] -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Agent -> [Form]
actrelfs [Agent]
ags
  factsFor :: Action -> Agent -> State
factsFor Action
a Agent
i = ([Action], State) -> State
forall a b. (a, b) -> b
snd (([Action], State) -> State) -> ([Action], State) -> State
forall a b. (a -> b) -> a -> b
$ [([Action], State)] -> ([Action], State)
forall a. HasCallStack => [a] -> a
head ([([Action], State)] -> ([Action], State))
-> [([Action], State)] -> ([Action], State)
forall a b. (a -> b) -> a -> b
$ (([Action], State) -> Bool)
-> [([Action], State)] -> [([Action], State)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\([Action]
as,State
_) -> Action
a Action -> [Action] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Action]
as) (Agent -> [([Action], State)]
copyactrel Agent
i)
  eventMap :: StateMap
eventMap Action
a   = StateMap
ell Action
a State -> State -> State
forall a. [a] -> [a] -> [a]
++ (Agent -> State) -> [Agent] -> State
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Action -> Agent -> State
factsFor Action
a) [Agent]
ags
  addlaw :: Form
addlaw       = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj (Form
actform Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [Form]
actrelforms)
  changeprops :: State
changeprops  = State -> State
forall a. Ord a => [a] -> [a]
sort (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ State -> State
forall a. Ord a => [a] -> [a]
nubOrd (State -> State) -> State -> State
forall a b. (a -> b) -> a -> b
$ ((Action, (Form, PostCondition)) -> State)
-> [(Action, (Form, PostCondition))] -> State
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Action
_,(Form
_,PostCondition
posts)) -> ((Prp, Form) -> Prp) -> PostCondition -> State
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Form) -> Prp
forall a b. (a, b) -> a
fst PostCondition
posts) [(Action, (Form, PostCondition))]
acts -- propositions to be changed
  changelaw :: [(Prp, Bdd)]
changelaw    = [ (Prp
p, Prp -> Bdd
changeFor Prp
p) | Prp
p <- State
changeprops ] -- encode postconditions
  changeFor :: Prp -> Bdd
changeFor Prp
p  = [Bdd] -> Bdd
disSet [ Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Action -> Form
happens Action
a, PostCondition -> Prp -> Form
safepost PostCondition
posts Prp
p ] | (Action
a,(Form
_,PostCondition
posts)) <- [(Action, (Form, PostCondition))]
acts ]
  addobs :: [(Agent, State)]
addobs       = [ (Agent
i,Agent -> State
newps Agent
i) | Agent
i<- [Agent]
ags ]

actionToEvent :: PointedActionModelS5 -> Event
actionToEvent :: PointedActionModelS5 -> Event
actionToEvent (ActionModelS5
actm, Action
action) = (KnowTransformer
trf, State
efacts) where
  (KnowTransformer
trf, StateMap
g) = ActionModelS5 -> (KnowTransformer, StateMap)
actionToTransformerWithMap ActionModelS5
actm
  efacts :: State
efacts = StateMap
g Action
action

actionToEventMulti :: MultipointedActionModelS5 -> MultipointedEvent
actionToEventMulti :: MultipointedActionModelS5 -> MultipointedEvent
actionToEventMulti (ActionModelS5
actm, [Action]
curActions) = (KnowTransformer
trf, Bdd
curActionsLaw) where
  (trf :: KnowTransformer
trf@(KnTrf State
addprops Form
_ [(Prp, Bdd)]
_ [(Agent, State)]
_), StateMap
g) = ActionModelS5 -> (KnowTransformer, StateMap)
actionToTransformerWithMap ActionModelS5
actm
  curActionsLaw :: Bdd
curActionsLaw = [Bdd] -> Bdd
disSet [ State -> State -> Bdd
booloutof (StateMap
g Action
w) State
addprops | Action
w <- [Action]
curActions ]