{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}

{- |
Here we provide some wrapper functions for epistemic planning via model checking.
Our main inspiration for this are the following references.

- [LPW 2011]
  Benedikt Löwe, Eric Pacuit, and Andreas Witzel (2011):
  /DEL Planning and Some Tractable Cases/.
  LORI 2011.
  <https://doi.org/10.1007/978-3-642-24130-7_13>
- [EBMN 2017]
  Thorsten Engesser, Thomas Bolander, Robert Mattmüller, and Bernhard Nebel (2017):
  /Cooperative Epistemic Multi-Agent Planning for Implicit Coordination/.
  Ninth Workshop on Methods for Modalities.
  <https://doi.org/10.4204/EPTCS.243.6>

/NOTE/: This module is still experimental and under development.
-}

module SMCDEL.Other.Planning where

import Data.Dynamic
import Data.HasCacBDD hiding (Top,Bot)
import Data.List (intersect,nub,sort,(\\))
import qualified Data.Map as M

import SMCDEL.Internal.Help (apply)
import SMCDEL.Language
import qualified SMCDEL.Symbolic.S5 as Sym
import qualified SMCDEL.Symbolic.K as SymK
import qualified SMCDEL.Explicit.S5 as Exp
import qualified SMCDEL.Explicit.K as ExpK

-- * Generic Planning functions and type classes

class IsPlan a where
  -- | A formula saying that the given plan reaches the given goal.
  reaches :: a -> Form -> Form
  reachesOn :: (Semantics o) => a -> Form -> o -> Bool
  reachesOn a
plan Form
f o
start = o
start o -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= a -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches a
plan Form
f

-- * Sequential Plans with Public Announcements

{- $
We first consider /sequential/ plans which are list of formulas to be publicly and truthfully announced, one after each other.
These are also called /offline/ plans.
We write \(\sigma\) for any sqeuential plan and \(\epsilon\) for the empty plan which does nothing.
The following then defines a formula which says that the given plan reaches a given goal \(\gamma\):

\[
\begin{array}{ll}
\mathsf{reaches}(\epsilon)(\gamma) & := & \gamma \\
\mathsf{reaches}(\phi;\sigma)(\gamma) & := & \langle \phi \rangle (\mathsf{reaches}(\sigma)(\gamma))
\end{array}
\]

-}

-- | A list of announcements to be made.
type OfflinePlan = [Form]

instance IsPlan OfflinePlan where
  reaches :: OfflinePlan -> Form -> Form
reaches []          Form
goal = Form
goal
  reaches (Form
step:OfflinePlan
rest) Form
goal = OfflinePlan -> Form
Conj [Form
step, Form -> Form -> Form
PubAnnounce Form
step (OfflinePlan -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches OfflinePlan
rest Form
goal)]

-- | Depth-first search for sequential public announcement plans.
offlineSearch :: (Eq a, Semantics a, Update a Form) =>
   Int ->    -- ^ maximum number of actions
   a ->      -- ^ starting model or structure
   [Form] -> -- ^ available actions (as public announcements)
   [Form] -> -- ^ intermediate goals / safety formulas
   Form ->   -- ^ goal
   [OfflinePlan]
offlineSearch :: forall a.
(Eq a, Semantics a, Update a Form) =>
Int -> a -> OfflinePlan -> OfflinePlan -> Form -> [OfflinePlan]
offlineSearch Int
roundsLeft a
now OfflinePlan
acts OfflinePlan
safety Form
goal
  | a
now a -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= Form
goal = [ [] ] -- done, goal reached
  | Int
roundsLeft Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = [    ] -- give up
  | Bool
otherwise = [ Form
a Form -> OfflinePlan -> OfflinePlan
forall a. a -> [a] -> [a]
: OfflinePlan
rest
                | Form
a <- OfflinePlan
acts
                , a
now a -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= Form
a              -- only allow truthful announcements!
                , let new :: a
new = a
now a -> Form -> a
forall a b. Update a b => a -> b -> a
`update` Form
a  -- the new state
                , a
new a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
now                -- ignore useless actions
                , (Form -> Bool) -> OfflinePlan -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (a
new a -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|=) OfflinePlan
safety
                -- depth-first search:
                , OfflinePlan
rest <- Int -> a -> OfflinePlan -> OfflinePlan -> Form -> [OfflinePlan]
forall a.
(Eq a, Semantics a, Update a Form) =>
Int -> a -> OfflinePlan -> OfflinePlan -> Form -> [OfflinePlan]
offlineSearch (Int
roundsLeftInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) a
new OfflinePlan
acts OfflinePlan
safety Form
goal ]

-- * Policy Plans with General Actions

{- $
A /policy/, also called /online plan/ can include tests and choices, to decide which action to do depending on the results of previous announcements.
To represent such plans we use a tree where non-terminal nodes are actions to be done or formulas to be checked.
Each action node has one outgoing edge and each checking node has two outgoing edges, leading to the follow-up plans.
Terminal-nodes are stop signals.

In contrast to the previous section we now also allow more general actions, namely any type in the `Update` class, for example action models and transformers.
-}

-- | A plan with choice, i.e. a policy.
data Plan a = Stop -- ^ Stop.
            | Do String a (Plan a) -- ^ Do a given action.
            | Check Form (Plan a) -- ^ Check that a formula holds. (If not, fail.)
            | IfThenElse Form (Plan a) (Plan a) -- ^ If ... then ... else ... .
  deriving (Plan a -> Plan a -> Bool
(Plan a -> Plan a -> Bool)
-> (Plan a -> Plan a -> Bool) -> Eq (Plan a)
forall a. Eq a => Plan a -> Plan a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Plan a -> Plan a -> Bool
== :: Plan a -> Plan a -> Bool
$c/= :: forall a. Eq a => Plan a -> Plan a -> Bool
/= :: Plan a -> Plan a -> Bool
Eq,Eq (Plan a)
Eq (Plan a) =>
(Plan a -> Plan a -> Ordering)
-> (Plan a -> Plan a -> Bool)
-> (Plan a -> Plan a -> Bool)
-> (Plan a -> Plan a -> Bool)
-> (Plan a -> Plan a -> Bool)
-> (Plan a -> Plan a -> Plan a)
-> (Plan a -> Plan a -> Plan a)
-> Ord (Plan a)
Plan a -> Plan a -> Bool
Plan a -> Plan a -> Ordering
Plan a -> Plan a -> Plan a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Plan a)
forall a. Ord a => Plan a -> Plan a -> Bool
forall a. Ord a => Plan a -> Plan a -> Ordering
forall a. Ord a => Plan a -> Plan a -> Plan a
$ccompare :: forall a. Ord a => Plan a -> Plan a -> Ordering
compare :: Plan a -> Plan a -> Ordering
$c< :: forall a. Ord a => Plan a -> Plan a -> Bool
< :: Plan a -> Plan a -> Bool
$c<= :: forall a. Ord a => Plan a -> Plan a -> Bool
<= :: Plan a -> Plan a -> Bool
$c> :: forall a. Ord a => Plan a -> Plan a -> Bool
> :: Plan a -> Plan a -> Bool
$c>= :: forall a. Ord a => Plan a -> Plan a -> Bool
>= :: Plan a -> Plan a -> Bool
$cmax :: forall a. Ord a => Plan a -> Plan a -> Plan a
max :: Plan a -> Plan a -> Plan a
$cmin :: forall a. Ord a => Plan a -> Plan a -> Plan a
min :: Plan a -> Plan a -> Plan a
Ord,Int -> Plan a -> ShowS
[Plan a] -> ShowS
Plan a -> String
(Int -> Plan a -> ShowS)
-> (Plan a -> String) -> ([Plan a] -> ShowS) -> Show (Plan a)
forall a. Show a => Int -> Plan a -> ShowS
forall a. Show a => [Plan a] -> ShowS
forall a. Show a => Plan a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Plan a -> ShowS
showsPrec :: Int -> Plan a -> ShowS
$cshow :: forall a. Show a => Plan a -> String
show :: Plan a -> String
$cshowList :: forall a. Show a => [Plan a] -> ShowS
showList :: [Plan a] -> ShowS
Show)

-- | Try to execute a policy plan on a given state.
execute :: Update state a => Plan a -> state -> Maybe state
execute :: forall state a. Update state a => Plan a -> state -> Maybe state
execute Plan a
Stop                 state
s = state -> Maybe state
forall a. a -> Maybe a
Just state
s
execute (Do String
_ a
action Plan a
rest)   state
s | state
s state -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= a -> Form
forall a. HasPrecondition a => a -> Form
preOf a
action = Plan a -> state -> Maybe state
forall state a. Update state a => Plan a -> state -> Maybe state
execute Plan a
rest (state
s state -> a -> state
forall a b. Update a b => a -> b -> a
`update` a
action)
                               | Bool
otherwise         = Maybe state
forall a. Maybe a
Nothing
execute (Check Form
f Plan a
rest)       state
s = if state
s state -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= Form
f then Plan a -> state -> Maybe state
forall state a. Update state a => Plan a -> state -> Maybe state
execute Plan a
rest state
s else Maybe state
forall a. Maybe a
Nothing
execute (IfThenElse Form
f Plan a
pa Plan a
pb) state
s = if state
s state -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= Form
f then Plan a -> state -> Maybe state
forall state a. Update state a => Plan a -> state -> Maybe state
execute Plan a
pa   state
s else Plan a -> state -> Maybe state
forall state a. Update state a => Plan a -> state -> Maybe state
execute Plan a
pb state
s

instance IsPlan (Plan Form) where
  reaches :: Plan Form -> Form -> Form
reaches Plan Form
Stop Form
goal = Form
goal
  reaches (Do String
_ Form
toBeAn Plan Form
next) Form
goal = OfflinePlan -> Form
Conj [Form
toBeAn, Form -> Form -> Form
PubAnnounce Form
toBeAn (Plan Form -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches Plan Form
next Form
goal)]
  reaches (Check Form
toBeChecked Plan Form
next) Form
goal = OfflinePlan -> Form
Conj [Form
toBeChecked, Plan Form -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches Plan Form
next Form
goal]
  reaches (IfThenElse Form
condition Plan Form
planA Plan Form
planB) Form
goal =
    OfflinePlan -> Form
Conj [ Form
condition Form -> Form -> Form
`Impl` Plan Form -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches Plan Form
planA Form
goal, Form -> Form
Neg Form
condition Form -> Form -> Form
`Impl` Plan Form -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches Plan Form
planB Form
goal ]

instance IsPlan (Plan Sym.MultipointedEvent) where
  reaches :: Plan MultipointedEvent -> Form -> Form
reaches Plan MultipointedEvent
Stop Form
goal = Form
goal
  reaches (Do String
actLabel MultipointedEvent
action Plan MultipointedEvent
next) Form
goal = DynamicOp -> Form -> Form
dix (String -> Dynamic -> DynamicOp
Dyn String
actLabel (MultipointedEvent -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn MultipointedEvent
action)) (Plan MultipointedEvent -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches Plan MultipointedEvent
next Form
goal)
  reaches (Check Form
toBeChecked Plan MultipointedEvent
next) Form
goal = OfflinePlan -> Form
Conj [Form
toBeChecked, Plan MultipointedEvent -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches Plan MultipointedEvent
next Form
goal]
  reaches (IfThenElse Form
check Plan MultipointedEvent
planA Plan MultipointedEvent
planB) Form
goal =
    OfflinePlan -> Form
Conj [ Form
check Form -> Form -> Form
`Impl` Plan MultipointedEvent -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches Plan MultipointedEvent
planA Form
goal, Form -> Form
Neg Form
check Form -> Form -> Form
`Impl` Plan MultipointedEvent -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches Plan MultipointedEvent
planB Form
goal ]

-- | The \(((\alpha))\phi := \langle \alpha \rangle \land [\alpha] \phi\) abbreviation from [EBMN 2017].
-- We call it `dix` because it is a combination of /di/amond and bo/x/.
dix :: DynamicOp -> Form -> Form
dix :: DynamicOp -> Form -> Form
dix DynamicOp
op Form
f = OfflinePlan -> Form
Conj [DynamicOp -> Form -> Form
Dia DynamicOp
op Form
Top, DynamicOp -> Form -> Form
box DynamicOp
op Form
f]


-- * Planning Tasks

{- $
A planning task (also called a planning problem) is given by a start, a list of actions and a goal.
Note that \texttt{state} and \texttt{action} here are type variables,
  because we use polymorphic functions for explicit and symbolic planning in K and S5.
-}

data Task state action = Task state [(String,action)] Form
  deriving (Task state action -> Task state action -> Bool
(Task state action -> Task state action -> Bool)
-> (Task state action -> Task state action -> Bool)
-> Eq (Task state action)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall state action.
(Eq state, Eq action) =>
Task state action -> Task state action -> Bool
$c== :: forall state action.
(Eq state, Eq action) =>
Task state action -> Task state action -> Bool
== :: Task state action -> Task state action -> Bool
$c/= :: forall state action.
(Eq state, Eq action) =>
Task state action -> Task state action -> Bool
/= :: Task state action -> Task state action -> Bool
Eq,Eq (Task state action)
Eq (Task state action) =>
(Task state action -> Task state action -> Ordering)
-> (Task state action -> Task state action -> Bool)
-> (Task state action -> Task state action -> Bool)
-> (Task state action -> Task state action -> Bool)
-> (Task state action -> Task state action -> Bool)
-> (Task state action -> Task state action -> Task state action)
-> (Task state action -> Task state action -> Task state action)
-> Ord (Task state action)
Task state action -> Task state action -> Bool
Task state action -> Task state action -> Ordering
Task state action -> Task state action -> Task state action
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall state action.
(Ord state, Ord action) =>
Eq (Task state action)
forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Bool
forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Ordering
forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Task state action
$ccompare :: forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Ordering
compare :: Task state action -> Task state action -> Ordering
$c< :: forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Bool
< :: Task state action -> Task state action -> Bool
$c<= :: forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Bool
<= :: Task state action -> Task state action -> Bool
$c> :: forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Bool
> :: Task state action -> Task state action -> Bool
$c>= :: forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Bool
>= :: Task state action -> Task state action -> Bool
$cmax :: forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Task state action
max :: Task state action -> Task state action -> Task state action
$cmin :: forall state action.
(Ord state, Ord action) =>
Task state action -> Task state action -> Task state action
min :: Task state action -> Task state action -> Task state action
Ord,Int -> Task state action -> ShowS
[Task state action] -> ShowS
Task state action -> String
(Int -> Task state action -> ShowS)
-> (Task state action -> String)
-> ([Task state action] -> ShowS)
-> Show (Task state action)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall state action.
(Show state, Show action) =>
Int -> Task state action -> ShowS
forall state action.
(Show state, Show action) =>
[Task state action] -> ShowS
forall state action.
(Show state, Show action) =>
Task state action -> String
$cshowsPrec :: forall state action.
(Show state, Show action) =>
Int -> Task state action -> ShowS
showsPrec :: Int -> Task state action -> ShowS
$cshow :: forall state action.
(Show state, Show action) =>
Task state action -> String
show :: Task state action -> String
$cshowList :: forall state action.
(Show state, Show action) =>
[Task state action] -> ShowS
showList :: [Task state action] -> ShowS
Show)


-- Given a maximal search depth and a task, we search for a plan as follows.
findPlan :: (Eq state, Update state action) => Int -> Task state action -> [Plan action]
findPlan :: forall state action.
(Eq state, Update state action) =>
Int -> Task state action -> [Plan action]
findPlan Int
d (Task state
now [(String, action)]
acts Form
goal)
  | state
now state -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= Form
goal = [ Plan action
forall a. Plan a
Stop ]
  | Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0      = [      ]
  | Bool
otherwise   = [ String -> action -> Plan action -> Plan action
forall a. String -> a -> Plan a -> Plan a
Do String
lbl action
act Plan action
continue
                  | (String
lbl,action
act) <- [(String, action)]
acts
                  , state -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
isTrue state
now (action -> Form
forall a. HasPrecondition a => a -> Form
preOf action
act)
                  , state
now state -> state -> Bool
forall a. Eq a => a -> a -> Bool
/= state -> action -> state
forall a b. Update a b => a -> b -> a
update state
now action
act -- ignore useless actions
                  , Plan action
continue <- Int -> Task state action -> [Plan action]
forall state action.
(Eq state, Update state action) =>
Int -> Task state action -> [Plan action]
findPlan (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (state -> [(String, action)] -> Form -> Task state action
forall state action.
state -> [(String, action)] -> Form -> Task state action
Task (state -> action -> state
forall a b. Update a b => a -> b -> a
update state
now action
act) [(String, action)]
acts Form
goal) ]

-- * Perspective Shifts

class Eq o => HasPerspective o where
  asSeenBy :: o -> Agent -> o
  isLocalFor :: o -> Agent -> Bool
  isLocalFor o
state String
i = o
state o -> String -> o
forall o. HasPerspective o => o -> String -> o
`asSeenBy` String
i o -> o -> Bool
forall a. Eq a => a -> a -> Bool
== o
state

-- ** Perspective Shits in S5

-- $
-- Given a multipointed S5 model \((\M,s)\), the local state of an agent \(i\) is given by
-- \[ s^i := \{ w \in W \mid \exists v \in s : v \sim_i w \} \]
-- This is the definition given in [EBMN 2017] and implemented by `asSeenBy`.

-- | See ...
instance HasPerspective Exp.MultipointedModelS5 where
  asSeenBy :: MultipointedModelS5 -> String -> MultipointedModelS5
asSeenBy (m :: KripkeModelS5
m@(Exp.KrMS5 [Int]
_ [(String, Partition)]
rel [(Int, Assignment)]
_), [Int]
actualWorlds) String
agent = (KripkeModelS5
m, [Int]
seenWorlds) where
    seenWorlds :: [Int]
seenWorlds = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Partition -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Partition -> [Int]) -> Partition -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> Partition -> Partition
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([Int] -> Bool) -> [Int] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Int] -> Bool) -> ([Int] -> [Int]) -> [Int] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Int]
actualWorlds) ([(String, Partition)] -> String -> Partition
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(String, Partition)]
rel String
agent)

-- | Here we also implement perspective shifts in K.
-- The authors of [EBMN 2017] only consider S5.
-- Given a multipointed Kripke model $(\M,s)$, let the local state of $i$ be:
-- \[ s^i := \{ w \in W \mid \exists v \in s : v R_i w \} \]
-- Intuitively, these are all worlds the agent considers possible if the current state is $s$.
instance HasPerspective ExpK.MultipointedModel where
  asSeenBy :: MultipointedModel -> String -> MultipointedModel
asSeenBy (ExpK.KrM Map Int (Map Prp Bool, Map String [Int])
m, [Int]
actualWorlds) String
agent = (Map Int (Map Prp Bool, Map String [Int]) -> KripkeModel
ExpK.KrM Map Int (Map Prp Bool, Map String [Int])
m, [Int]
seenWorlds) where
    seenWorlds :: [Int]
seenWorlds = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Int -> (Map Prp Bool, Map String [Int]) -> [Int])
-> [Int] -> Map Int (Map Prp Bool, Map String [Int]) -> [Int]
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
M.foldlWithKey
      (\ [Int]
vs Int
w (Map Prp Bool
_,Map String [Int]
rel) -> [Int]
vs [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ Partition -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Map String [Int]
rel Map String [Int] -> String -> [Int]
forall k a. Ord k => Map k a -> k -> a
M.! String
agent | Int
w Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
actualWorlds ])
      []
      Map Int (Map Prp Bool, Map String [Int])
m

-- | We can also make perspective shifts symbolically.
-- In the S5 setting we can exploit symmetry as follows.
-- Suppose we have a multipointed scene $(\F,\sigma)$ where $\sigma \in \Lng_B(V)$ encodes the set of actual states.
-- As usual, we assume that agent $i$ has the observational variables $O_i$.
-- Then the perspective of $i$ is given by:
-- \[ \sigma^i :=  \exists (V \setminus O_i) \sigma \]
-- On purpose we do not use $\theta$ in order to avoid redundancy in the resulting multipointed scene.
instance HasPerspective Sym.MultipointedKnowScene where
  asSeenBy :: MultipointedKnowScene -> String -> MultipointedKnowScene
asSeenBy (Sym.KnS [Prp]
props Bdd
lawbdd [(String, [Prp])]
obs, Bdd
statesBdd) String
agent =
    ([Prp] -> Bdd -> [(String, [Prp])] -> KnowStruct
Sym.KnS [Prp]
props Bdd
lawbdd [(String, [Prp])]
obs, Bdd
seenStatesBdd) where
      seenStatesBdd :: Bdd
seenStatesBdd = [Int] -> Bdd -> Bdd
existsSet [Int]
otherps Bdd
statesBdd
      otherps :: [Int]
otherps = (Prp -> Int) -> [Prp] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Int
forall a. Enum a => a -> Int
fromEnum ([Prp]
props [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [(String, [Prp])] -> String -> [Prp]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(String, [Prp])]
obs String
agent)

-- ** Perspective Shits in K

{- $
Note that in S5 we always have \(s \subseteq s^i\), but this is not the case in general for K.
Also note that \((\cdot)^i\) is no longer idempotent if \(R_i\) is not transitive.

For the K setting we first need a way to flip the direction of the encoded relation \(\Omega_i\).
This is done by `fliRelBdd`.

Suppose we have a set of actual states encoded by \(\sigma \in \mathcal{L}_B(V)\).
Then the perspective of agent \(i\) is given by:

\[ \sigma^i := \exists V' (\Omega_i^\smile \land \sigma') \]

The following chain of equivalences shows that this definition does indeed what we want.
A state \(s\) satisifes the encoding of the local state \(\sigma^i\) iff it can be reached from a state \(t\) which satisfies the encoding of the global state \(\sigma\).

\[ \begin{array}{rl}
     & s \vDash \sigma^i \\
\iff & s \vDash \exists V' (\Omega_i^\smile \land \sigma') \\
\iff & \exists t \subseteq V : s \cup t' \vDash (\Omega_i^\smile \land \sigma') \\
\iff & \exists t \subseteq V : t \cup s' \vDash (\Omega_i        \land \sigma ) \\
\iff & \exists t \subseteq V : t \vDash \sigma \text{ and } t \cup s' \vDash \Omega_i
\end{array} \]

Again we do not include \(\theta\) here to avoid redundancy in the multipointed structure.

-}
-- TODO If not transitive, does it make sense to consider "what would my perspective be?"
-- TODO For KD45 we still have the following properties: ...

-- TODO instance HasPerspective Sym.MultipointedEvent

-- | Simultaneously prime and unprime all its variables. (TODO: \subst)
-- Formally, the resulting BDD is \( \Omega_i^\smile := \subst{V \cup V'}{V' \cup V} \Omega_i \).
flipRelBdd :: [Prp] -> SymK.RelBDD -> SymK.RelBDD
flipRelBdd :: [Prp] -> RelBDD -> RelBDD
flipRelBdd [Prp]
props = (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b. (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bdd -> Bdd) -> RelBDD -> RelBDD)
-> (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b. (a -> b) -> a -> b
$ [(Prp, Prp)] -> Bdd -> Bdd
Sym.relabelWith [(Prp -> Prp
SymK.mvP Prp
p, Prp -> Prp
SymK.cpP Prp
p) | Prp
p <- [Prp]
props ]

-- | See ...
instance HasPerspective SymK.MultipointedBelScene where
  asSeenBy :: MultipointedBelScene -> String -> MultipointedBelScene
asSeenBy (SymK.BlS [Prp]
props Bdd
lawbdd Map String RelBDD
obsBdds, Bdd
statesBdd) String
agent =
    ([Prp] -> Bdd -> Map String RelBDD -> BelStruct
SymK.BlS [Prp]
props Bdd
lawbdd Map String RelBDD
obsBdds, Bdd
seenStatesBdd) where
      flippedObsBdd :: RelBDD
flippedObsBdd = [Prp] -> RelBDD -> RelBDD
flipRelBdd [Prp]
props (Map String RelBDD
obsBdds Map String RelBDD -> String -> RelBDD
forall k a. Ord k => Map k a -> k -> a
M.! String
agent)
      seenStatesBdd :: Bdd
seenStatesBdd = RelBDD -> Bdd
SymK.unmvBdd (RelBDD -> Bdd) -> RelBDD -> Bdd
forall a b. (a -> b) -> a -> b
$ [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] -> [Prp]
SymK.cp [Prp]
props) (Bdd -> Bdd) -> RelBDD -> RelBDD
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                        (Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bdd -> RelBDD
SymK.cpBdd Bdd
statesBdd Tagged Dubbel (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b.
Tagged Dubbel (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RelBDD
flippedObsBdd)

-- TODO instance HasPerspective SymK.MultipointedEvent

-- * Implicit Cooperation

-- $ We now introduce owner functions as discussed in [EBMN 2017] and based on [LPW 2011]

data CoopTask state action = CoopTask state [Owned action] Form
  deriving (CoopTask state action -> CoopTask state action -> Bool
(CoopTask state action -> CoopTask state action -> Bool)
-> (CoopTask state action -> CoopTask state action -> Bool)
-> Eq (CoopTask state action)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall state action.
(Eq state, Eq action) =>
CoopTask state action -> CoopTask state action -> Bool
$c== :: forall state action.
(Eq state, Eq action) =>
CoopTask state action -> CoopTask state action -> Bool
== :: CoopTask state action -> CoopTask state action -> Bool
$c/= :: forall state action.
(Eq state, Eq action) =>
CoopTask state action -> CoopTask state action -> Bool
/= :: CoopTask state action -> CoopTask state action -> Bool
Eq,Eq (CoopTask state action)
Eq (CoopTask state action) =>
(CoopTask state action -> CoopTask state action -> Ordering)
-> (CoopTask state action -> CoopTask state action -> Bool)
-> (CoopTask state action -> CoopTask state action -> Bool)
-> (CoopTask state action -> CoopTask state action -> Bool)
-> (CoopTask state action -> CoopTask state action -> Bool)
-> (CoopTask state action
    -> CoopTask state action -> CoopTask state action)
-> (CoopTask state action
    -> CoopTask state action -> CoopTask state action)
-> Ord (CoopTask state action)
CoopTask state action -> CoopTask state action -> Bool
CoopTask state action -> CoopTask state action -> Ordering
CoopTask state action
-> CoopTask state action -> CoopTask state action
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall state action.
(Ord state, Ord action) =>
Eq (CoopTask state action)
forall state action.
(Ord state, Ord action) =>
CoopTask state action -> CoopTask state action -> Bool
forall state action.
(Ord state, Ord action) =>
CoopTask state action -> CoopTask state action -> Ordering
forall state action.
(Ord state, Ord action) =>
CoopTask state action
-> CoopTask state action -> CoopTask state action
$ccompare :: forall state action.
(Ord state, Ord action) =>
CoopTask state action -> CoopTask state action -> Ordering
compare :: CoopTask state action -> CoopTask state action -> Ordering
$c< :: forall state action.
(Ord state, Ord action) =>
CoopTask state action -> CoopTask state action -> Bool
< :: CoopTask state action -> CoopTask state action -> Bool
$c<= :: forall state action.
(Ord state, Ord action) =>
CoopTask state action -> CoopTask state action -> Bool
<= :: CoopTask state action -> CoopTask state action -> Bool
$c> :: forall state action.
(Ord state, Ord action) =>
CoopTask state action -> CoopTask state action -> Bool
> :: CoopTask state action -> CoopTask state action -> Bool
$c>= :: forall state action.
(Ord state, Ord action) =>
CoopTask state action -> CoopTask state action -> Bool
>= :: CoopTask state action -> CoopTask state action -> Bool
$cmax :: forall state action.
(Ord state, Ord action) =>
CoopTask state action
-> CoopTask state action -> CoopTask state action
max :: CoopTask state action
-> CoopTask state action -> CoopTask state action
$cmin :: forall state action.
(Ord state, Ord action) =>
CoopTask state action
-> CoopTask state action -> CoopTask state action
min :: CoopTask state action
-> CoopTask state action -> CoopTask state action
Ord,Int -> CoopTask state action -> ShowS
[CoopTask state action] -> ShowS
CoopTask state action -> String
(Int -> CoopTask state action -> ShowS)
-> (CoopTask state action -> String)
-> ([CoopTask state action] -> ShowS)
-> Show (CoopTask state action)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall state action.
(Show state, Show action) =>
Int -> CoopTask state action -> ShowS
forall state action.
(Show state, Show action) =>
[CoopTask state action] -> ShowS
forall state action.
(Show state, Show action) =>
CoopTask state action -> String
$cshowsPrec :: forall state action.
(Show state, Show action) =>
Int -> CoopTask state action -> ShowS
showsPrec :: Int -> CoopTask state action -> ShowS
$cshow :: forall state action.
(Show state, Show action) =>
CoopTask state action -> String
show :: CoopTask state action -> String
$cshowList :: forall state action.
(Show state, Show action) =>
[CoopTask state action] -> ShowS
showList :: [CoopTask state action] -> ShowS
Show)

instance (HasPerspective state, Eq action) => HasPerspective (CoopTask state action) where
  asSeenBy :: CoopTask state action -> String -> CoopTask state action
asSeenBy (CoopTask state
start [Owned action]
acts Form
goal) String
agent = state -> [Owned action] -> Form -> CoopTask state action
forall state action.
state -> [Owned action] -> Form -> CoopTask state action
CoopTask (state
start state -> String -> state
forall o. HasPerspective o => o -> String -> o
`asSeenBy` String
agent) [Owned action]
acts Form
goal


-- ** Implicitly coordinated sequential plans

-- $ As done in section 3.2 of [EBMN 2017].

-- | Helper type to label actions with strings.
type Labelled a = (String,a)

-- | An owned action is a pair of an agent and a labelled action.
type Owned action = (Agent,Labelled action)

-- | An implicitly coordinated plan is a sequence of owned actions.
-- Note: there is no check that the action is actually local for the agent!
type ICPlan action = [Owned action]

instance Typeable a => IsPlan (ICPlan a) where
  -- | A formula to say that the given IC plan reaches the given foal.
  reaches :: ICPlan a -> Form -> Form
reaches [] Form
goal = Form
goal
  reaches ((String
agent,(String
label,a
action)):ICPlan a
rest) Form
goal =
    String -> Form -> Form
K String
agent (DynamicOp -> Form -> Form
dix (String -> Dynamic -> DynamicOp
Dyn String
label (a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
action)) (ICPlan a -> Form -> Form
forall a. IsPlan a => a -> Form -> Form
reaches ICPlan a
rest Form
goal))

-- | Pretty print an IC plan.
ppICPlan :: ICPlan action -> String
ppICPlan :: forall action. ICPlan action -> String
ppICPlan [] = String
""
ppICPlan [(String
agent,(String
label,action
_))] = String
agent String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
label String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
ppICPlan ((String
agent,(String
label,action
_)):[Owned action]
rest) = String
agent String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
label String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"; " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Owned action] -> String
forall action. ICPlan action -> String
ppICPlan [Owned action]
rest

-- | Check that the given IC plan solves the given Coop task.
icSolves :: (Typeable action, Semantics state) => ICPlan action -> CoopTask state action -> Bool
icSolves :: forall action state.
(Typeable action, Semantics state) =>
ICPlan action -> CoopTask state action -> Bool
icSolves ICPlan action
plan (CoopTask state
start ICPlan action
acts Form
goal) =
  ((String, Labelled action) -> Bool) -> ICPlan action -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((String, Labelled action) -> String) -> ICPlan action -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Labelled action) -> String
forall a b. (a, b) -> a
fst ICPlan action
acts) (String -> Bool)
-> ((String, Labelled action) -> String)
-> (String, Labelled action)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Labelled action) -> String
forall a b. (a, b) -> a
fst) ICPlan action
plan Bool -> Bool -> Bool
&& ICPlan action -> Form -> state -> Bool
forall o. Semantics o => ICPlan action -> Form -> o -> Bool
forall a o. (IsPlan a, Semantics o) => a -> Form -> o -> Bool
reachesOn ICPlan action
plan Form
goal state
start

-- | Depth-first search for sequential IC plans.
findSequentialIcPlan :: (Typeable action, Eq state, Update state action) => Int -> CoopTask state action -> [ICPlan action]
findSequentialIcPlan :: forall action state.
(Typeable action, Eq state, Update state action) =>
Int -> CoopTask state action -> [ICPlan action]
findSequentialIcPlan Int
d (CoopTask state
now [Owned action]
acts Form
goal)
  | state
now state -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= Form
goal = [ [] ] -- goal reached
  | Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0      = [    ] -- give up
  | Bool
otherwise   = [ (String
agent,(String
label, action
act)) Owned action -> [Owned action] -> [Owned action]
forall a. a -> [a] -> [a]
: [Owned action]
continue
                  | a :: Owned action
a@(String
agent,(String
label,action
act)) <- [Owned action]
acts
                  , state
now state -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= action -> Form
forall a. HasPrecondition a => a -> Form
preOf action
act           -- action must be executable
                  , state
now state -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= String -> Form -> Form
K String
agent (action -> Form
forall a. HasPrecondition a => a -> Form
preOf action
act) -- agent must know that it is executable!
                  , state
now state -> state -> Bool
forall a. Eq a => a -> a -> Bool
/= state -> action -> state
forall a b. Update a b => a -> b -> a
update state
now action
act      -- ignore useless actions
                  , [Owned action]
continue <- Int -> CoopTask state action -> [[Owned action]]
forall action state.
(Typeable action, Eq state, Update state action) =>
Int -> CoopTask state action -> [ICPlan action]
findSequentialIcPlan (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (state -> [Owned action] -> Form -> CoopTask state action
forall state action.
state -> [Owned action] -> Form -> CoopTask state action
CoopTask (state -> action -> state
forall a b. Update a b => a -> b -> a
update state
now action
act) [Owned action]
acts Form
goal) -- DFS!
                  , (Owned action
aOwned action -> [Owned action] -> [Owned action]
forall a. a -> [a] -> [a]
:[Owned action]
continue) [Owned action] -> CoopTask state action -> Bool
forall action state.
(Typeable action, Semantics state) =>
ICPlan action -> CoopTask state action -> Bool
`icSolves` state -> [Owned action] -> Form -> CoopTask state action
forall state action.
state -> [Owned action] -> Form -> CoopTask state action
CoopTask state
now [Owned action]
acts Form
goal  ]

-- | Breadth-first search for shortest IC plans.
findSequentialIcPlanBFS :: (Typeable action, Eq state, Update state action) => Int -> CoopTask state action -> Maybe (ICPlan action)
findSequentialIcPlanBFS :: forall action state.
(Typeable action, Eq state, Update state action) =>
Int -> CoopTask state action -> Maybe (ICPlan action)
findSequentialIcPlanBFS Int
maxDepth (CoopTask state
start [Owned action]
acts Form
goal) = [([Owned action], state)] -> Maybe [Owned action]
forall {a}.
(Eq a, Update a action) =>
[([Owned action], a)] -> Maybe [Owned action]
loop [([],state
start)] where
  loop :: [([Owned action], a)] -> Maybe [Owned action]
loop [] = Maybe [Owned action]
forall a. Maybe a
Nothing
  loop (([Owned action]
done,a
now):[([Owned action], a)]
rest)
    | a
now a -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= Form
goal = [Owned action] -> Maybe [Owned action]
forall a. a -> Maybe a
Just [Owned action]
done -- FIXME: need stronger condition >> icSolves (CoopTask now acts goal) (done)
    | Bool
otherwise   = [([Owned action], a)] -> Maybe [Owned action]
loop ([([Owned action], a)] -> Maybe [Owned action])
-> [([Owned action], a)] -> Maybe [Owned action]
forall a b. (a -> b) -> a -> b
$ [([Owned action], a)]
rest [([Owned action], a)]
-> [([Owned action], a)] -> [([Owned action], a)]
forall a. [a] -> [a] -> [a]
++
                      [ ([Owned action]
done [Owned action] -> [Owned action] -> [Owned action]
forall a. [a] -> [a] -> [a]
++ [Owned action
a], a -> action -> a
forall a b. Update a b => a -> b -> a
update a
now action
act) -- TODO optimize (vocabOf start) ?
                      | [Owned action] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Owned action]
done Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxDepth     -- do not use more than maxDepth actions
                      , a :: Owned action
a@(String
agent,(String
_,action
act)) <- [Owned action]
acts
                      , a
now a -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= action -> Form
forall a. HasPrecondition a => a -> Form
preOf action
act           -- action must be executable
                      , a
now a -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
|= String -> Form -> Form
K String
agent (action -> Form
forall a. HasPrecondition a => a -> Form
preOf action
act) -- agent must know that it is executable!
                      , a
now a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a -> action -> a
forall a b. Update a b => a -> b -> a
update a
now action
act      -- ignore useless actions
                      ]

-- TODO
-- - [x] DFS with max depth
-- - [x] BFS
-- - conditional plans
-- - random CoopTask generation
-- - testing
-- - plan visualisation?
-- - MCTS